Theorem 0zd 9263

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 9262	. 2 |- 0 e. ZZ
2	1	a1i 9	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2148   0cc0 7810   ZZcz 9251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8129  df-z 9252

This theorem is referenced by:  fzctr  10130  fzosubel3  10193  frecfzennn  10423  frechashgf1o  10425  0tonninf  10436  1tonninf  10437  exp3val  10519  exp0  10521  bcval  10724  bccmpl  10729  bcval5  10738  bcpasc  10741  bccl  10742  hashcl  10756  hashfiv01gt1  10757  hashfz1  10758  hashen  10759  fihashneq0  10769  omgadd  10777  fihashdom  10778  fiubz  10804  fnfz0hash  10807  ffzo0hash  10809  fzomaxdiflem  11116  fsumzcl  11405  fisum0diag  11444  fisum0diag2  11450  binomlem  11486  binom1dif  11490  isumnn0nn  11496  expcnvre  11506  explecnv  11508  pwm1geoserap1  11511  geolim  11514  geolim2  11515  geo2sum  11517  geoisum  11520  geoisumr  11521  mertenslemub  11537  mertenslemi1  11538  mertenslem2  11539  mertensabs  11540  fprod0diagfz  11631  eftcl  11657  efval  11664  eff  11666  efcvg  11669  efcvgfsum  11670  reefcl  11671  ege2le3  11674  efcj  11676  efaddlem  11677  eftlub  11693  effsumlt  11695  efgt1p2  11698  efgt1p  11699  eflegeo  11704  eirraplem  11779  dvdsmodexp  11797  dvdsmod  11862  gcdn0gt0  11973  gcdaddm  11979  gcdmultipled  11988  bezoutlemle  12003  nn0seqcvgd  12035  alginv  12041  algcvg  12042  algcvga  12045  algfx  12046  eucalgval2  12047  eucalgcvga  12052  eucalg  12053  lcmcllem  12061  lcmid  12074  mulgcddvds  12088  divgcdcoprmex  12096  cncongr1  12097  cncongr2  12098  phiprmpw  12216  modprm0  12248  pcpremul  12287  pceu  12289  pcmul  12295  pcqmul  12297  pcge0  12306  pcdvdsb  12313  pcneg  12318  pcgcd1  12321  pc2dvds  12323  pcz  12325  dvdsprmpweqle  12330  qexpz  12344  ennnfonelemjn  12397  ennnfonelemh  12399  ennnfonelem0  12400  ennnfonelem1  12402  ennnfonelemom  12403  ennnfonelemkh  12407  ennnfonelemhf1o  12408  ennnfonelemex  12409  ennnfonelemrn  12414  ennnfonelemnn0  12417  ctinfomlemom  12422  mulgval  12940  mulgfng  12941  subgmulg  13001  lgsval  14298  lgsfvalg  14299  lgscllem  14301  lgsval2lem  14304  lgsneg1  14319  lgsne0  14332  012of  14627  2o01f  14628  isomninnlem  14660  iswomninnlem  14679  ismkvnnlem  14682  dceqnconst  14689  dcapnconst  14690