![]() |
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 7488 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqid 2088 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | 3mix1i 1115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | elz 8752 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | mpbir2an 888 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-1re 7439 ax-addrcl 7442 ax-rnegex 7454 |
This theorem depends on definitions: df-bi 115 df-3or 925 df-3an 926 df-tru 1292 df-nf 1395 df-sb 1693 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ral 2364 df-rex 2365 df-rab 2368 df-v 2621 df-un 3003 df-sn 3452 df-pr 3453 df-op 3455 df-uni 3654 df-br 3846 df-iota 4980 df-fv 5023 df-ov 5655 df-neg 7656 df-z 8751 |
This theorem is referenced by: 0zd 8762 nn0ssz 8768 znegcl 8781 zgt0ge1 8808 nn0n0n1ge2b 8826 nn0lt10b 8827 nnm1ge0 8832 gtndiv 8841 msqznn 8846 zeo 8851 nn0ind 8860 fnn0ind 8862 nn0uz 9053 1eluzge0 9062 eqreznegel 9099 qreccl 9127 qdivcl 9128 irrmul 9132 fz10 9460 fz01en 9467 fzpreddisj 9485 fzshftral 9522 fznn0 9527 fz1ssfz0 9531 fz0tp 9535 elfz0ubfz0 9536 1fv 9550 lbfzo0 9592 elfzonlteqm1 9621 fzo01 9627 fzo0to2pr 9629 fzo0to3tp 9630 flqge0nn0 9700 divfl0 9703 btwnzge0 9707 modqmulnn 9749 zmodfz 9753 modqid 9756 zmodid2 9759 q0mod 9762 modqmuladdnn0 9775 frecfzennn 9833 qexpclz 9976 facdiv 10146 bcval 10157 bcnn 10165 bcm1k 10168 ibcval5 10171 bcpasc 10174 4bc2eq6 10182 hashinfom 10186 rexfiuz 10422 qabsor 10508 nn0abscl 10518 nnabscl 10533 climz 10680 climaddc1 10717 climmulc2 10719 climsubc1 10720 climsubc2 10721 climlec2 10730 binomlem 10877 binom 10878 bcxmas 10883 arisum2 10893 explecnv 10899 ef0lem 10950 dvdsval2 11077 dvdsdc 11082 moddvds 11083 dvds0 11089 0dvds 11094 zdvdsdc 11095 dvdscmulr 11103 dvdsmulcr 11104 dvdslelemd 11122 dvdsabseq 11126 divconjdvds 11128 alzdvds 11133 fzo0dvdseq 11136 odd2np1lem 11150 gcdmndc 11218 gcdsupex 11227 gcdsupcl 11228 gcd0val 11230 gcddvds 11233 gcd0id 11248 gcdid0 11249 gcdid 11255 bezoutlema 11266 bezoutlemb 11267 bezoutlembi 11272 dfgcd3 11277 dfgcd2 11281 gcdmultiplez 11288 dvdssq 11298 algcvgblem 11309 lcmmndc 11322 lcm0val 11325 dvdslcm 11329 lcmeq0 11331 lcmgcd 11338 lcmdvds 11339 lcmid 11340 3lcm2e6woprm 11346 6lcm4e12 11347 cncongr2 11364 sqrt2irrap 11436 dfphi2 11474 phiprmpw 11476 crth 11478 phimullem 11479 hashgcdeq 11482 |
Copyright terms: Public domain | W3C validator |