Theorem 1zzd 9434

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

Syntax hints:   -> wi 4   e. wcel 2178   1c1 7961   ZZcz 9407

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-distr 8064  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-cnre 8071  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-iota 5251  df-fun 5292  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-sub 8280  df-neg 8281  df-inn 9072  df-z 9408

This theorem is referenced by:  uzm1  9714  elfz1b  10247  fzm1  10257  fzoss2  10331  fzo1fzo0n0  10344  nninfdcex  10417  qnegmod  10551  addmodid  10554  q2submod  10567  ser3mono  10669  seq3f1olemqsumkj  10693  seqf1oglem2  10702  exp3vallem  10722  exp3val  10723  exp1  10727  facnn  10909  fac0  10910  fac1  10911  bcp1nk  10944  hashfiv01gt1  10964  fseq1hash  10983  hashfz  11003  zfz1isolemsplit  11020  seq3coll  11024  wrdind  11213  wrd2ind  11214  resqrexlemf  11433  resqrexlemf1  11434  resqrexlemnmsq  11443  resqrexlemcvg  11445  climuni  11719  climrecvg1n  11774  climcvg1nlem  11775  nnf1o  11802  summodclem2a  11807  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  sum0  11814  fisumss  11818  fsumcl2lem  11824  fsumadd  11832  sumsnf  11835  fsummulc2  11874  telfsumo  11892  fsumparts  11896  binomlem  11909  divcnv  11923  arisum  11924  arisum2  11925  trireciplem  11926  trirecip  11927  expcnvap0  11928  expcnv  11930  geo2sum  11940  geo2lim  11942  geoisum1  11945  geoisum1c  11946  cvgratnnlemseq  11952  cvgratnnlemsumlt  11954  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  prodmodclem3  12001  prodmodclem2a  12002  prodmodclem2  12003  zproddc  12005  fprodseq  12009  fprodssdc  12016  prodsnf  12018  fprodzcl  12035  fprodfac  12041  ege2le3  12097  modm1div  12226  nn0o1gt2  12331  bitsfzolem  12380  bitscmp  12384  gcdsupex  12393  gcdsupcl  12394  gcdaddm  12420  nnmindc  12470  nnminle  12471  uzwodc  12473  lcmval  12500  lcmcllem  12504  lcmledvds  12507  isprm3  12555  isprm4  12556  prmind2  12557  dvdsnprmd  12562  rpexp  12590  pw2dvds  12603  phivalfi  12649  phicl2  12651  hashdvds  12658  phiprmpw  12659  phimullem  12662  eulerthlemfi  12665  eulerthlemh  12668  eulerthlemth  12669  eulerth  12670  prmdiv  12672  dvdsfi  12676  hashgcdeq  12677  odzcllem  12680  odzdvds  12683  odzphi  12684  pcid  12762  pcmptcl  12780  pcmpt  12781  pcfac  12788  pcbc  12789  pockthlem  12794  infpnlem2  12798  1arith  12805  4sqlem11  12839  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  nninfdclemf  12935  gsumpr12val  13347  mulgval  13573  mulgfng  13575  mulgnngsum  13578  mulg1  13580  mulgnnsubcl  13585  mulgpropdg  13615  mulgrhm  14486  mulgrhm2  14487  znunit  14536  znrrg  14537  lmtopcnp  14837  dvply1  15352  relogbval  15538  relogbzcl  15539  nnlogbexp  15546  wilthlem1  15567  mersenne  15584  perfectlem1  15586  perfectlem2  15587  lgslem1  15592  lgsval  15596  lgsfvalg  15597  lgscllem  15599  lgsval2lem  15602  lgsval4a  15614  lgsneg  15616  lgsdir2  15625  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  gausslemma2dlem1  15653  gausslemma2dlem4  15656  gausslemma2dlem6  15659  gausslemma2dlem7  15660  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlemsfi  15667  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem1  15673  lgsquad3  15676  m1lgs  15677  2lgsoddprm  15705  cvgcmp2nlemabs  16173  cvgcmp2n  16174  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  dceqnconst  16201  dcapnconst  16202  nconstwlpolemgt0  16205