Theorem 0zd 9090

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

Syntax hints:   -> wi 4   e. wcel 1481   0cc0 7644   ZZcz 9078

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7738  ax-addrcl 7741  ax-rnegex 7753

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-neg 7960  df-z 9079

This theorem is referenced by:  fzctr  9941  fzosubel3  10004  frecfzennn  10230  frechashgf1o  10232  0tonninf  10243  1tonninf  10244  exp3val  10326  exp0  10328  bcval  10527  bccmpl  10532  bcval5  10541  bcpasc  10544  bccl  10545  hashcl  10559  hashfiv01gt1  10560  hashfz1  10561  hashen  10562  fihashneq0  10573  omgadd  10580  fihashdom  10581  fnfz0hash  10607  ffzo0hash  10609  fzomaxdiflem  10916  fsumzcl  11203  fisum0diag  11242  fisum0diag2  11248  binomlem  11284  binom1dif  11288  isumnn0nn  11294  expcnvre  11304  explecnv  11306  pwm1geoserap1  11309  geolim  11312  geolim2  11313  geo2sum  11315  geoisum  11318  geoisumr  11319  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  eftcl  11397  efval  11404  eff  11406  efcvg  11409  efcvgfsum  11410  reefcl  11411  ege2le3  11414  efcj  11416  efaddlem  11417  eftlub  11433  effsumlt  11435  efgt1p2  11438  efgt1p  11439  eflegeo  11444  eirraplem  11519  dvdsmod  11596  gcdn0gt0  11702  gcdaddm  11708  gcdmultipled  11717  bezoutlemle  11732  nn0seqcvgd  11758  alginv  11764  algcvg  11765  algcvga  11768  algfx  11769  eucalgval2  11770  eucalgcvga  11775  eucalg  11776  lcmcllem  11784  lcmid  11797  mulgcddvds  11811  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  phiprmpw  11934  ennnfonelemjn  11951  ennnfonelemh  11953  ennnfonelem0  11954  ennnfonelem1  11956  ennnfonelemom  11957  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemrn  11968  ennnfonelemnn0  11971  ctinfomlemom  11976  012of  13363  2o01f  13364  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423