![]() |
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 8815 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-1re 7493 ax-addrcl 7496 ax-rnegex 7508 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-rab 2369 df-v 2622 df-un 3004 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-iota 4993 df-fv 5036 df-ov 5669 df-neg 7710 df-z 8805 |
This theorem is referenced by: fzctr 9598 fzosubel3 9661 frecfzennn 9887 frechashgf1o 9889 0tonninf 9899 1tonninf 9900 exp3val 10011 exp0 10013 bcval 10211 bccmpl 10216 ibcval5 10225 bcpasc 10228 bccl 10229 hashcl 10243 hashfiv01gt1 10244 hashfz1 10245 hashen 10246 fihashneq0 10257 omgadd 10264 fihashdom 10265 fnfz0hash 10291 ffzo0hash 10293 fzomaxdiflem 10599 fsumzcl 10850 fisum0diag 10889 fisum0diag2 10895 binomlem 10931 binom1dif 10935 isumnn0nn 10941 expcnvre 10951 explecnv 10953 pwm1geoserap1 10956 geolim 10959 geolim2 10960 geo2sum 10962 geoisum 10965 geoisumr 10966 mertenslemub 10982 mertenslemi1 10983 mertenslem2 10984 mertensabs 10985 eftcl 10998 efval 11005 eff 11007 efcvg 11010 efcvgfsum 11011 reefcl 11012 ege2le3 11015 efcj 11017 efaddlem 11018 eftlub 11034 effsumlt 11036 efgt1p2 11039 efgt1p 11040 eflegeo 11046 eirraplem 11118 dvdsmod 11195 gcdn0gt0 11301 gcdaddm 11307 bezoutlemle 11329 nn0seqcvgd 11355 alginv 11361 algcvg 11362 algcvga 11365 algfx 11366 eucalgval2 11367 eucalgcvga 11372 eucalg 11373 lcmcllem 11381 lcmid 11394 mulgcddvds 11408 divgcdcoprmex 11416 cncongr1 11417 cncongr2 11418 phiprmpw 11530 |
Copyright terms: Public domain | W3C validator |