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 9058 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cc0 7613 cz 9047 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-1re 7707 ax-addrcl 7710 ax-rnegex 7722 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ral 2419 df-rex 2420 df-rab 2423 df-v 2683 df-un 3070 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-br 3925 df-iota 5083 df-fv 5126 df-ov 5770 df-neg 7929 df-z 9048 |
This theorem is referenced by: fzctr 9903 fzosubel3 9966 frecfzennn 10192 frechashgf1o 10194 0tonninf 10205 1tonninf 10206 exp3val 10288 exp0 10290 bcval 10488 bccmpl 10493 bcval5 10502 bcpasc 10505 bccl 10506 hashcl 10520 hashfiv01gt1 10521 hashfz1 10522 hashen 10523 fihashneq0 10534 omgadd 10541 fihashdom 10542 fnfz0hash 10568 ffzo0hash 10570 fzomaxdiflem 10877 fsumzcl 11164 fisum0diag 11203 fisum0diag2 11209 binomlem 11245 binom1dif 11249 isumnn0nn 11255 expcnvre 11265 explecnv 11267 pwm1geoserap1 11270 geolim 11273 geolim2 11274 geo2sum 11276 geoisum 11279 geoisumr 11280 mertenslemub 11296 mertenslemi1 11297 mertenslem2 11298 mertensabs 11299 eftcl 11349 efval 11356 eff 11358 efcvg 11361 efcvgfsum 11362 reefcl 11363 ege2le3 11366 efcj 11368 efaddlem 11369 eftlub 11385 effsumlt 11387 efgt1p2 11390 efgt1p 11391 eflegeo 11397 eirraplem 11472 dvdsmod 11549 gcdn0gt0 11655 gcdaddm 11661 gcdmultipled 11670 bezoutlemle 11685 nn0seqcvgd 11711 alginv 11717 algcvg 11718 algcvga 11721 algfx 11722 eucalgval2 11723 eucalgcvga 11728 eucalg 11729 lcmcllem 11737 lcmid 11750 mulgcddvds 11764 divgcdcoprmex 11772 cncongr1 11773 cncongr2 11774 phiprmpw 11887 ennnfonelemjn 11904 ennnfonelemh 11906 ennnfonelem0 11907 ennnfonelem1 11909 ennnfonelemom 11910 ennnfonelemkh 11914 ennnfonelemhf1o 11915 ennnfonelemex 11916 ennnfonelemrn 11921 ennnfonelemnn0 11924 ctinfomlemom 11929 isomninnlem 13214 |
Copyright terms: Public domain | W3C validator |