![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0zd | Unicode version |
Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0zd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z 9262 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-1re 7904 ax-addrcl 7907 ax-rnegex 7919 |
This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-un 3133 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-iota 5178 df-fv 5224 df-ov 5877 df-neg 8129 df-z 9252 |
This theorem is referenced by: fzctr 10130 fzosubel3 10193 frecfzennn 10423 frechashgf1o 10425 0tonninf 10436 1tonninf 10437 exp3val 10519 exp0 10521 bcval 10724 bccmpl 10729 bcval5 10738 bcpasc 10741 bccl 10742 hashcl 10756 hashfiv01gt1 10757 hashfz1 10758 hashen 10759 fihashneq0 10769 omgadd 10777 fihashdom 10778 fiubz 10804 fnfz0hash 10807 ffzo0hash 10809 fzomaxdiflem 11116 fsumzcl 11405 fisum0diag 11444 fisum0diag2 11450 binomlem 11486 binom1dif 11490 isumnn0nn 11496 expcnvre 11506 explecnv 11508 pwm1geoserap1 11511 geolim 11514 geolim2 11515 geo2sum 11517 geoisum 11520 geoisumr 11521 mertenslemub 11537 mertenslemi1 11538 mertenslem2 11539 mertensabs 11540 fprod0diagfz 11631 eftcl 11657 efval 11664 eff 11666 efcvg 11669 efcvgfsum 11670 reefcl 11671 ege2le3 11674 efcj 11676 efaddlem 11677 eftlub 11693 effsumlt 11695 efgt1p2 11698 efgt1p 11699 eflegeo 11704 eirraplem 11779 dvdsmodexp 11797 dvdsmod 11862 gcdn0gt0 11973 gcdaddm 11979 gcdmultipled 11988 bezoutlemle 12003 nn0seqcvgd 12035 alginv 12041 algcvg 12042 algcvga 12045 algfx 12046 eucalgval2 12047 eucalgcvga 12052 eucalg 12053 lcmcllem 12061 lcmid 12074 mulgcddvds 12088 divgcdcoprmex 12096 cncongr1 12097 cncongr2 12098 phiprmpw 12216 modprm0 12248 pcpremul 12287 pceu 12289 pcmul 12295 pcqmul 12297 pcge0 12306 pcdvdsb 12313 pcneg 12318 pcgcd1 12321 pc2dvds 12323 pcz 12325 dvdsprmpweqle 12330 qexpz 12344 ennnfonelemjn 12397 ennnfonelemh 12399 ennnfonelem0 12400 ennnfonelem1 12402 ennnfonelemom 12403 ennnfonelemkh 12407 ennnfonelemhf1o 12408 ennnfonelemex 12409 ennnfonelemrn 12414 ennnfonelemnn0 12417 ctinfomlemom 12422 mulgval 12940 mulgfng 12941 subgmulg 13001 lgsval 14298 lgsfvalg 14299 lgscllem 14301 lgsval2lem 14304 lgsneg1 14319 lgsne0 14332 012of 14627 2o01f 14628 isomninnlem 14660 iswomninnlem 14679 ismkvnnlem 14682 dceqnconst 14689 dcapnconst 14690 |
Copyright terms: Public domain | W3C validator |