Theorem 1zzd 9604

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

Assertion

Ref	Expression
1zzd	|- ( ph -> 1 e. ZZ )

Proof of Theorem 1zzd

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

Syntax hints:   -> wi 4   e. wcel 2203   1c1 8128   ZZcz 9577

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-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-z 9578

This theorem is referenced by:  uzm1  9885  elfz1b  10424  fzm1  10434  fzoss2  10508  fzo1fzo0n0  10522  nninfdcex  10597  qnegmod  10731  addmodid  10734  q2submod  10747  ser3mono  10849  seq3f1olemqsumkj  10873  seqf1oglem2  10882  exp3vallem  10902  exp3val  10903  exp1  10907  facnn  11089  fac0  11090  fac1  11091  bcp1nk  11124  hashfiv01gt1  11145  fseq1hash  11165  hashfz  11186  sseqn  11203  zfz1isolemsplit  11210  seq3coll  11214  wrdind  11414  wrd2ind  11415  resqrexlemf  11692  resqrexlemf1  11693  resqrexlemnmsq  11702  resqrexlemcvg  11704  climuni  11978  climrecvg1n  12033  climcvg1nlem  12034  nnf1o  12062  summodclem2a  12067  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  sum0  12074  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  sumsnf  12095  fsummulc2  12134  telfsumo  12152  fsumparts  12156  binomlem  12169  divcnv  12183  arisum  12184  arisum2  12185  trireciplem  12186  trirecip  12187  expcnvap0  12188  expcnv  12190  geo2sum  12200  geo2lim  12202  geoisum1  12205  geoisum1c  12206  cvgratnnlemseq  12212  cvgratnnlemsumlt  12214  cvgratnnlemrate  12216  cvgratnn  12217  cvgratz  12218  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  prodmodclem3  12261  prodmodclem2a  12262  prodmodclem2  12263  zproddc  12265  fprodseq  12269  fprodssdc  12276  prodsnf  12278  fprodzcl  12295  fprodfac  12301  ege2le3  12357  modm1div  12486  nn0o1gt2  12591  bitsfzolem  12640  bitscmp  12644  gcdsupex  12653  gcdsupcl  12654  gcdaddm  12680  nnmindc  12730  nnminle  12731  uzwodc  12733  lcmval  12760  lcmcllem  12764  lcmledvds  12767  isprm3  12815  isprm4  12816  prmind2  12817  dvdsnprmd  12822  rpexp  12850  pw2dvds  12863  phivalfi  12909  phicl2  12911  hashdvds  12918  phiprmpw  12919  phimullem  12922  eulerthlemfi  12925  eulerthlemh  12928  eulerthlemth  12929  eulerth  12930  prmdiv  12932  dvdsfi  12936  hashgcdeq  12937  odzcllem  12940  odzdvds  12943  odzphi  12944  pcid  13022  pcmptcl  13040  pcmpt  13041  pcfac  13048  pcbc  13049  pockthlem  13054  infpnlem2  13058  1arith  13065  4sqlem11  13099  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  nninfdclemf  13200  gsumpr12val  13613  mulgval  13839  mulgfng  13841  mulgnngsum  13844  mulg1  13846  mulgnnsubcl  13851  mulgpropdg  13881  mulgrhm  14757  mulgrhm2  14758  znunit  14807  znrrg  14808  lmtopcnp  15115  dvply1  15630  relogbval  15816  relogbzcl  15817  nnlogbexp  15824  wilthlem1  15848  mersenne  15865  perfectlem1  15867  perfectlem2  15868  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgscllem  15880  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsdir2  15906  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  gausslemma2dlem1  15934  gausslemma2dlem4  15937  gausslemma2dlem6  15940  gausslemma2dlem7  15941  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlemsfi  15948  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad3  15957  m1lgs  15958  2lgsoddprm  15986  clwwlkccatlem  16395  clwwlknonex2lem2  16433  konigsberglem1  16483  cvgcmp2nlemabs  16816  cvgcmp2n  16817  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  dceqnconst  16846  dcapnconst  16847  nconstwlpolemgt0  16850  gfsumval  16862  gsumgfsum1  16863  gsumgfsumlem  16865  gsumgfsum  16866  gfsumsn  16867  gfsump1  16868