![]() |
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 8657 |
. 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 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-1re 7342 ax-addrcl 7345 ax-rnegex 7357 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-rab 2362 df-v 2614 df-un 2988 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-iota 4934 df-fv 4977 df-ov 5594 df-neg 7559 df-z 8647 |
This theorem is referenced by: fzctr 9435 fzosubel3 9496 frecfzennn 9722 frechashgf1o 9724 0tonninf 9734 1tonninf 9735 exp0 9796 bcval 9992 bccmpl 9997 ibcval5 10006 bcpasc 10009 bccl 10010 hashcl 10024 hashfiv01gt1 10025 hashfz1 10026 hashen 10027 fihashneq0 10038 omgadd 10045 fihashdom 10046 fnfz0hash 10071 ffzo0hash 10073 fzomaxdiflem 10372 dvdsmod 10643 gcdn0gt0 10749 gcdaddm 10755 bezoutlemle 10777 nn0seqcvgd 10803 ialginv 10809 ialgcvg 10810 ialgcvga 10813 ialgfx 10814 eucalgval2 10815 eucialgcvga 10820 eucialg 10821 lcmcllem 10829 lcmid 10842 mulgcddvds 10856 divgcdcoprmex 10864 cncongr1 10865 cncongr2 10866 phiprmpw 10978 |
Copyright terms: Public domain | W3C validator |