![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0z | GIF version |
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.) |
Ref | Expression |
---|---|
0z | ⊢ 0 ∈ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7987 | . 2 ⊢ 0 ∈ ℝ | |
2 | eqid 2189 | . . 3 ⊢ 0 = 0 | |
3 | 2 | 3mix1i 1171 | . 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ) |
4 | elz 9285 | . 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ))) | |
5 | 1, 3, 4 | mpbir2an 944 | 1 ⊢ 0 ∈ ℤ |
Colors of variables: wff set class |
Syntax hints: ∨ w3o 979 = wceq 1364 ∈ wcel 2160 ℝcr 7840 0cc0 7841 -cneg 8159 ℕcn 8949 ℤcz 9283 |
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 7935 ax-addrcl 7938 ax-rnegex 7950 |
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 5899 df-neg 8161 df-z 9284 |
This theorem is referenced by: 0zd 9295 nn0ssz 9301 znegcl 9314 zgt0ge1 9341 nn0n0n1ge2b 9362 nn0lt10b 9363 nnm1ge0 9369 gtndiv 9378 msqznn 9383 zeo 9388 nn0ind 9397 fnn0ind 9399 nn0uz 9592 1eluzge0 9604 elnn0dc 9641 eqreznegel 9644 qreccl 9672 qdivcl 9673 irrmul 9677 fz10 10076 fz01en 10083 fzpreddisj 10101 fzshftral 10138 fznn0 10143 fz1ssfz0 10147 fz0sn 10151 fz0tp 10152 fz0to3un2pr 10153 fz0to4untppr 10154 elfz0ubfz0 10155 1fv 10169 lbfzo0 10211 elfzonlteqm1 10240 fzo01 10246 fzo0to2pr 10248 fzo0to3tp 10249 flqge0nn0 10324 divfl0 10327 btwnzge0 10331 modqmulnn 10373 zmodfz 10377 modqid 10380 zmodid2 10383 q0mod 10386 modqmuladdnn0 10399 frecfzennn 10457 qexpclz 10572 qsqeqor 10662 facdiv 10750 bcval 10761 bcnn 10769 bcm1k 10772 bcval5 10775 bcpasc 10778 4bc2eq6 10786 hashinfom 10790 rexfiuz 11030 qabsor 11116 nn0abscl 11126 nnabscl 11141 climz 11332 climaddc1 11369 climmulc2 11371 climsubc1 11372 climsubc2 11373 climlec2 11381 binomlem 11523 binom 11524 bcxmas 11529 arisum2 11539 explecnv 11545 ef0lem 11700 dvdsval2 11829 dvdsdc 11837 moddvds 11838 dvds0 11845 0dvds 11850 zdvdsdc 11851 dvdscmulr 11859 dvdsmulcr 11860 dvdslelemd 11881 dvdsabseq 11885 divconjdvds 11887 alzdvds 11892 fzo0dvdseq 11895 odd2np1lem 11909 gcdmndc 11977 gcdsupex 11990 gcdsupcl 11991 gcd0val 11993 gcddvds 11996 gcd0id 12012 gcdid0 12013 gcdid 12019 bezoutlema 12032 bezoutlemb 12033 bezoutlembi 12038 dfgcd3 12043 dfgcd2 12047 gcdmultiplez 12054 dvdssq 12064 algcvgblem 12081 lcmmndc 12094 lcm0val 12097 dvdslcm 12101 lcmeq0 12103 lcmgcd 12110 lcmdvds 12111 lcmid 12112 3lcm2e6woprm 12118 6lcm4e12 12119 cncongr2 12136 sqrt2irrap 12212 dfphi2 12252 phiprmpw 12254 crth 12256 phimullem 12257 eulerthlemfi 12260 hashgcdeq 12271 phisum 12272 pceu 12327 pcdiv 12334 pc0 12336 pcqdiv 12339 pcexp 12341 pcxnn0cl 12342 pcxcl 12343 pcxqcl 12344 pcdvdstr 12359 dvdsprmpweqnn 12368 pcaddlem 12371 pcadd 12372 pcfaclem 12381 qexpz 12384 zgz 12405 igz 12406 4sqlem19 12441 ennnfonelemjn 12453 ennnfonelem1 12458 mulg0 13067 subgmulg 13127 zring0 13899 rpcxp0 14776 lgslem2 14860 lgsfcl2 14865 lgs0 14872 lgsneg 14883 lgsdilem 14886 lgsdir2lem3 14889 lgsdir 14894 lgsdilem2 14895 lgsdi 14896 lgsne0 14897 lgsprme0 14901 lgsdirnn0 14906 lgsdinn0 14907 apdifflemr 15254 apdiff 15255 iswomni0 15258 nconstwlpolem 15272 |
Copyright terms: Public domain | W3C validator |