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

Theorem 1zzd 10891
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 10890 . 2  |-  1  e.  ZZ
21a1i 11 1  |-  ( ph  ->  1  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   1c1 9482   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-z 10861
This theorem is referenced by:  elfz1b  11752  fzm1  11762  fzoss2  11830  fzo1fzo0n0  11841  elfznelfzo  11896  modnegd  12024  2submod  12030  sermono  12121  seqf1olem2  12129  bcp1nk  12377  climuni  13457  isercoll  13572  telfsumo  13698  fsumparts  13702  binomlem  13723  climcndslem2  13744  climcnds  13745  divcnv  13747  supcvg  13749  arisum  13753  trireciplem  13755  trirecip  13756  expcnv  13757  geo2sum  13764  geo2lim  13766  geoisum1  13770  geoisum1c  13771  mertenslem1  13775  mertenslem2  13776  fprodser  13838  fprodzcl  13843  ege2le3  13907  rpnnen2  14043  bitscmp  14172  hashdvds  14389  phiprmpw  14390  prmdiv  14399  odzdvds  14406  odzphi  14407  modprm1div  14408  iserodd  14443  pcid  14480  pcmptcl  14494  pockthlem  14507  prmreclem4  14521  prmreclem6  14523  vdwapun  14576  gsumpr12val  16108  mulgpropd  16374  sylow1lem1  16817  sylow3lem6  16851  pgpfac1lem2  17321  zringcyg  18701  mulgrhm2  18711  znunit  18775  znrrg  18777  cpmadugsumlemF  19544  lmcnp  19972  lmmo  20048  1stcelcls  20128  1stccnp  20129  1stckgenlem  20220  1stckgen  20221  clmvneg1  21757  clmmulg  21759  lmnn  21868  cmetcaulem  21893  iscmet2  21899  causs  21903  caubl  21912  iscmet3i  21916  ovolsf  22050  ovoliunlem1  22079  ovoliun  22082  ovoliun2  22083  ovolicc2lem2  22095  ovolicc2lem3  22096  ovolicc2lem4  22097  voliunlem2  22127  voliunlem3  22128  ioombl1lem4  22137  uniioombllem2  22158  uniioombllem3  22160  uniioombllem6  22163  vitalilem4  22186  itg1climres  22287  mbfi1fseqlem6  22293  mbfi1flimlem  22295  mbfmullem2  22297  itg2monolem1  22323  itg2i1fseq  22328  itg2i1fseq2  22329  itg2addlem  22331  plyeq0lem  22773  dvply1  22846  dvtaylp  22931  pserdvlem2  22989  pserdv2  22991  advlogexp  23204  logtayl  23209  logtaylsum  23210  logtayl2  23211  atantayl  23465  leibpilem2  23469  leibpi  23470  birthdaylem2  23480  dfef2  23498  divsqrtsumlem  23507  emcllem4  23526  emcllem6  23528  emcllem7  23529  wilthlem1  23540  wilthlem2  23541  basellem6  23557  basellem7  23558  basellem8  23559  basellem9  23560  mersenne  23700  perfectlem1  23702  perfectlem2  23703  lgslem1  23769  lgsqrlem1  23814  lgseisenlem1  23822  lgsquad2lem1  23831  lgsquad3  23834  m1lgs  23835  2sqlem11  23848  dchrisumlema  23871  dchrisumlem3  23874  dchrmusum2  23877  dchrvmasumiflem1  23884  dchrvmaeq0  23887  dchrisum0re  23896  dchrisum0lem1b  23898  dchrisum0lem2a  23900  logdivsum  23916  pntrlog2bndlem1  23960  pntpbnd2  23970  axlowdimlem6  24452  axlowdim  24466  redwlk  24810  wwlkextproplem1  24943  wwlkextproplem2  24944  clwlkfclwwlk  25046  nvlmle  25800  minvecolem3  25990  minvecolem4b  25992  minvecolem4  25994  h2hcau  26094  h2hlm  26095  hlimadd  26308  hhsscms  26393  occllem  26419  nlelchi  27178  opsqrlem4  27260  hmopidmchi  27268  fzspl  27832  fzsplit3  27833  archirngz  27967  archiabllem1a  27969  rge0scvg  28166  lmxrge0  28169  lmdvg  28170  qqhval2lem  28196  esumfsupre  28300  esumpcvgval  28307  esumcvg  28315  eulerpartlems  28563  fiblem  28601  ballotlemfp1  28694  ballotlemimin  28708  ballotlemic  28709  ballotlem1c  28710  ballotlemsdom  28714  ballotlemsel1i  28715  ballotlemsima  28718  ballotlemfrceq  28731  ballotlemfrcn0  28732  zetacvg  28821  lgamgulmlem4  28838  lgamgulmlem6  28840  lgamgulm2  28842  lgamcvg2  28861  gamcvg  28862  regamcl  28867  relgamcl  28868  sinccvg  29303  circum  29304  divcnvlin  29359  iprodgam  29366  risefacval2  29373  fallfacval2  29374  binomfallfaclem2  29403  faclimlem2  29410  faclim  29412  iprodfac  29413  faclim2  29414  bpolydiflem  30044  lmclim2  30491  geomcau  30492  heibor1lem  30545  heibor1  30546  bfplem1  30558  bfplem2  30559  rrncmslem  30568  rrncms  30569  fzsplit1nn0  30926  eldioph2lem1  30932  pellexlem6  31009  rmspecnonsq  31082  jm2.22  31176  jm2.23  31177  jm2.25  31180  dvradcnv2  31493  binomcxplemnn0  31495  binomcxplemrat  31496  binomcxplemnotnn0  31502  oddfl  31699  fmuldfeq  31816  fmul01lt1lem2  31818  fmul01lt1  31819  clim1fr1  31846  sumnnodd  31875  dvnmul  31979  stoweidlem3  32024  stoweidlem7  32028  stoweidlem11  32032  stoweidlem14  32035  stoweidlem20  32041  stoweidlem26  32047  stoweidlem34  32055  stoweidlem51  32072  wallispilem5  32090  wallispi  32091  stirlinglem1  32095  stirlinglem5  32099  stirlinglem7  32101  stirlinglem8  32102  stirlinglem10  32104  stirlinglem12  32106  stirlinglem13  32107  stirlinglem14  32108  stirlinglem15  32109  stirlingr  32111  fourierdlem4  32132  fourierdlem11  32139  fourierdlem26  32154  fourierdlem41  32169  fourierdlem42  32170  fourierdlem48  32176  fourierdlem49  32177  fourierdlem79  32207  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  etransclem15  32271  etransclem28  32284  etransclem35  32291  etransclem38  32294  etransclem44  32300  etransclem48  32304  2even  32993  nn0o1gt2  33391  fldivexpfllog2  33440  nnlog2ge0lt1  33441  logbpw2m1  33442  blenpw2m1  33454  blennnt2  33464  nnolog2flm1  33465  blennn0e2  33469  digexp  33482  dignn0flhalflem1  33490  dignn0flhalflem2  33491
  Copyright terms: Public domain W3C validator