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 9033 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 cc0 7588 cz 9022 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-1re 7682 ax-addrcl 7685 ax-rnegex 7697 |
This theorem depends on definitions: df-bi 116 df-3or 948 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-rex 2399 df-rab 2402 df-v 2662 df-un 3045 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-iota 5058 df-fv 5101 df-ov 5745 df-neg 7904 df-z 9023 |
This theorem is referenced by: fzctr 9878 fzosubel3 9941 frecfzennn 10167 frechashgf1o 10169 0tonninf 10180 1tonninf 10181 exp3val 10263 exp0 10265 bcval 10463 bccmpl 10468 bcval5 10477 bcpasc 10480 bccl 10481 hashcl 10495 hashfiv01gt1 10496 hashfz1 10497 hashen 10498 fihashneq0 10509 omgadd 10516 fihashdom 10517 fnfz0hash 10543 ffzo0hash 10545 fzomaxdiflem 10852 fsumzcl 11139 fisum0diag 11178 fisum0diag2 11184 binomlem 11220 binom1dif 11224 isumnn0nn 11230 expcnvre 11240 explecnv 11242 pwm1geoserap1 11245 geolim 11248 geolim2 11249 geo2sum 11251 geoisum 11254 geoisumr 11255 mertenslemub 11271 mertenslemi1 11272 mertenslem2 11273 mertensabs 11274 eftcl 11287 efval 11294 eff 11296 efcvg 11299 efcvgfsum 11300 reefcl 11301 ege2le3 11304 efcj 11306 efaddlem 11307 eftlub 11323 effsumlt 11325 efgt1p2 11328 efgt1p 11329 eflegeo 11335 eirraplem 11410 dvdsmod 11487 gcdn0gt0 11593 gcdaddm 11599 gcdmultipled 11608 bezoutlemle 11623 nn0seqcvgd 11649 alginv 11655 algcvg 11656 algcvga 11659 algfx 11660 eucalgval2 11661 eucalgcvga 11666 eucalg 11667 lcmcllem 11675 lcmid 11688 mulgcddvds 11702 divgcdcoprmex 11710 cncongr1 11711 cncongr2 11712 phiprmpw 11825 ennnfonelemjn 11842 ennnfonelemh 11844 ennnfonelem0 11845 ennnfonelem1 11847 ennnfonelemom 11848 ennnfonelemkh 11852 ennnfonelemhf1o 11853 ennnfonelemex 11854 ennnfonelemrn 11859 ennnfonelemnn0 11862 ctinfomlemom 11867 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |