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

Theorem 1zzd 12005
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 12004 . 2 1 ∈ ℤ
21a1i 11 1 (𝜑 → 1 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  1c1 10531  cz 11973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-neg 10866  df-nn 11630  df-z 11974
This theorem is referenced by:  fzm1  12986  fzoss2  13064  fzo1fzo0n0  13087  elfznelfzo  13141  negmod  13283  addmodid  13286  modnegd  13293  2submod  13299  sermono  13402  seqf1olem2  13410  bcp1nk  13677  eqwrds3  14320  climuni  14904  isercoll  15019  telfsumo  15152  fsumparts  15156  binomlem  15179  climcndslem2  15200  climcnds  15201  divcnv  15203  supcvg  15206  arisum  15210  trireciplem  15212  trirecip  15213  expcnv  15214  pwdif  15218  geo2sum  15224  geo2lim  15226  geoisum1  15230  geoisum1c  15231  mertenslem1  15235  mertenslem2  15236  fprodser  15298  fprodzcl  15303  risefacval2  15359  fallfacval2  15360  binomfallfaclem2  15389  bpolydiflem  15403  ege2le3  15438  rpnnen2lem12  15573  modm1div  15614  nn0o1gt2  15725  pwp1fsum  15735  bitscmp  15780  dvdsnprmd  16027  2mulprm  16030  hashdvds  16105  phiprmpw  16106  prmdiv  16115  odzdvds  16125  odzphi  16126  iserodd  16165  pcid  16202  pcmptcl  16220  pockthlem  16234  prmreclem4  16248  prmreclem6  16250  vdwapun  16303  prmdvdsprmo  16371  prmodvdslcmf  16376  prmgapprmo  16391  gsumpr12val  17894  mulgpropd  18264  cycsubggend  18343  sylow1lem1  18718  sylow3lem6  18752  pgpfac1lem2  19193  ablsimpgfindlem1  19225  zringcyg  20187  mulgrhm2  20195  znunit  20258  znrrg  20260  frgpcyg  20268  cpmadugsumlemF  21484  lmcnp  21912  lmmo  21988  1stcelcls  22069  1stccnp  22070  1stckgenlem  22161  1stckgen  22162  clmvneg1  23707  clmmulg  23709  lmnn  23870  cmetcaulem  23895  iscmet2  23901  causs  23905  nglmle  23909  caubl  23915  iscmet3i  23919  ovolsf  24079  ovoliunlem1  24109  ovoliun  24112  ovoliun2  24113  ovolicc2lem2  24125  ovolicc2lem3  24126  ovolicc2lem4  24127  voliunlem2  24158  voliunlem3  24159  ioombl1lem4  24168  uniioombllem2  24190  uniioombllem3  24192  uniioombllem6  24195  vitalilem4  24218  itg1climres  24321  mbfi1fseqlem6  24327  mbfi1flimlem  24329  mbfmullem2  24331  itg2monolem1  24357  itg2i1fseq  24362  itg2i1fseq2  24363  itg2addlem  24365  plyeq0lem  24810  dvply1  24883  dvtaylp  24968  pserdvlem2  25026  pserdv2  25028  advlogexp  25249  logtayl  25254  logtaylsum  25255  logtayl2  25256  atantayl  25526  leibpilem2  25530  leibpi  25531  birthdaylem2  25541  dfef2  25559  divsqrtsumlem  25568  emcllem4  25587  emcllem6  25589  emcllem7  25590  zetacvg  25603  lgamgulmlem4  25620  lgamgulmlem6  25622  lgamgulm2  25624  lgamcvglem  25628  lgamcvg2  25643  gamcvg  25644  regamcl  25649  relgamcl  25650  wilthlem1  25656  wilthlem2  25657  basellem6  25674  basellem7  25675  basellem8  25676  basellem9  25677  mersenne  25814  perfectlem1  25816  perfectlem2  25817  lgslem1  25884  lgsqrlem1  25933  gausslemma2dlem4  25956  gausslemma2dlem6  25959  gausslemma2dlem7  25960  lgseisenlem1  25962  lgsquad2lem1  25971  lgsquad3  25974  m1lgs  25975  2sqlem11  26016  dchrisumlema  26075  dchrisumlem3  26078  dchrmusum2  26081  dchrvmasumiflem1  26088  dchrvmaeq0  26091  dchrisum0re  26100  dchrisum0lem1b  26102  dchrisum0lem2a  26104  logdivsum  26120  pntrlog2bndlem1  26164  pntpbnd2  26174  axlowdimlem6  26744  axlowdim  26758  upgrewlkle2  27399  redwlk  27465  pthdadjvtx  27522  pthdlem1  27558  wwlksnextproplem2  27699  clwwlkccatlem  27777  minvecolem3  28662  minvecolem4b  28664  minvecolem4  28666  h2hcau  28765  h2hlm  28766  hlimadd  28979  hhsscms  29064  occllem  29089  nlelchi  29847  opsqrlem4  29929  hmopidmchi  29937  fzm1ne1  30541  fzspl  30542  fzsplit3  30546  prmdvdsbc  30561  pfxlsw2ccat  30655  tocycfvres1  30805  tocycfvres2  30806  cycpmfvlem  30807  cycpmfv1  30808  cycpmfv2  30809  cycpmfv3  30810  cycpmcl  30811  tocyc01  30813  cycpmco2lem6  30826  cycpmco2lem7  30827  cycpmconjv  30837  cycpmrn  30838  cycpmconjslem1  30849  cycpmconjslem2  30850  archirngz  30871  archiabllem1a  30873  smatrcl  31149  submateqlem1  31160  submateqlem2  31161  mdetlap  31185  rge0scvg  31300  lmxrge0  31303  lmdvg  31304  qqhval2lem  31330  esumfsupre  31438  esumpcvgval  31445  esumcvg  31453  eulerpartlems  31726  fiblem  31764  ballotlemfp1  31857  ballotlemimin  31871  ballotlemic  31872  ballotlem1c  31873  ballotlemsdom  31877  ballotlemsel1i  31878  ballotlemsima  31881  ballotlemfrceq  31894  ballotlemfrcn0  31895  chtvalz  32008  sinccvg  33024  circum  33025  divcnvlin  33072  bcprod  33078  iprodgam  33082  faclimlem2  33084  faclim  33086  iprodfac  33087  faclim2  33088  fwddifnp1  33734  lmclim2  35189  geomcau  35190  heibor1lem  35240  heibor1  35241  bfplem1  35253  bfplem2  35254  rrncmslem  35263  rrncms  35264  fzsplitnd  39263  lcmineqlem4  39313  lcmineqlem13  39322  lcmineqlem23  39332  metakunt1  39341  metakunt2  39342  metakunt3  39343  metakunt5  39345  metakunt7  39347  metakunt10  39350  metakunt15  39355  metakunt16  39356  metakunt19  39359  metakunt21  39361  metakunt22  39362  metakunt24  39364  metakunt25  39365  metakunt26  39366  metakunt28  39368  metakunt29  39369  metakunt30  39370  fzsplit1nn0  39682  eldioph2lem1  39688  pellexlem6  39762  rmspecnonsq  39835  jm2.22  39923  jm2.23  39924  jm2.25  39927  dvradcnv2  41038  binomcxplemnn0  41040  binomcxplemrat  41041  binomcxplemnotnn0  41047  oddfl  41895  uzubioo  42191  fmuldfeq  42212  fmul01lt1lem2  42214  fmul01lt1  42215  clim1fr1  42230  sumnnodd  42259  limsup10exlem  42401  fprodsubrecnncnvlem  42536  fprodaddrecnncnvlem  42538  dvnmul  42572  stoweidlem3  42632  stoweidlem7  42636  stoweidlem11  42640  stoweidlem14  42643  stoweidlem20  42649  stoweidlem26  42655  stoweidlem34  42663  stoweidlem51  42680  wallispilem5  42698  wallispi  42699  stirlinglem1  42703  stirlinglem5  42707  stirlinglem7  42709  stirlinglem8  42710  stirlinglem10  42712  stirlinglem12  42714  stirlinglem13  42715  stirlinglem14  42716  stirlinglem15  42717  stirlingr  42719  fourierdlem4  42740  fourierdlem11  42747  fourierdlem26  42762  fourierdlem41  42777  fourierdlem42  42778  fourierdlem48  42783  fourierdlem49  42784  fourierdlem79  42814  fourierdlem97  42832  fourierdlem103  42838  fourierdlem104  42839  fourierdlem112  42847  sqwvfoura  42857  sqwvfourb  42858  fouriersw  42860  etransclem15  42878  etransclem28  42891  etransclem35  42898  etransclem38  42901  etransclem44  42907  etransclem48  42911  sge0ad2en  43057  voliunsge0lem  43098  caragenunicl  43150  caratheodorylem2  43153  ovolval2lem  43269  ovolval2  43270  vonioolem2  43307  vonicclem2  43310  iccpartiltu  43926  iccpartgt  43931  fmtnoge3  44034  fmtnoprmfac1lem  44068  2pwp1prm  44093  sfprmdvdsmersenne  44108  lighneallem2  44111  perfectALTVlem2  44227  fpprwpprb  44245  nnsum3primesprm  44295  bgoldbtbndlem3  44312  2even  44544  fldivexpfllog2  44966  nnlog2ge0lt1  44967  logbpw2m1  44968  blenpw2m1  44980  blennnt2  44990  nnolog2flm1  44991  blennn0e2  44995  digexp  45008  dignn0flhalflem1  45016  dignn0flhalflem2  45017
  Copyright terms: Public domain W3C validator