![]() |
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 9089 | . 2 ⊢ 0 ∈ ℤ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1481 0cc0 7644 ℤcz 9078 |
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 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-1re 7738 ax-addrcl 7741 ax-rnegex 7753 |
This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 df-rex 2423 df-rab 2426 df-v 2691 df-un 3080 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-br 3938 df-iota 5096 df-fv 5139 df-ov 5785 df-neg 7960 df-z 9079 |
This theorem is referenced by: fzctr 9941 fzosubel3 10004 frecfzennn 10230 frechashgf1o 10232 0tonninf 10243 1tonninf 10244 exp3val 10326 exp0 10328 bcval 10527 bccmpl 10532 bcval5 10541 bcpasc 10544 bccl 10545 hashcl 10559 hashfiv01gt1 10560 hashfz1 10561 hashen 10562 fihashneq0 10573 omgadd 10580 fihashdom 10581 fnfz0hash 10607 ffzo0hash 10609 fzomaxdiflem 10916 fsumzcl 11203 fisum0diag 11242 fisum0diag2 11248 binomlem 11284 binom1dif 11288 isumnn0nn 11294 expcnvre 11304 explecnv 11306 pwm1geoserap1 11309 geolim 11312 geolim2 11313 geo2sum 11315 geoisum 11318 geoisumr 11319 mertenslemub 11335 mertenslemi1 11336 mertenslem2 11337 mertensabs 11338 eftcl 11397 efval 11404 eff 11406 efcvg 11409 efcvgfsum 11410 reefcl 11411 ege2le3 11414 efcj 11416 efaddlem 11417 eftlub 11433 effsumlt 11435 efgt1p2 11438 efgt1p 11439 eflegeo 11444 eirraplem 11519 dvdsmod 11596 gcdn0gt0 11702 gcdaddm 11708 gcdmultipled 11717 bezoutlemle 11732 nn0seqcvgd 11758 alginv 11764 algcvg 11765 algcvga 11768 algfx 11769 eucalgval2 11770 eucalgcvga 11775 eucalg 11776 lcmcllem 11784 lcmid 11797 mulgcddvds 11811 divgcdcoprmex 11819 cncongr1 11820 cncongr2 11821 phiprmpw 11934 ennnfonelemjn 11951 ennnfonelemh 11953 ennnfonelem0 11954 ennnfonelem1 11956 ennnfonelemom 11957 ennnfonelemkh 11961 ennnfonelemhf1o 11962 ennnfonelemex 11963 ennnfonelemrn 11968 ennnfonelemnn0 11971 ctinfomlemom 11976 012of 13363 2o01f 13364 isomninnlem 13400 iswomninnlem 13417 ismkvnnlem 13419 dceqnconst 13423 |
Copyright terms: Public domain | W3C validator |