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

Theorem 1zzd 10968
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 10967 . 2  |-  1  e.  ZZ
21a1i 11 1  |-  ( ph  ->  1  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   1c1 9540   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-z 10938
This theorem is referenced by:  elfz1b  11864  fzm1  11874  fzoss2  11946  fzo1fzo0n0  11957  fz1fzo0m1  11963  elfznelfzo  12014  negmod  12138  addmodid  12139  modnegd  12145  2submod  12151  sermono  12245  seqf1olem2  12253  bcp1nk  12502  climuni  13616  isercoll  13731  telfsumo  13862  fsumparts  13866  binomlem  13887  climcndslem2  13908  climcnds  13909  divcnv  13911  supcvg  13914  arisum  13918  trireciplem  13920  trirecip  13921  expcnv  13922  geo2sum  13929  geo2lim  13931  geoisum1  13935  geoisum1c  13936  mertenslem1  13940  mertenslem2  13941  fprodser  14003  fprodzcl  14008  risefacval2  14063  fallfacval2  14064  binomfallfaclem2  14093  bpolydiflem  14107  ege2le3  14144  rpnnen2  14278  bitscmp  14412  hashdvds  14723  phiprmpw  14724  prmdiv  14733  odzdvds  14740  odzphi  14741  odzdvdsOLD  14746  odzphiOLD  14747  modprm1div  14748  iserodd  14785  pcid  14822  pcmptcl  14836  pockthlem  14849  prmreclem4  14863  prmreclem6  14865  vdwapun  14924  prmdvdsprmo  15000  prmodvdslcmf  15005  prmdvdsprmorOLD  15015  prmgapprmo  15033  gsumpr12val  16525  mulgpropd  16791  sylow1lem1  17250  sylow3lem6  17284  pgpfac1lem2  17708  zringcyg  19060  mulgrhm2  19070  znunit  19134  znrrg  19136  cpmadugsumlemF  19900  lmcnp  20320  lmmo  20396  1stcelcls  20476  1stccnp  20477  1stckgenlem  20568  1stckgen  20569  clmvneg1  22122  clmmulg  22124  lmnn  22233  cmetcaulem  22258  iscmet2  22264  causs  22268  caubl  22277  iscmet3i  22281  ovolsf  22425  ovoliunlem1  22455  ovoliun  22458  ovoliun2  22459  ovolicc2lem2  22471  ovolicc2lem3  22472  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  voliunlem2  22504  voliunlem3  22505  ioombl1lem4  22514  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3  22543  uniioombllem6  22546  vitalilem4  22569  itg1climres  22672  mbfi1fseqlem6  22678  mbfi1flimlem  22680  mbfmullem2  22682  itg2monolem1  22708  itg2i1fseq  22713  itg2i1fseq2  22714  itg2addlem  22716  plyeq0lem  23164  dvply1  23237  dvtaylp  23325  pserdvlem2  23383  pserdv2  23385  advlogexp  23600  logtayl  23605  logtaylsum  23606  logtayl2  23607  atantayl  23863  leibpilem2  23867  leibpi  23868  birthdaylem2  23878  dfef2  23896  divsqrtsumlem  23905  emcllem4  23924  emcllem6  23926  emcllem7  23927  zetacvg  23940  lgamgulmlem4  23957  lgamgulmlem6  23959  lgamgulm2  23961  lgamcvg2  23980  gamcvg  23981  regamcl  23986  relgamcl  23987  wilthlem1  23993  wilthlem2  23994  basellem6  24012  basellem7  24013  basellem8  24014  basellem9  24015  mersenne  24155  perfectlem1  24157  perfectlem2  24158  lgslem1  24224  lgsqrlem1  24269  lgseisenlem1  24277  lgsquad2lem1  24286  lgsquad3  24289  m1lgs  24290  2sqlem11  24303  dchrisumlema  24326  dchrisumlem3  24329  dchrmusum2  24332  dchrvmasumiflem1  24339  dchrvmaeq0  24342  dchrisum0re  24351  dchrisum0lem1b  24353  dchrisum0lem2a  24355  logdivsum  24371  pntrlog2bndlem1  24415  pntpbnd2  24425  axlowdimlem6  24977  axlowdim  24991  redwlk  25336  wwlkextproplem1  25469  wwlkextproplem2  25470  clwlkfclwwlk  25572  nvlmle  26328  minvecolem3  26518  minvecolem4b  26520  minvecolem4  26522  minvecolem3OLD  26528  minvecolem4bOLD  26530  minvecolem4OLD  26532  h2hcau  26632  h2hlm  26633  hlimadd  26846  hhsscms  26930  occllem  26956  nlelchi  27714  opsqrlem4  27796  hmopidmchi  27804  fzspl  28368  fzsplit3  28370  archirngz  28506  archiabllem1a  28508  smatrcl  28622  submateqlem1  28633  submateqlem2  28634  mdetlap  28658  rge0scvg  28755  lmxrge0  28758  lmdvg  28759  qqhval2lem  28785  esumfsupre  28892  esumpcvgval  28899  esumcvg  28907  eulerpartlems  29193  fiblem  29231  ballotlemfp1  29324  ballotlemimin  29338  ballotlemic  29339  ballotlem1c  29340  ballotlemsdom  29344  ballotlemsel1i  29345  ballotlemsima  29348  ballotlemfrceq  29361  ballotlemfrcn0  29362  ballotlemiminOLD  29376  ballotlemicOLD  29377  ballotlem1cOLD  29378  ballotlemsdomOLD  29382  ballotlemsel1iOLD  29383  ballotlemsimaOLD  29386  ballotlemfrceqOLD  29399  ballotlemfrcn0OLD  29400  sinccvg  30317  circum  30318  divcnvlin  30367  bcprod  30374  iprodgam  30378  faclimlem2  30380  faclim  30382  iprodfac  30383  faclim2  30384  fwddifnp1  30932  lmclim2  32087  geomcau  32088  heibor1lem  32141  heibor1  32142  bfplem1  32154  bfplem2  32155  rrncmslem  32164  rrncms  32165  fzsplit1nn0  35596  eldioph2lem1  35602  pellexlem6  35678  rmspecnonsq  35755  jm2.22  35850  jm2.23  35851  jm2.25  35854  dvradcnv2  36696  binomcxplemnn0  36698  binomcxplemrat  36699  binomcxplemnotnn0  36705  oddfl  37487  fmuldfeq  37661  fmul01lt1lem2  37663  fmul01lt1  37664  clim1fr1  37679  sumnnodd  37710  dvnmul  37818  stoweidlem3  37863  stoweidlem7  37867  stoweidlem11  37871  stoweidlem14  37874  stoweidlem20  37880  stoweidlem26  37886  stoweidlem34  37895  stoweidlem51  37912  wallispilem5  37931  wallispi  37932  stirlinglem1  37936  stirlinglem5  37940  stirlinglem7  37942  stirlinglem8  37943  stirlinglem10  37945  stirlinglem12  37947  stirlinglem13  37948  stirlinglem14  37949  stirlinglem15  37950  stirlingr  37952  fourierdlem4  37973  fourierdlem11  37980  fourierdlem26  37995  fourierdlem41  38011  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem48  38018  fourierdlem49  38019  fourierdlem79  38049  fourierdlem97  38067  fourierdlem103  38073  fourierdlem104  38074  fourierdlem112  38082  sqwvfoura  38092  sqwvfourb  38093  fouriersw  38095  etransclem15  38114  etransclem28  38127  etransclem35  38134  etransclem38  38137  etransclem44  38143  etransclem48OLD  38147  etransclem48  38148  sge0ad2en  38273  caragenunicl  38345  caratheodorylem2  38348  iccpartiltu  38736  iccpartgt  38741  perfectALTVlem2  38844  bgoldbtbndlem3  38902  upgrewlkle2  39625  2even  39986  nn0o1gt2  40380  fldivexpfllog2  40429  nnlog2ge0lt1  40430  logbpw2m1  40431  blenpw2m1  40443  blennnt2  40453  nnolog2flm1  40454  blennn0e2  40458  digexp  40471  dignn0flhalflem1  40479  dignn0flhalflem2  40480
  Copyright terms: Public domain W3C validator