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

Theorem 1zzd 11674
Description: One is an integer, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1zzd (𝜑 → 1 ∈ ℤ)

Proof of Theorem 1zzd
StepHypRef Expression
1 1z 11673 . 2 1 ∈ ℤ
21a1i 11 1 (𝜑 → 1 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  1c1 10222  cz 11643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-z 11644
This theorem is referenced by:  fzm1  12643  fzoss2  12720  fz1fzo0m1  12740  fzo1fzo0n0  12743  elfznelfzo  12797  negmod  12939  addmodid  12942  modnegd  12949  2submod  12955  sermono  13056  seqf1olem2  13064  bcp1nk  13324  eqwrds3  13929  climuni  14506  isercoll  14621  telfsumo  14756  fsumparts  14760  binomlem  14783  climcndslem2  14804  climcnds  14805  divcnv  14807  supcvg  14810  arisum  14814  trireciplem  14816  trirecip  14817  expcnv  14818  geo2sum  14826  geo2lim  14828  geoisum1  14832  geoisum1c  14833  mertenslem1  14837  mertenslem2  14838  fprodser  14900  fprodzcl  14905  risefacval2  14961  fallfacval2  14962  binomfallfaclem2  14991  bpolydiflem  15005  ege2le3  15040  rpnnen2lem12  15174  nn0o1gt2  15317  pwp1fsum  15334  bitscmp  15379  dvdsnprmd  15621  hashdvds  15697  phiprmpw  15698  prmdiv  15707  odzdvds  15717  odzphi  15718  modprm1div  15719  iserodd  15757  pcid  15794  pcmptcl  15812  pockthlem  15826  prmreclem4  15840  prmreclem6  15842  vdwapun  15895  prmdvdsprmo  15963  prmodvdslcmf  15968  prmgapprmo  15983  gsumpr12val  17487  mulgpropd  17786  sylow1lem1  18214  sylow3lem6  18248  pgpfac1lem2  18676  zringcyg  20047  mulgrhm2  20055  znunit  20119  znrrg  20121  frgpcyg  20129  cpmadugsumlemF  20894  lmcnp  21322  lmmo  21398  1stcelcls  21478  1stccnp  21479  1stckgenlem  21570  1stckgen  21571  clmvneg1  23111  clmmulg  23113  lmnn  23273  cmetcaulem  23298  iscmet2  23304  causs  23308  nglmle  23312  caubl  23318  iscmet3i  23322  ovolsf  23453  ovoliunlem1  23483  ovoliun  23486  ovoliun2  23487  ovolicc2lem2  23499  ovolicc2lem3  23500  ovolicc2lem4  23501  voliunlem2  23532  voliunlem3  23533  ioombl1lem4  23542  uniioombllem2  23564  uniioombllem3  23566  uniioombllem6  23569  vitalilem4  23592  itg1climres  23695  mbfi1fseqlem6  23701  mbfi1flimlem  23703  mbfmullem2  23705  itg2monolem1  23731  itg2i1fseq  23736  itg2i1fseq2  23737  itg2addlem  23739  plyeq0lem  24180  dvply1  24253  dvtaylp  24338  pserdvlem2  24396  pserdv2  24398  advlogexp  24615  logtayl  24620  logtaylsum  24621  logtayl2  24622  atantayl  24878  leibpilem2  24882  leibpi  24883  birthdaylem2  24893  dfef2  24911  divsqrtsumlem  24920  emcllem4  24939  emcllem6  24941  emcllem7  24942  zetacvg  24955  lgamgulmlem4  24972  lgamgulmlem6  24974  lgamgulm2  24976  lgamcvglem  24980  lgamcvg2  24995  gamcvg  24996  regamcl  25001  relgamcl  25002  wilthlem1  25008  wilthlem2  25009  basellem6  25026  basellem7  25027  basellem8  25028  basellem9  25029  mersenne  25166  perfectlem1  25168  perfectlem2  25169  lgslem1  25236  lgsqrlem1  25285  gausslemma2dlem4  25308  gausslemma2dlem6  25311  gausslemma2dlem7  25312  lgseisenlem1  25314  lgsquad2lem1  25323  lgsquad3  25326  m1lgs  25327  2sqlem11  25368  dchrisumlema  25391  dchrisumlem3  25394  dchrmusum2  25397  dchrvmasumiflem1  25404  dchrvmaeq0  25407  dchrisum0re  25416  dchrisum0lem1b  25418  dchrisum0lem2a  25420  logdivsum  25436  pntrlog2bndlem1  25480  pntpbnd2  25490  axlowdimlem6  26041  axlowdim  26055  upgrewlkle2  26730  redwlk  26797  pthdadjvtx  26854  pthdlem1  26890  wwlksnextproplem2  27048  clwlksfclwwlkOLD  27236  minvecolem3  28060  minvecolem4b  28062  minvecolem4  28064  h2hcau  28164  h2hlm  28165  hlimadd  28378  hhsscms  28464  occllem  28490  nlelchi  29248  opsqrlem4  29330  hmopidmchi  29338  fzspl  29877  fzsplit3  29880  archirngz  30068  archiabllem1a  30070  smatrcl  30187  submateqlem1  30198  submateqlem2  30199  mdetlap  30223  rge0scvg  30320  lmxrge0  30323  lmdvg  30324  qqhval2lem  30350  esumfsupre  30458  esumpcvgval  30465  esumcvg  30473  eulerpartlems  30747  fiblem  30785  ballotlemfp1  30878  ballotlemimin  30892  ballotlemic  30893  ballotlem1c  30894  ballotlemsdom  30898  ballotlemsel1i  30899  ballotlemsima  30902  ballotlemfrceq  30915  ballotlemfrcn0  30916  chtvalz  31032  sinccvg  31889  circum  31890  divcnvlin  31940  bcprod  31946  iprodgam  31950  faclimlem2  31952  faclim  31954  iprodfac  31955  faclim2  31956  fwddifnp1  32593  lmclim2  33865  geomcau  33866  heibor1lem  33919  heibor1  33920  bfplem1  33932  bfplem2  33933  rrncmslem  33942  rrncms  33943  fzsplit1nn0  37819  eldioph2lem1  37825  pellexlem6  37900  rmspecnonsq  37973  jm2.22  38063  jm2.23  38064  jm2.25  38067  dvradcnv2  39046  binomcxplemnn0  39048  binomcxplemrat  39049  binomcxplemnotnn0  39055  oddfl  39971  uzubioo  40274  fmuldfeq  40295  fmul01lt1lem2  40297  fmul01lt1  40298  clim1fr1  40313  sumnnodd  40342  limsup10exlem  40484  fprodsubrecnncnvlem  40601  fprodaddrecnncnvlem  40603  dvnmul  40638  stoweidlem3  40699  stoweidlem7  40703  stoweidlem11  40707  stoweidlem14  40710  stoweidlem20  40716  stoweidlem26  40722  stoweidlem34  40730  stoweidlem51  40747  wallispilem5  40765  wallispi  40766  stirlinglem1  40770  stirlinglem5  40774  stirlinglem7  40776  stirlinglem8  40777  stirlinglem10  40779  stirlinglem12  40781  stirlinglem13  40782  stirlinglem14  40783  stirlinglem15  40784  stirlingr  40786  fourierdlem4  40807  fourierdlem11  40814  fourierdlem26  40829  fourierdlem41  40844  fourierdlem42  40845  fourierdlem48  40850  fourierdlem49  40851  fourierdlem79  40881  fourierdlem97  40899  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  sqwvfoura  40924  sqwvfourb  40925  fouriersw  40927  etransclem15  40945  etransclem28  40958  etransclem35  40965  etransclem38  40968  etransclem44  40974  etransclem48  40978  sge0ad2en  41127  voliunsge0lem  41168  caragenunicl  41220  caratheodorylem2  41223  ovolval2lem  41339  ovolval2  41340  vonioolem2  41377  vonicclem2  41380  iccpartiltu  41933  iccpartgt  41938  fmtnoge3  42017  fmtnoprmfac1lem  42051  pwdif  42076  2pwp1prm  42078  sfprmdvdsmersenne  42095  lighneallem2  42098  perfectALTVlem2  42206  nnsum3primesprm  42253  bgoldbtbndlem3  42270  2even  42501  fldivexpfllog2  42927  nnlog2ge0lt1  42928  logbpw2m1  42929  blenpw2m1  42941  blennnt2  42951  nnolog2flm1  42952  blennn0e2  42956  digexp  42969  dignn0flhalflem1  42977  dignn0flhalflem2  42978
  Copyright terms: Public domain W3C validator