![]() |
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 7988 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqid 2189 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | 3mix1i 1171 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | elz 9286 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | mpbir2an 944 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-1re 7936 ax-addrcl 7939 ax-rnegex 7951 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-un 3148 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-iota 5196 df-fv 5243 df-ov 5900 df-neg 8162 df-z 9285 |
This theorem is referenced by: 0zd 9296 nn0ssz 9302 znegcl 9315 zgt0ge1 9342 nn0n0n1ge2b 9363 nn0lt10b 9364 nnm1ge0 9370 gtndiv 9379 msqznn 9384 zeo 9389 nn0ind 9398 fnn0ind 9400 nn0uz 9594 1eluzge0 9606 elnn0dc 9643 eqreznegel 9646 qreccl 9674 qdivcl 9675 irrmul 9679 fz10 10078 fz01en 10085 fzpreddisj 10103 fzshftral 10140 fznn0 10145 fz1ssfz0 10149 fz0sn 10153 fz0tp 10154 fz0to3un2pr 10155 fz0to4untppr 10156 elfz0ubfz0 10157 1fv 10171 lbfzo0 10213 elfzonlteqm1 10242 fzo01 10248 fzo0to2pr 10250 fzo0to3tp 10251 flqge0nn0 10326 divfl0 10329 btwnzge0 10333 modqmulnn 10375 zmodfz 10379 modqid 10382 zmodid2 10385 q0mod 10388 modqmuladdnn0 10401 frecfzennn 10459 qexpclz 10575 qsqeqor 10665 facdiv 10753 bcval 10764 bcnn 10772 bcm1k 10775 bcval5 10778 bcpasc 10781 4bc2eq6 10789 hashinfom 10793 rexfiuz 11033 qabsor 11119 nn0abscl 11129 nnabscl 11144 climz 11335 climaddc1 11372 climmulc2 11374 climsubc1 11375 climsubc2 11376 climlec2 11384 binomlem 11526 binom 11527 bcxmas 11532 arisum2 11542 explecnv 11548 ef0lem 11703 dvdsval2 11832 dvdsdc 11840 moddvds 11841 dvds0 11848 0dvds 11853 zdvdsdc 11854 dvdscmulr 11862 dvdsmulcr 11863 dvdslelemd 11884 dvdsabseq 11888 divconjdvds 11890 alzdvds 11895 fzo0dvdseq 11898 odd2np1lem 11912 gcdmndc 11980 gcdsupex 11993 gcdsupcl 11994 gcd0val 11996 gcddvds 11999 gcd0id 12015 gcdid0 12016 gcdid 12022 bezoutlema 12035 bezoutlemb 12036 bezoutlembi 12041 dfgcd3 12046 dfgcd2 12050 gcdmultiplez 12057 dvdssq 12067 algcvgblem 12084 lcmmndc 12097 lcm0val 12100 dvdslcm 12104 lcmeq0 12106 lcmgcd 12113 lcmdvds 12114 lcmid 12115 3lcm2e6woprm 12121 6lcm4e12 12122 cncongr2 12139 sqrt2irrap 12215 dfphi2 12255 phiprmpw 12257 crth 12259 phimullem 12260 eulerthlemfi 12263 hashgcdeq 12274 phisum 12275 pceu 12330 pcdiv 12337 pc0 12339 pcqdiv 12342 pcexp 12344 pcxnn0cl 12345 pcxcl 12346 pcxqcl 12347 pcdvdstr 12362 dvdsprmpweqnn 12371 pcaddlem 12374 pcadd 12375 pcfaclem 12384 qexpz 12387 zgz 12408 igz 12409 4sqlem19 12444 ennnfonelemjn 12456 ennnfonelem1 12461 mulg0 13082 subgmulg 13144 zring0 13916 rpcxp0 14796 lgslem2 14880 lgsfcl2 14885 lgs0 14892 lgsneg 14903 lgsdilem 14906 lgsdir2lem3 14909 lgsdir 14914 lgsdilem2 14915 lgsdi 14916 lgsne0 14917 lgsprme0 14921 lgsdirnn0 14926 lgsdinn0 14927 apdifflemr 15274 apdiff 15275 iswomni0 15278 nconstwlpolem 15292 |
Copyright terms: Public domain | W3C validator |