Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0zd | GIF version |
Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0zd | ⊢ (𝜑 → 0 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z 9065 | . 2 ⊢ 0 ∈ ℤ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 0cc0 7620 ℤcz 9054 |
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 2121 ax-1re 7714 ax-addrcl 7717 ax-rnegex 7729 |
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 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-rab 2425 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-iota 5088 df-fv 5131 df-ov 5777 df-neg 7936 df-z 9055 |
This theorem is referenced by: fzctr 9910 fzosubel3 9973 frecfzennn 10199 frechashgf1o 10201 0tonninf 10212 1tonninf 10213 exp3val 10295 exp0 10297 bcval 10495 bccmpl 10500 bcval5 10509 bcpasc 10512 bccl 10513 hashcl 10527 hashfiv01gt1 10528 hashfz1 10529 hashen 10530 fihashneq0 10541 omgadd 10548 fihashdom 10549 fnfz0hash 10575 ffzo0hash 10577 fzomaxdiflem 10884 fsumzcl 11171 fisum0diag 11210 fisum0diag2 11216 binomlem 11252 binom1dif 11256 isumnn0nn 11262 expcnvre 11272 explecnv 11274 pwm1geoserap1 11277 geolim 11280 geolim2 11281 geo2sum 11283 geoisum 11286 geoisumr 11287 mertenslemub 11303 mertenslemi1 11304 mertenslem2 11305 mertensabs 11306 eftcl 11360 efval 11367 eff 11369 efcvg 11372 efcvgfsum 11373 reefcl 11374 ege2le3 11377 efcj 11379 efaddlem 11380 eftlub 11396 effsumlt 11398 efgt1p2 11401 efgt1p 11402 eflegeo 11408 eirraplem 11483 dvdsmod 11560 gcdn0gt0 11666 gcdaddm 11672 gcdmultipled 11681 bezoutlemle 11696 nn0seqcvgd 11722 alginv 11728 algcvg 11729 algcvga 11732 algfx 11733 eucalgval2 11734 eucalgcvga 11739 eucalg 11740 lcmcllem 11748 lcmid 11761 mulgcddvds 11775 divgcdcoprmex 11783 cncongr1 11784 cncongr2 11785 phiprmpw 11898 ennnfonelemjn 11915 ennnfonelemh 11917 ennnfonelem0 11918 ennnfonelem1 11920 ennnfonelemom 11921 ennnfonelemkh 11925 ennnfonelemhf1o 11926 ennnfonelemex 11927 ennnfonelemrn 11932 ennnfonelemnn0 11935 ctinfomlemom 11940 isomninnlem 13225 |
Copyright terms: Public domain | W3C validator |