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 7890 | . 2 | |
2 | eqid 2164 | . . 3 | |
3 | 2 | 3mix1i 1158 | . 2 |
4 | elz 9184 | . 2 | |
5 | 1, 3, 4 | mpbir2an 931 | 1 |
Colors of variables: wff set class |
Syntax hints: w3o 966 wceq 1342 wcel 2135 cr 7743 cc0 7744 cneg 8061 cn 8848 cz 9182 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-1re 7838 ax-addrcl 7841 ax-rnegex 7853 |
This theorem depends on definitions: df-bi 116 df-3or 968 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-rab 2451 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-iota 5147 df-fv 5190 df-ov 5839 df-neg 8063 df-z 9183 |
This theorem is referenced by: 0zd 9194 nn0ssz 9200 znegcl 9213 zgt0ge1 9240 nn0n0n1ge2b 9261 nn0lt10b 9262 nnm1ge0 9268 gtndiv 9277 msqznn 9282 zeo 9287 nn0ind 9296 fnn0ind 9298 nn0uz 9491 1eluzge0 9503 elnn0dc 9540 eqreznegel 9543 qreccl 9571 qdivcl 9572 irrmul 9576 fz10 9971 fz01en 9978 fzpreddisj 9996 fzshftral 10033 fznn0 10038 fz1ssfz0 10042 fz0sn 10046 fz0tp 10047 fz0to3un2pr 10048 fz0to4untppr 10049 elfz0ubfz0 10050 1fv 10064 lbfzo0 10106 elfzonlteqm1 10135 fzo01 10141 fzo0to2pr 10143 fzo0to3tp 10144 flqge0nn0 10218 divfl0 10221 btwnzge0 10225 modqmulnn 10267 zmodfz 10271 modqid 10274 zmodid2 10277 q0mod 10280 modqmuladdnn0 10293 frecfzennn 10351 qexpclz 10466 facdiv 10640 bcval 10651 bcnn 10659 bcm1k 10662 bcval5 10665 bcpasc 10668 4bc2eq6 10676 hashinfom 10680 rexfiuz 10917 qabsor 11003 nn0abscl 11013 nnabscl 11028 climz 11219 climaddc1 11256 climmulc2 11258 climsubc1 11259 climsubc2 11260 climlec2 11268 binomlem 11410 binom 11411 bcxmas 11416 arisum2 11426 explecnv 11432 ef0lem 11587 dvdsval2 11716 dvdsdc 11724 moddvds 11725 dvds0 11732 0dvds 11737 zdvdsdc 11738 dvdscmulr 11746 dvdsmulcr 11747 dvdslelemd 11766 dvdsabseq 11770 divconjdvds 11772 alzdvds 11777 fzo0dvdseq 11780 odd2np1lem 11794 gcdmndc 11862 gcdsupex 11875 gcdsupcl 11876 gcd0val 11878 gcddvds 11881 gcd0id 11897 gcdid0 11898 gcdid 11904 bezoutlema 11917 bezoutlemb 11918 bezoutlembi 11923 dfgcd3 11928 dfgcd2 11932 gcdmultiplez 11939 dvdssq 11949 algcvgblem 11960 lcmmndc 11973 lcm0val 11976 dvdslcm 11980 lcmeq0 11982 lcmgcd 11989 lcmdvds 11990 lcmid 11991 3lcm2e6woprm 11997 6lcm4e12 11998 cncongr2 12015 sqrt2irrap 12091 dfphi2 12131 phiprmpw 12133 crth 12135 phimullem 12136 eulerthlemfi 12139 hashgcdeq 12150 phisum 12151 pceu 12206 pcdiv 12213 pc0 12215 pcqdiv 12218 pcexp 12220 pcxnn0cl 12221 pcxcl 12222 pcdvdstr 12237 dvdsprmpweqnn 12246 pcaddlem 12249 pcadd 12250 pcfaclem 12258 qexpz 12261 ennnfonelemjn 12278 ennnfonelem1 12283 rpcxp0 13366 apdifflemr 13767 apdiff 13768 iswomni0 13771 nconstwlpolem 13784 |
Copyright terms: Public domain | W3C validator |