Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0z | Unicode version |
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.) |
Ref | Expression |
---|---|
0z |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7027 | . 2 | |
2 | eqid 2040 | . . 3 | |
3 | 2 | 3mix1i 1076 | . 2 |
4 | elz 8247 | . 2 | |
5 | 1, 3, 4 | mpbir2an 849 | 1 |
Colors of variables: wff set class |
Syntax hints: w3o 884 wceq 1243 wcel 1393 cr 6888 cc0 6889 cneg 7183 cn 7914 cz 8245 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-1re 6978 ax-addrcl 6981 ax-rnegex 6993 |
This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-rab 2315 df-v 2559 df-un 2922 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-br 3765 df-iota 4867 df-fv 4910 df-ov 5515 df-neg 7185 df-z 8246 |
This theorem is referenced by: 0zd 8257 nn0ssz 8263 znegcl 8276 zgt0ge1 8302 nn0n0n1ge2b 8320 nn0lt10b 8321 nnm1ge0 8326 gtndiv 8335 msqznn 8338 zeo 8343 nn0ind 8352 fnn0ind 8354 nn0uz 8507 1eluzge0 8516 2eluzge0OLD 8518 eqreznegel 8549 qreccl 8576 qdivcl 8577 irrmul 8581 fz10 8910 fz01en 8917 fzpreddisj 8933 fzshftral 8970 fznn0 8974 fz0tp 8981 elfz0ubfz0 8982 1fv 8996 lbfzo0 9037 elfzonlteqm1 9066 fzo01 9072 fzo0to2pr 9074 fzo0to3tp 9075 flqge0nn0 9135 divfl0 9138 btwnzge0 9142 modqmulnn 9184 frecfzennn 9203 expival 9257 qexpclz 9276 nn0abscl 9681 nnabscl 9696 climz 9813 climaddc1 9849 climmulc2 9851 climsubc1 9852 climsubc2 9853 climlec2 9861 algcvgblem 9888 |
Copyright terms: Public domain | W3C validator |