![]() |
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 7549 | . 2 ⊢ 0 ∈ ℝ | |
2 | eqid 2089 | . . 3 ⊢ 0 = 0 | |
3 | 2 | 3mix1i 1116 | . 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ) |
4 | elz 8813 | . 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ))) | |
5 | 1, 3, 4 | mpbir2an 889 | 1 ⊢ 0 ∈ ℤ |
Colors of variables: wff set class |
Syntax hints: ∨ w3o 924 = wceq 1290 ∈ wcel 1439 ℝcr 7410 0cc0 7411 -cneg 7715 ℕcn 8483 ℤcz 8811 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-1re 7500 ax-addrcl 7503 ax-rnegex 7515 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-rab 2369 df-v 2622 df-un 3004 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-iota 4993 df-fv 5036 df-ov 5669 df-neg 7717 df-z 8812 |
This theorem is referenced by: 0zd 8823 nn0ssz 8829 znegcl 8842 zgt0ge1 8869 nn0n0n1ge2b 8887 nn0lt10b 8888 nnm1ge0 8893 gtndiv 8902 msqznn 8907 zeo 8912 nn0ind 8921 fnn0ind 8923 nn0uz 9114 1eluzge0 9123 eqreznegel 9160 qreccl 9188 qdivcl 9189 irrmul 9193 fz10 9521 fz01en 9528 fzpreddisj 9546 fzshftral 9583 fznn0 9588 fz1ssfz0 9592 fz0tp 9596 elfz0ubfz0 9597 1fv 9611 lbfzo0 9653 elfzonlteqm1 9682 fzo01 9688 fzo0to2pr 9690 fzo0to3tp 9691 flqge0nn0 9761 divfl0 9764 btwnzge0 9768 modqmulnn 9810 zmodfz 9814 modqid 9817 zmodid2 9820 q0mod 9823 modqmuladdnn0 9836 frecfzennn 9894 qexpclz 10037 facdiv 10207 bcval 10218 bcnn 10226 bcm1k 10229 ibcval5 10232 bcpasc 10235 4bc2eq6 10243 hashinfom 10247 rexfiuz 10483 qabsor 10569 nn0abscl 10579 nnabscl 10594 climz 10741 climaddc1 10778 climmulc2 10780 climsubc1 10781 climsubc2 10782 climlec2 10791 binomlem 10938 binom 10939 bcxmas 10944 arisum2 10954 explecnv 10960 ef0lem 11011 dvdsval2 11138 dvdsdc 11143 moddvds 11144 dvds0 11150 0dvds 11155 zdvdsdc 11156 dvdscmulr 11164 dvdsmulcr 11165 dvdslelemd 11183 dvdsabseq 11187 divconjdvds 11189 alzdvds 11194 fzo0dvdseq 11197 odd2np1lem 11211 gcdmndc 11279 gcdsupex 11288 gcdsupcl 11289 gcd0val 11291 gcddvds 11294 gcd0id 11309 gcdid0 11310 gcdid 11316 bezoutlema 11327 bezoutlemb 11328 bezoutlembi 11333 dfgcd3 11338 dfgcd2 11342 gcdmultiplez 11349 dvdssq 11359 algcvgblem 11370 lcmmndc 11383 lcm0val 11386 dvdslcm 11390 lcmeq0 11392 lcmgcd 11399 lcmdvds 11400 lcmid 11401 3lcm2e6woprm 11407 6lcm4e12 11408 cncongr2 11425 sqrt2irrap 11497 dfphi2 11535 phiprmpw 11537 crth 11539 phimullem 11540 hashgcdeq 11543 |
Copyright terms: Public domain | W3C validator |