Theorem 0zd 8658

Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	|- ( ph -> 0 e. ZZ )

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 8657	. 2 |- 0 e. ZZ
2	1	a1i 9	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1434   0cc0 7253   ZZcz 8646

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