Theorem 1zzd 9315

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

Syntax hints:   -> wi 4   e. wcel 2160   1c1 7847   ZZcz 9288

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557  ax-cnex 7937  ax-resscn 7938  ax-1cn 7939  ax-1re 7940  ax-icn 7941  ax-addcl 7942  ax-addrcl 7943  ax-mulcl 7944  ax-addcom 7946  ax-addass 7948  ax-distr 7950  ax-i2m1 7951  ax-0lt1 7952  ax-0id 7954  ax-rnegex 7955  ax-cnre 7957  ax-pre-ltirr 7958  ax-pre-ltwlin 7959  ax-pre-lttrn 7960  ax-pre-ltadd 7962

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-int 3863  df-br 4022  df-opab 4083  df-id 4314  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-iota 5199  df-fun 5240  df-fv 5246  df-riota 5855  df-ov 5903  df-oprab 5904  df-mpo 5905  df-pnf 8029  df-mnf 8030  df-xr 8031  df-ltxr 8032  df-le 8033  df-sub 8165  df-neg 8166  df-inn 8955  df-z 9289

This theorem is referenced by:  uzm1  9594  elfz1b  10126  fzm1  10136  fzoss2  10208  fzo1fzo0n0  10219  qnegmod  10406  addmodid  10409  q2submod  10422  ser3mono  10517  seq3f1olemqsumkj  10537  exp3vallem  10561  exp3val  10562  exp1  10566  facnn  10748  fac0  10749  fac1  10750  bcp1nk  10783  hashfiv01gt1  10803  fseq1hash  10822  hashfz  10842  zfz1isolemsplit  10859  seq3coll  10863  resqrexlemf  11057  resqrexlemf1  11058  resqrexlemnmsq  11067  resqrexlemcvg  11069  climuni  11342  climrecvg1n  11397  climcvg1nlem  11398  nnf1o  11425  summodclem2a  11430  summodclem2  11431  summodc  11432  zsumdc  11433  fsum3  11436  sum0  11437  fisumss  11441  fsumcl2lem  11447  fsumadd  11455  sumsnf  11458  fsummulc2  11497  telfsumo  11515  fsumparts  11519  binomlem  11532  divcnv  11546  arisum  11547  arisum2  11548  trireciplem  11549  trirecip  11550  expcnvap0  11551  expcnv  11553  geo2sum  11563  geo2lim  11565  geoisum1  11568  geoisum1c  11569  cvgratnnlemseq  11575  cvgratnnlemsumlt  11577  cvgratnnlemrate  11579  cvgratnn  11580  cvgratz  11581  mertenslemub  11583  mertenslemi1  11584  mertenslem2  11585  prodmodclem3  11624  prodmodclem2a  11625  prodmodclem2  11626  zproddc  11628  fprodseq  11632  fprodssdc  11639  prodsnf  11641  fprodzcl  11658  fprodfac  11664  ege2le3  11720  modm1div  11848  nn0o1gt2  11951  nninfdcex  11995  gcdsupex  11999  gcdsupcl  12000  gcdaddm  12026  nnmindc  12076  nnminle  12077  uzwodc  12079  lcmval  12106  lcmcllem  12110  lcmledvds  12113  isprm3  12161  isprm4  12162  prmind2  12163  dvdsnprmd  12168  rpexp  12196  pw2dvds  12209  phivalfi  12255  phicl2  12257  hashdvds  12264  phiprmpw  12265  phimullem  12268  eulerthlemfi  12271  eulerthlemh  12274  eulerthlemth  12275  eulerth  12276  prmdiv  12278  hashgcdeq  12282  phisum  12283  odzcllem  12285  odzdvds  12288  odzphi  12289  pcid  12367  pcmptcl  12385  pcmpt  12386  pcfac  12393  pcbc  12394  pockthlem  12399  infpnlem2  12403  1arith  12410  4sqlem11  12444  4sqlem13m  12446  4sqlem14  12447  4sqlem17  12450  4sqlem18  12451  nninfdclemf  12511  gsumpr12val  12886  mulgval  13087  mulgfng  13089  mulgnngsum  13092  mulg1  13094  mulgnnsubcl  13099  mulgpropdg  13129  mulgrhm  13932  mulgrhm2  13933  lmtopcnp  14235  relogbval  14854  relogbzcl  14855  nnlogbexp  14862  wilthlem1  14883  lgslem1  14887  lgsval  14891  lgsfvalg  14892  lgscllem  14894  lgsval2lem  14897  lgsval4a  14909  lgsneg  14911  lgsdir2  14920  lgsdir  14922  lgsdilem2  14923  lgsdi  14924  lgsne0  14925  lgseisenlem1  14936  lgseisenlem2  14937  m1lgs  14938  cvgcmp2nlemabs  15268  cvgcmp2n  15269  trilpolemcl  15273  trilpolemisumle  15274  trilpolemeq1  15276  trilpolemlt1  15277  dceqnconst  15296  dcapnconst  15297  nconstwlpolemgt0  15300