Theorem 1zzd 9481

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

Syntax hints:   -> wi 4   e. wcel 2200   1c1 8008   ZZcz 9454

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-addcom 8107  ax-addass 8109  ax-distr 8111  ax-i2m1 8112  ax-0lt1 8113  ax-0id 8115  ax-rnegex 8116  ax-cnre 8118  ax-pre-ltirr 8119  ax-pre-ltwlin 8120  ax-pre-lttrn 8121  ax-pre-ltadd 8123

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8191  df-mnf 8192  df-xr 8193  df-ltxr 8194  df-le 8195  df-sub 8327  df-neg 8328  df-inn 9119  df-z 9455

This theorem is referenced by:  uzm1  9761  elfz1b  10294  fzm1  10304  fzoss2  10378  fzo1fzo0n0  10391  nninfdcex  10465  qnegmod  10599  addmodid  10602  q2submod  10615  ser3mono  10717  seq3f1olemqsumkj  10741  seqf1oglem2  10750  exp3vallem  10770  exp3val  10771  exp1  10775  facnn  10957  fac0  10958  fac1  10959  bcp1nk  10992  hashfiv01gt1  11012  fseq1hash  11031  hashfz  11051  zfz1isolemsplit  11068  seq3coll  11072  wrdind  11262  wrd2ind  11263  resqrexlemf  11526  resqrexlemf1  11527  resqrexlemnmsq  11536  resqrexlemcvg  11538  climuni  11812  climrecvg1n  11867  climcvg1nlem  11868  nnf1o  11895  summodclem2a  11900  summodclem2  11901  summodc  11902  zsumdc  11903  fsum3  11906  sum0  11907  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  sumsnf  11928  fsummulc2  11967  telfsumo  11985  fsumparts  11989  binomlem  12002  divcnv  12016  arisum  12017  arisum2  12018  trireciplem  12019  trirecip  12020  expcnvap0  12021  expcnv  12023  geo2sum  12033  geo2lim  12035  geoisum1  12038  geoisum1c  12039  cvgratnnlemseq  12045  cvgratnnlemsumlt  12047  cvgratnnlemrate  12049  cvgratnn  12050  cvgratz  12051  mertenslemub  12053  mertenslemi1  12054  mertenslem2  12055  prodmodclem3  12094  prodmodclem2a  12095  prodmodclem2  12096  zproddc  12098  fprodseq  12102  fprodssdc  12109  prodsnf  12111  fprodzcl  12128  fprodfac  12134  ege2le3  12190  modm1div  12319  nn0o1gt2  12424  bitsfzolem  12473  bitscmp  12477  gcdsupex  12486  gcdsupcl  12487  gcdaddm  12513  nnmindc  12563  nnminle  12564  uzwodc  12566  lcmval  12593  lcmcllem  12597  lcmledvds  12600  isprm3  12648  isprm4  12649  prmind2  12650  dvdsnprmd  12655  rpexp  12683  pw2dvds  12696  phivalfi  12742  phicl2  12744  hashdvds  12751  phiprmpw  12752  phimullem  12755  eulerthlemfi  12758  eulerthlemh  12761  eulerthlemth  12762  eulerth  12763  prmdiv  12765  dvdsfi  12769  hashgcdeq  12770  odzcllem  12773  odzdvds  12776  odzphi  12777  pcid  12855  pcmptcl  12873  pcmpt  12874  pcfac  12881  pcbc  12882  pockthlem  12887  infpnlem2  12891  1arith  12898  4sqlem11  12932  4sqlem13m  12934  4sqlem14  12935  4sqlem17  12938  4sqlem18  12939  nninfdclemf  13028  gsumpr12val  13441  mulgval  13667  mulgfng  13669  mulgnngsum  13672  mulg1  13674  mulgnnsubcl  13679  mulgpropdg  13709  mulgrhm  14581  mulgrhm2  14582  znunit  14631  znrrg  14632  lmtopcnp  14932  dvply1  15447  relogbval  15633  relogbzcl  15634  nnlogbexp  15641  wilthlem1  15662  mersenne  15679  perfectlem1  15681  perfectlem2  15682  lgslem1  15687  lgsval  15691  lgsfvalg  15692  lgscllem  15694  lgsval2lem  15697  lgsval4a  15709  lgsneg  15711  lgsdir2  15720  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  gausslemma2dlem1  15748  gausslemma2dlem4  15751  gausslemma2dlem6  15754  gausslemma2dlem7  15755  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgseisen  15761  lgsquadlemsfi  15762  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem1  15768  lgsquad3  15771  m1lgs  15772  2lgsoddprm  15800  cvgcmp2nlemabs  16430  cvgcmp2n  16431  trilpolemcl  16435  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  dceqnconst  16458  dcapnconst  16459  nconstwlpolemgt0  16462