![]() |
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 7690 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqid 2115 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | 3mix1i 1136 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | elz 8960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | mpbir2an 909 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-1re 7639 ax-addrcl 7642 ax-rnegex 7654 |
This theorem depends on definitions: df-bi 116 df-3or 946 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-rab 2399 df-v 2659 df-un 3041 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-br 3896 df-iota 5046 df-fv 5089 df-ov 5731 df-neg 7859 df-z 8959 |
This theorem is referenced by: 0zd 8970 nn0ssz 8976 znegcl 8989 zgt0ge1 9016 nn0n0n1ge2b 9034 nn0lt10b 9035 nnm1ge0 9041 gtndiv 9050 msqznn 9055 zeo 9060 nn0ind 9069 fnn0ind 9071 nn0uz 9262 1eluzge0 9271 eqreznegel 9308 qreccl 9336 qdivcl 9337 irrmul 9341 fz10 9719 fz01en 9726 fzpreddisj 9744 fzshftral 9781 fznn0 9786 fz1ssfz0 9790 fz0tp 9794 elfz0ubfz0 9795 1fv 9809 lbfzo0 9851 elfzonlteqm1 9880 fzo01 9886 fzo0to2pr 9888 fzo0to3tp 9889 flqge0nn0 9959 divfl0 9962 btwnzge0 9966 modqmulnn 10008 zmodfz 10012 modqid 10015 zmodid2 10018 q0mod 10021 modqmuladdnn0 10034 frecfzennn 10092 qexpclz 10207 facdiv 10377 bcval 10388 bcnn 10396 bcm1k 10399 bcval5 10402 bcpasc 10405 4bc2eq6 10413 hashinfom 10417 rexfiuz 10653 qabsor 10739 nn0abscl 10749 nnabscl 10764 climz 10953 climaddc1 10990 climmulc2 10992 climsubc1 10993 climsubc2 10994 climlec2 11002 binomlem 11144 binom 11145 bcxmas 11150 arisum2 11160 explecnv 11166 ef0lem 11217 dvdsval2 11344 dvdsdc 11349 moddvds 11350 dvds0 11356 0dvds 11361 zdvdsdc 11362 dvdscmulr 11370 dvdsmulcr 11371 dvdslelemd 11389 dvdsabseq 11393 divconjdvds 11395 alzdvds 11400 fzo0dvdseq 11403 odd2np1lem 11417 gcdmndc 11485 gcdsupex 11494 gcdsupcl 11495 gcd0val 11497 gcddvds 11500 gcd0id 11515 gcdid0 11516 gcdid 11522 bezoutlema 11533 bezoutlemb 11534 bezoutlembi 11539 dfgcd3 11544 dfgcd2 11548 gcdmultiplez 11555 dvdssq 11565 algcvgblem 11576 lcmmndc 11589 lcm0val 11592 dvdslcm 11596 lcmeq0 11598 lcmgcd 11605 lcmdvds 11606 lcmid 11607 3lcm2e6woprm 11613 6lcm4e12 11614 cncongr2 11631 sqrt2irrap 11703 dfphi2 11741 phiprmpw 11743 crth 11745 phimullem 11746 hashgcdeq 11749 ennnfonelemjn 11760 ennnfonelem1 11765 |
Copyright terms: Public domain | W3C validator |