Theorem 1zzd 9253

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

Syntax hints:   -> wi 4   e. wcel 2146   1c1 7787   ZZcz 9226

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-addcom 7886  ax-addass 7888  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-0id 7894  ax-rnegex 7895  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-ltadd 7902

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-iota 5170  df-fun 5210  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-inn 8893  df-z 9227

This theorem is referenced by:  uzm1  9531  elfz1b  10060  fzm1  10070  fzoss2  10142  fzo1fzo0n0  10153  qnegmod  10339  addmodid  10342  q2submod  10355  ser3mono  10448  seq3f1olemqsumkj  10468  exp3vallem  10491  exp3val  10492  exp1  10496  facnn  10675  fac0  10676  fac1  10677  bcp1nk  10710  hashfiv01gt1  10730  fseq1hash  10749  hashfz  10769  zfz1isolemsplit  10786  seq3coll  10790  resqrexlemf  10984  resqrexlemf1  10985  resqrexlemnmsq  10994  resqrexlemcvg  10996  climuni  11269  climrecvg1n  11324  climcvg1nlem  11325  nnf1o  11352  summodclem2a  11357  summodclem2  11358  summodc  11359  zsumdc  11360  fsum3  11363  sum0  11364  fisumss  11368  fsumcl2lem  11374  fsumadd  11382  sumsnf  11385  fsummulc2  11424  telfsumo  11442  fsumparts  11446  binomlem  11459  divcnv  11473  arisum  11474  arisum2  11475  trireciplem  11476  trirecip  11477  expcnvap0  11478  expcnv  11480  geo2sum  11490  geo2lim  11492  geoisum1  11495  geoisum1c  11496  cvgratnnlemseq  11502  cvgratnnlemsumlt  11504  cvgratnnlemrate  11506  cvgratnn  11507  cvgratz  11508  mertenslemub  11510  mertenslemi1  11511  mertenslem2  11512  prodmodclem3  11551  prodmodclem2a  11552  prodmodclem2  11553  zproddc  11555  fprodseq  11559  fprodssdc  11566  prodsnf  11568  fprodzcl  11585  fprodfac  11591  ege2le3  11647  modm1div  11775  nn0o1gt2  11877  nninfdcex  11921  gcdsupex  11925  gcdsupcl  11926  gcdaddm  11952  nnmindc  12002  nnminle  12003  uzwodc  12005  lcmval  12030  lcmcllem  12034  lcmledvds  12037  isprm3  12085  isprm4  12086  prmind2  12087  dvdsnprmd  12092  rpexp  12120  pw2dvds  12133  phivalfi  12179  phicl2  12181  hashdvds  12188  phiprmpw  12189  phimullem  12192  eulerthlemfi  12195  eulerthlemh  12198  eulerthlemth  12199  eulerth  12200  prmdiv  12202  hashgcdeq  12206  phisum  12207  odzcllem  12209  odzdvds  12212  odzphi  12213  pcid  12290  pcmptcl  12307  pcmpt  12308  pcfac  12315  pcbc  12316  pockthlem  12321  infpnlem2  12325  1arith  12332  nninfdclemf  12417  mulgval  12847  mulgfng  12848  mulg1  12851  mulgnnsubcl  12856  mulgpropdg  12885  lmtopcnp  13321  relogbval  13940  relogbzcl  13941  nnlogbexp  13948  lgslem1  13972  lgsval  13976  lgsfvalg  13977  lgscllem  13979  lgsval2lem  13982  lgsval4a  13994  lgsneg  13996  lgsdir2  14005  lgsdir  14007  lgsdilem2  14008  lgsdi  14009  lgsne0  14010  cvgcmp2nlemabs  14341  cvgcmp2n  14342  trilpolemcl  14346  trilpolemisumle  14347  trilpolemeq1  14349  trilpolemlt1  14350  dceqnconst  14368  dcapnconst  14369  nconstwlpolemgt0  14372