![]() |
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 9266 | . 2 ⊢ 0 ∈ ℤ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 0cc0 7813 ℤcz 9255 |
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 7907 ax-addrcl 7910 ax-rnegex 7922 |
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 2741 df-un 3135 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-br 4006 df-iota 5180 df-fv 5226 df-ov 5880 df-neg 8133 df-z 9256 |
This theorem is referenced by: fzctr 10135 fzosubel3 10198 frecfzennn 10428 frechashgf1o 10430 0tonninf 10441 1tonninf 10442 exp3val 10524 exp0 10526 bcval 10731 bccmpl 10736 bcval5 10745 bcpasc 10748 bccl 10749 hashcl 10763 hashfiv01gt1 10764 hashfz1 10765 hashen 10766 fihashneq0 10776 omgadd 10784 fihashdom 10785 fiubz 10811 fnfz0hash 10814 ffzo0hash 10816 fzomaxdiflem 11123 fsumzcl 11412 fisum0diag 11451 fisum0diag2 11457 binomlem 11493 binom1dif 11497 isumnn0nn 11503 expcnvre 11513 explecnv 11515 pwm1geoserap1 11518 geolim 11521 geolim2 11522 geo2sum 11524 geoisum 11527 geoisumr 11528 mertenslemub 11544 mertenslemi1 11545 mertenslem2 11546 mertensabs 11547 fprod0diagfz 11638 eftcl 11664 efval 11671 eff 11673 efcvg 11676 efcvgfsum 11677 reefcl 11678 ege2le3 11681 efcj 11683 efaddlem 11684 eftlub 11700 effsumlt 11702 efgt1p2 11705 efgt1p 11706 eflegeo 11711 eirraplem 11786 dvdsmodexp 11804 dvdsmod 11870 gcdn0gt0 11981 gcdaddm 11987 gcdmultipled 11996 bezoutlemle 12011 nn0seqcvgd 12043 alginv 12049 algcvg 12050 algcvga 12053 algfx 12054 eucalgval2 12055 eucalgcvga 12060 eucalg 12061 lcmcllem 12069 lcmid 12082 mulgcddvds 12096 divgcdcoprmex 12104 cncongr1 12105 cncongr2 12106 phiprmpw 12224 modprm0 12256 pcpremul 12295 pceu 12297 pcmul 12303 pcqmul 12305 pcge0 12314 pcdvdsb 12321 pcneg 12326 pcgcd1 12329 pc2dvds 12331 pcz 12333 dvdsprmpweqle 12338 qexpz 12352 ennnfonelemjn 12405 ennnfonelemh 12407 ennnfonelem0 12408 ennnfonelem1 12410 ennnfonelemom 12411 ennnfonelemkh 12415 ennnfonelemhf1o 12416 ennnfonelemex 12417 ennnfonelemrn 12422 ennnfonelemnn0 12425 ctinfomlemom 12430 mulgval 12991 mulgfng 12992 subgmulg 13053 lgsval 14444 lgsfvalg 14445 lgscllem 14447 lgsval2lem 14450 lgsneg1 14465 lgsne0 14478 012of 14784 2o01f 14785 isomninnlem 14817 iswomninnlem 14836 ismkvnnlem 14839 dceqnconst 14846 dcapnconst 14847 |
Copyright terms: Public domain | W3C validator |