Theorem 1zzd 9399

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

Syntax hints:   -> wi 4   e. wcel 2176   1c1 7926   ZZcz 9372

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-cnex 8016  ax-resscn 8017  ax-1cn 8018  ax-1re 8019  ax-icn 8020  ax-addcl 8021  ax-addrcl 8022  ax-mulcl 8023  ax-addcom 8025  ax-addass 8027  ax-distr 8029  ax-i2m1 8030  ax-0lt1 8031  ax-0id 8033  ax-rnegex 8034  ax-cnre 8036  ax-pre-ltirr 8037  ax-pre-ltwlin 8038  ax-pre-lttrn 8039  ax-pre-ltadd 8041

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-nel 2472  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-iota 5232  df-fun 5273  df-fv 5279  df-riota 5899  df-ov 5947  df-oprab 5948  df-mpo 5949  df-pnf 8109  df-mnf 8110  df-xr 8111  df-ltxr 8112  df-le 8113  df-sub 8245  df-neg 8246  df-inn 9037  df-z 9373

This theorem is referenced by:  uzm1  9679  elfz1b  10212  fzm1  10222  fzoss2  10296  fzo1fzo0n0  10307  nninfdcex  10380  qnegmod  10514  addmodid  10517  q2submod  10530  ser3mono  10632  seq3f1olemqsumkj  10656  seqf1oglem2  10665  exp3vallem  10685  exp3val  10686  exp1  10690  facnn  10872  fac0  10873  fac1  10874  bcp1nk  10907  hashfiv01gt1  10927  fseq1hash  10946  hashfz  10966  zfz1isolemsplit  10983  seq3coll  10987  resqrexlemf  11318  resqrexlemf1  11319  resqrexlemnmsq  11328  resqrexlemcvg  11330  climuni  11604  climrecvg1n  11659  climcvg1nlem  11660  nnf1o  11687  summodclem2a  11692  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  sum0  11699  fisumss  11703  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  fsummulc2  11759  telfsumo  11777  fsumparts  11781  binomlem  11794  divcnv  11808  arisum  11809  arisum2  11810  trireciplem  11811  trirecip  11812  expcnvap0  11813  expcnv  11815  geo2sum  11825  geo2lim  11827  geoisum1  11830  geoisum1c  11831  cvgratnnlemseq  11837  cvgratnnlemsumlt  11839  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  prodmodclem3  11886  prodmodclem2a  11887  prodmodclem2  11888  zproddc  11890  fprodseq  11894  fprodssdc  11901  prodsnf  11903  fprodzcl  11920  fprodfac  11926  ege2le3  11982  modm1div  12111  nn0o1gt2  12216  bitsfzolem  12265  bitscmp  12269  gcdsupex  12278  gcdsupcl  12279  gcdaddm  12305  nnmindc  12355  nnminle  12356  uzwodc  12358  lcmval  12385  lcmcllem  12389  lcmledvds  12392  isprm3  12440  isprm4  12441  prmind2  12442  dvdsnprmd  12447  rpexp  12475  pw2dvds  12488  phivalfi  12534  phicl2  12536  hashdvds  12543  phiprmpw  12544  phimullem  12547  eulerthlemfi  12550  eulerthlemh  12553  eulerthlemth  12554  eulerth  12555  prmdiv  12557  dvdsfi  12561  hashgcdeq  12562  odzcllem  12565  odzdvds  12568  odzphi  12569  pcid  12647  pcmptcl  12665  pcmpt  12666  pcfac  12673  pcbc  12674  pockthlem  12679  infpnlem2  12683  1arith  12690  4sqlem11  12724  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  nninfdclemf  12820  gsumpr12val  13232  mulgval  13458  mulgfng  13460  mulgnngsum  13463  mulg1  13465  mulgnnsubcl  13470  mulgpropdg  13500  mulgrhm  14371  mulgrhm2  14372  znunit  14421  znrrg  14422  lmtopcnp  14722  dvply1  15237  relogbval  15423  relogbzcl  15424  nnlogbexp  15431  wilthlem1  15452  mersenne  15469  perfectlem1  15471  perfectlem2  15472  lgslem1  15477  lgsval  15481  lgsfvalg  15482  lgscllem  15484  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsdir2  15510  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  gausslemma2dlem1  15538  gausslemma2dlem4  15541  gausslemma2dlem6  15544  gausslemma2dlem7  15545  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlemsfi  15552  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad2lem1  15558  lgsquad3  15561  m1lgs  15562  2lgsoddprm  15590  cvgcmp2nlemabs  15975  cvgcmp2n  15976  trilpolemcl  15980  trilpolemisumle  15981  trilpolemeq1  15983  trilpolemlt1  15984  dceqnconst  16003  dcapnconst  16004  nconstwlpolemgt0  16007