MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1zzd Structured version   Unicode version

Theorem 1zzd 10901
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
StepHypRef Expression
1 1z 10900 . 2  |-  1  e.  ZZ
21a1i 11 1  |-  ( ph  ->  1  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   1c1 9496   ZZcz 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10543  df-z 10871
This theorem is referenced by:  elfz1b  11757  fzoss2  11832  fzo1fzo0n0  11843  elfznelfzo  11894  modnegd  12021  2submod  12027  sermono  12118  seqf1olem2  12126  bcp1nk  12374  climuni  13354  isercoll  13469  telfsumo  13595  fsumparts  13599  binomlem  13620  climcndslem2  13641  climcnds  13642  divcnv  13644  supcvg  13646  arisum  13650  trireciplem  13652  trirecip  13653  expcnv  13654  geo2sum  13661  geo2lim  13663  geoisum1  13667  geoisum1c  13668  mertenslem1  13672  mertenslem2  13673  ege2le3  13703  rpnnen2  13836  bitscmp  13965  hashdvds  14182  phiprmpw  14183  prmdiv  14192  odzdvds  14199  odzphi  14200  modprm1div  14201  iserodd  14236  pcid  14273  pcmptcl  14287  pockthlem  14300  prmreclem4  14314  prmreclem6  14316  vdwapun  14369  gsumpr12val  15783  mulgpropd  16049  sylow1lem1  16492  sylow3lem6  16526  pgpfac1lem2  17000  zringcyg  18386  zcyg  18391  mulgrhm2  18406  mulgrhm2OLD  18409  znunit  18475  znrrg  18477  cpmadugsumlemF  19250  lmcnp  19678  lmmo  19754  1stcelcls  19835  1stccnp  19836  1stckgenlem  19927  1stckgen  19928  clmvneg1  21464  clmmulg  21466  lmnn  21575  cmetcaulem  21600  iscmet2  21606  causs  21610  caubl  21619  iscmet3i  21623  ovolsf  21757  ovoliunlem1  21786  ovoliun  21789  ovoliun2  21790  ovolicc2lem2  21802  ovolicc2lem3  21803  ovolicc2lem4  21804  voliunlem2  21834  voliunlem3  21835  ioombl1lem4  21844  uniioombllem2  21865  uniioombllem3  21867  uniioombllem6  21870  vitalilem4  21893  itg1climres  21994  mbfi1fseqlem6  22000  mbfi1flimlem  22002  mbfmullem2  22004  itg2monolem1  22030  itg2i1fseq  22035  itg2i1fseq2  22036  itg2addlem  22038  plyeq0lem  22480  dvply1  22552  dvtaylp  22637  pserdvlem2  22695  pserdv2  22697  advlogexp  22908  logtayl  22913  logtaylsum  22914  logtayl2  22915  atantayl  23140  leibpilem2  23144  leibpi  23145  birthdaylem2  23154  dfef2  23172  divsqrtsumlem  23181  emcllem4  23200  emcllem6  23202  emcllem7  23203  wilthlem1  23214  wilthlem2  23215  basellem6  23231  basellem7  23232  basellem8  23233  basellem9  23234  mersenne  23374  perfectlem1  23376  perfectlem2  23377  lgslem1  23443  lgsqrlem1  23488  lgseisenlem1  23496  lgsquad2lem1  23505  lgsquad3  23508  m1lgs  23509  2sqlem11  23522  dchrisumlema  23545  dchrisumlem3  23548  dchrmusum2  23551  dchrvmasumiflem1  23558  dchrvmaeq0  23561  dchrisum0re  23570  dchrisum0lem1b  23572  dchrisum0lem2a  23574  logdivsum  23590  pntrlog2bndlem1  23634  pntpbnd2  23644  axlowdimlem6  24122  axlowdim  24136  redwlk  24480  wwlkextproplem1  24613  wwlkextproplem2  24614  clwlkfclwwlk  24716  nvlmle  25474  minvecolem3  25664  minvecolem4b  25666  minvecolem4  25668  h2hcau  25768  h2hlm  25769  hlimadd  25982  hhsscms  26067  occllem  26093  nlelchi  26852  opsqrlem4  26934  hmopidmchi  26942  fzspl  27470  fzsplit3  27471  archirngz  27606  archiabllem1a  27608  rge0scvg  27804  lmxrge0  27807  lmdvg  27808  qqhval2lem  27835  esumfsupre  27950  esumpcvgval  27957  esumcvg  27965  eulerpartlems  28172  fiblem  28210  ballotlemfp1  28303  ballotlemimin  28317  ballotlemic  28318  ballotlem1c  28319  ballotlemsdom  28323  ballotlemsel1i  28324  ballotlemsima  28327  ballotlemfrceq  28340  ballotlemfrcn0  28341  zetacvg  28430  lgamgulmlem4  28447  lgamgulmlem6  28449  lgamgulm2  28451  lgamcvg2  28470  gamcvg  28471  regamcl  28476  relgamcl  28477  sinccvg  28912  circum  28913  divcnvlin  28993  fprodser  29056  fprodzcl  29061  iprodgam  29100  risefacval2  29107  fallfacval2  29108  binomfallfaclem2  29137  faclimlem2  29144  faclim  29146  iprodfac  29147  faclim2  29148  bpolydiflem  29791  lmclim2  30226  geomcau  30227  heibor1lem  30280  heibor1  30281  bfplem1  30293  bfplem2  30294  rrncmslem  30303  rrncms  30304  fzsplit1nn0  30662  eldioph2lem1  30668  pellexlem6  30745  rmspecnonsq  30818  jm2.22  30912  jm2.23  30913  jm2.25  30916  oddfl  31408  fmuldfeq  31505  fmul01lt1lem2  31507  fmul01lt1  31508  clim1fr1  31515  sumnnodd  31544  stoweidlem3  31674  stoweidlem7  31678  stoweidlem11  31682  stoweidlem14  31685  stoweidlem20  31691  stoweidlem26  31697  stoweidlem34  31705  stoweidlem51  31722  wallispilem5  31740  wallispi  31741  stirlinglem1  31745  stirlinglem5  31749  stirlinglem7  31751  stirlinglem8  31752  stirlinglem10  31754  stirlinglem12  31756  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  stirlingr  31761  fourierdlem4  31782  fourierdlem11  31789  fourierdlem26  31804  fourierdlem41  31819  fourierdlem42  31820  fourierdlem48  31826  fourierdlem49  31827  fourierdlem79  31857  fourierdlem97  31875  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  2even  32449
  Copyright terms: Public domain W3C validator