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

Theorem 1zzd 10957
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 10956 . 2  |-  1  e.  ZZ
21a1i 11 1  |-  ( ph  ->  1  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   1c1 9529   ZZcz 10926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-nn 10599  df-z 10927
This theorem is referenced by:  elfz1b  11851  fzm1  11861  fzoss2  11933  fzo1fzo0n0  11944  elfznelfzo  12000  negmod  12124  addmodid  12125  modnegd  12131  2submod  12137  sermono  12231  seqf1olem2  12239  bcp1nk  12488  climuni  13583  isercoll  13698  telfsumo  13829  fsumparts  13833  binomlem  13854  climcndslem2  13875  climcnds  13876  divcnv  13878  supcvg  13881  arisum  13885  trireciplem  13887  trirecip  13888  expcnv  13889  geo2sum  13896  geo2lim  13898  geoisum1  13902  geoisum1c  13903  mertenslem1  13907  mertenslem2  13908  fprodser  13970  fprodzcl  13975  risefacval2  14030  fallfacval2  14031  binomfallfaclem2  14060  bpolydiflem  14074  ege2le3  14111  rpnnen2  14245  bitscmp  14375  hashdvds  14681  phiprmpw  14682  prmdiv  14691  odzdvds  14698  odzphi  14699  modprm1div  14700  iserodd  14737  pcid  14774  pcmptcl  14788  pockthlem  14801  prmreclem4  14815  prmreclem6  14817  vdwapun  14876  prmdvdsprmo  14952  prmodvdslcmf  14957  prmdvdsprmorOLD  14967  prmgapprmo  14985  gsumpr12val  16469  mulgpropd  16735  sylow1lem1  17178  sylow3lem6  17212  pgpfac1lem2  17636  zringcyg  18984  mulgrhm2  18994  znunit  19058  znrrg  19060  cpmadugsumlemF  19824  lmcnp  20244  lmmo  20320  1stcelcls  20400  1stccnp  20401  1stckgenlem  20492  1stckgen  20493  clmvneg1  22008  clmmulg  22010  lmnn  22119  cmetcaulem  22144  iscmet2  22150  causs  22154  caubl  22163  iscmet3i  22167  ovolsf  22299  ovoliunlem1  22329  ovoliun  22332  ovoliun2  22333  ovolicc2lem2  22345  ovolicc2lem3  22346  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  voliunlem2  22378  voliunlem3  22379  ioombl1lem4  22388  uniioombllem2  22414  uniioombllem2OLD  22415  uniioombllem3  22417  uniioombllem6  22420  vitalilem4  22443  itg1climres  22546  mbfi1fseqlem6  22552  mbfi1flimlem  22554  mbfmullem2  22556  itg2monolem1  22582  itg2i1fseq  22587  itg2i1fseq2  22588  itg2addlem  22590  plyeq0lem  23029  dvply1  23102  dvtaylp  23187  pserdvlem2  23245  pserdv2  23247  advlogexp  23462  logtayl  23467  logtaylsum  23468  logtayl2  23469  atantayl  23725  leibpilem2  23729  leibpi  23730  birthdaylem2  23740  dfef2  23758  divsqrtsumlem  23767  emcllem4  23786  emcllem6  23788  emcllem7  23789  zetacvg  23802  lgamgulmlem4  23819  lgamgulmlem6  23821  lgamgulm2  23823  lgamcvg2  23842  gamcvg  23843  regamcl  23848  relgamcl  23849  wilthlem1  23855  wilthlem2  23856  basellem6  23872  basellem7  23873  basellem8  23874  basellem9  23875  mersenne  24015  perfectlem1  24017  perfectlem2  24018  lgslem1  24084  lgsqrlem1  24129  lgseisenlem1  24137  lgsquad2lem1  24146  lgsquad3  24149  m1lgs  24150  2sqlem11  24163  dchrisumlema  24186  dchrisumlem3  24189  dchrmusum2  24192  dchrvmasumiflem1  24199  dchrvmaeq0  24202  dchrisum0re  24211  dchrisum0lem1b  24213  dchrisum0lem2a  24215  logdivsum  24231  pntrlog2bndlem1  24275  pntpbnd2  24285  axlowdimlem6  24820  axlowdim  24834  redwlk  25178  wwlkextproplem1  25311  wwlkextproplem2  25312  clwlkfclwwlk  25414  nvlmle  26170  minvecolem3  26360  minvecolem4b  26362  minvecolem4  26364  h2hcau  26464  h2hlm  26465  hlimadd  26678  hhsscms  26762  occllem  26788  nlelchi  27546  opsqrlem4  27628  hmopidmchi  27636  fzspl  28201  fzsplit3  28203  fz1fzo0m1  28212  archirngz  28341  archiabllem1a  28343  smatrcl  28458  submateqlem1  28469  submateqlem2  28470  mdetlap  28494  rge0scvg  28591  lmxrge0  28594  lmdvg  28595  qqhval2lem  28621  esumfsupre  28728  esumpcvgval  28735  esumcvg  28743  eulerpartlems  29016  fiblem  29054  ballotlemfp1  29147  ballotlemimin  29161  ballotlemic  29162  ballotlem1c  29163  ballotlemsdom  29167  ballotlemsel1i  29168  ballotlemsima  29171  ballotlemfrceq  29184  ballotlemfrcn0  29185  sinccvg  30102  circum  30103  divcnvlin  30151  bcprod  30158  iprodgam  30162  faclimlem2  30164  faclim  30166  iprodfac  30167  faclim2  30168  fwddifnp1  30714  lmclim2  31791  geomcau  31792  heibor1lem  31845  heibor1  31846  bfplem1  31858  bfplem2  31859  rrncmslem  31868  rrncms  31869  fzsplit1nn0  35305  eldioph2lem1  35311  pellexlem6  35388  rmspecnonsq  35465  jm2.22  35560  jm2.23  35561  jm2.25  35564  dvradcnv2  36337  binomcxplemnn0  36339  binomcxplemrat  36340  binomcxplemnotnn0  36346  oddfl  37100  fmuldfeq  37237  fmul01lt1lem2  37239  fmul01lt1  37240  clim1fr1  37255  sumnnodd  37286  dvnmul  37391  stoweidlem3  37436  stoweidlem7  37440  stoweidlem11  37444  stoweidlem14  37447  stoweidlem20  37453  stoweidlem26  37459  stoweidlem34  37468  stoweidlem51  37485  wallispilem5  37504  wallispi  37505  stirlinglem1  37509  stirlinglem5  37513  stirlinglem7  37515  stirlinglem8  37516  stirlinglem10  37518  stirlinglem12  37520  stirlinglem13  37521  stirlinglem14  37522  stirlinglem15  37523  stirlingr  37525  fourierdlem4  37546  fourierdlem11  37553  fourierdlem26  37568  fourierdlem41  37583  fourierdlem42  37584  fourierdlem48  37590  fourierdlem49  37591  fourierdlem79  37621  fourierdlem97  37639  fourierdlem103  37645  fourierdlem104  37646  fourierdlem112  37654  sqwvfoura  37664  sqwvfourb  37665  fouriersw  37667  etransclem15  37685  etransclem28  37698  etransclem35  37705  etransclem38  37708  etransclem44  37714  etransclem48  37718  caragenunicl  37858  caratheodorylem2  37861  iccpartiltu  38139  iccpartgt  38144  perfectALTVlem2  38247  bgoldbtbndlem3  38305  2even  38704  nn0o1gt2  39101  fldivexpfllog2  39150  nnlog2ge0lt1  39151  logbpw2m1  39152  blenpw2m1  39164  blennnt2  39174  nnolog2flm1  39175  blennn0e2  39179  digexp  39192  dignn0flhalflem1  39200  dignn0flhalflem2  39201
  Copyright terms: Public domain W3C validator