Theorem 1zzd 12640

Description: One is an integer, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1zzd	⊢ (𝜑 → 1 ∈ ℤ)

Proof of Theorem 1zzd

Step	Hyp	Ref	Expression
1		1z 12639	. 2 ⊢ 1 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  1c1 11116  ℤcz 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-i2m1 11183  ax-1ne0 11184  ax-rrecex 11187  ax-cnre 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11459  df-nn 12249  df-z 12607

This theorem is used by:  fzm1  13652  fzoss2  13733  fzo1fzo0n0  13761  elfznelfzo  13819  negmod  13970  addmodid  13973  modnegd  13980  2submod  13986  sermono  14088  seqf1olem2  14096  bcp1nk  14371  eqwrds3  15022  climuni  15627  isercoll  15743  telfsumo  15877  fsumparts  15881  binomlem  15906  climcndslem2  15927  climcnds  15928  divcnv  15930  supcvg  15933  arisum  15937  trireciplem  15939  trirecip  15940  expcnv  15941  pwdif  15945  geo2sum  15950  geo2lim  15952  geoisum1  15956  geoisum1c  15957  mertenslem1  15961  mertenslem2  15962  fprodser  16026  fprodzcl  16031  risefacval2  16087  fallfacval2  16088  binomfallfaclem2  16116  bpolydiflem  16130  ege2le3  16166  rpnnen2lem12  16303  modm1div  16344  nn0o1gt2  16461  pwp1fsum  16471  bitscmp  16518  dvdsnprmd  16770  2mulprm  16773  prmdvdsbc  16807  hashdvds  16856  phiprmpw  16857  prmdiv  16866  odzdvds  16877  odzphi  16878  iserodd  16917  pcid  16955  pcmptcl  16973  pockthlem  16987  prmreclem4  17001  prmreclem6  17003  vdwapun  17056  prmdvdsprmo  17124  prmodvdslcmf  17129  prmgapprmo  17144  chnub  18700  gsumpr12val  18779  mulgpropd  19226  cycsubggend  19320  odm1inv  19667  sylow1lem1  19712  sylow3lem6  19746  pgpfac1lem2  20191  ablsimpgfindlem1  20223  zringcyg  21669  mulgrhm2  21678  pzriprnglem6  21686  znunit  21763  znrrg  21765  frgpcyg  21773  cpmadugsumlemF  23083  lmcnp  23511  lmmo  23587  1stcelcls  23669  1stccnp  23670  1stckgenlem  23761  1stckgen  23762  clmvneg1  25309  clmmulg  25311  lmnn  25473  cmetcaulem  25498  iscmet2  25504  causs  25508  nglmle  25512  caubl  25518  iscmet3i  25522  ovolsf  25682  ovoliunlem1  25712  ovoliun  25715  ovoliun2  25716  ovolicc2lem2  25728  ovolicc2lem3  25729  ovolicc2lem4  25730  voliunlem2  25761  voliunlem3  25762  ioombl1lem4  25771  uniioombllem2  25793  uniioombllem3  25795  uniioombllem6  25798  vitalilem4  25821  itg1climres  25924  mbfi1fseqlem6  25930  mbfi1flimlem  25932  mbfmullem2  25934  itg2monolem1  25960  itg2i1fseq  25965  itg2i1fseq2  25966  itg2addlem  25968  plyeq0lem  26418  dvply1  26496  dvtaylp  26584  pserdvlem2  26642  pserdv2  26644  advlogexp  26871  logtayl  26876  logtaylsum  26877  logtayl2  26878  atantayl  27153  leibpilem2  27157  leibpi  27158  birthdaylem2  27168  dfef2  27186  divsqrtsumlem  27195  emcllem4  27214  emcllem6  27216  emcllem7  27217  zetacvg  27230  lgamgulmlem4  27247  lgamgulmlem6  27249  lgamgulm2  27251  lgamcvglem  27255  lgamcvg2  27270  gamcvg  27271  regamcl  27276  relgamcl  27277  wilthlem1  27283  wilthlem2  27284  basellem6  27301  basellem7  27302  basellem8  27303  basellem9  27304  ppiub  27419  mersenne  27442  perfectlem1  27444  perfectlem2  27445  lgslem1  27512  lgsqrlem1  27561  gausslemma2dlem4  27584  gausslemma2dlem6  27587  gausslemma2dlem7  27588  lgseisenlem1  27590  lgsquad2lem1  27599  lgsquad3  27602  m1lgs  27603  2sqlem11  27644  dchrisumlema  27703  dchrisumlem3  27706  dchrmusum2  27709  dchrvmasumiflem1  27716  dchrvmaeq0  27719  dchrisum0re  27728  dchrisum0lem1b  27730  dchrisum0lem2a  27732  logdivsum  27748  pntrlog2bndlem1  27792  pntpbnd2  27802  axlowdimlem6  29352  axlowdim  29366  upgrewlkle2  30014  redwlk  30078  pthdadjvtx  30140  pthdlem1  30179  wwlksnextproplem2  30326  clwwlkccatlem  30407  minvecolem3  31299  minvecolem4b  31301  minvecolem4  31303  h2hcau  31402  h2hlm  31403  hlimadd  31616  hhsscms  31701  occllem  31726  nlelchi  32484  opsqrlem4  32566  hmopidmchi  32574  fzm1ne1  33203  fzspl  33204  fzsplit3  33208  pfxlsw2ccat  33336  tocycfvres1  33494  tocycfvres2  33495  cycpmfvlem  33496  cycpmfv1  33497  cycpmfv2  33498  cycpmfv3  33499  cycpmcl  33500  tocyc01  33502  cycpmco2lem6  33515  cycpmco2lem7  33516  cycpmconjv  33526  cycpmrn  33527  cycpmconjslem1  33538  cycpmconjslem2  33539  archirngz  33573  archiabllem1a  33575  elrgspnlem2  33627  elrgspnlem3  33628  elrgspnsubrunlem1  33631  zringfrac  33908  esplyfval0  34018  esplympl  34021  esplyfval3  34026  vieta  34034  rtelextdg2  34181  constrrecl  34223  constrimcl  34224  constrmulcl  34225  constrreinvcl  34226  constrinvcl  34227  constrsdrg  34229  constrresqrtcl  34231  constrabscl  34232  cos9thpiminplylem2  34237  cos9thpiminplylem6  34241  cos9thpiminply  34242  cos9thpinconstrlem1  34243  smatrcl  34250  submateqlem1  34261  submateqlem2  34262  mdetlap  34286  rge0scvg  34403  lmxrge0  34406  lmdvg  34407  zrhcntr  34433  qqhval2lem  34435  esumfsupre  34525  esumpcvgval  34532  esumcvg  34540  eulerpartlems  34815  fiblem  34853  ballotlemfp1  34947  ballotlemimin  34961  ballotlemic  34962  ballotlem1c  34963  ballotlemsdom  34967  ballotlemsel1i  34968  ballotlemsima  34971  ballotlemfrceq  34984  ballotlemfrcn0  34985  chtvalz  35081  sinccvg  36202  circum  36203  divcnvlin  36262  bcprod  36267  iprodgam  36271  faclimlem2  36273  faclim  36275  iprodfac  36276  faclim2  36277  fwddifnp1  36694  lmclim2  38467  geomcau  38468  heibor1lem  38518  heibor1  38519  bfplem1  38531  bfplem2  38532  rrncmslem  38541  rrncms  38542  fzsplitnd  42807  lcmineqlem4  42857  lcmineqlem13  42866  lcmineqlem23  42876  dvrelogpow2b  42893  aks4d1p1p7  42899  aks4d1p1  42901  aks4d1p3  42903  aks4d1p5  42905  aks4d1p7  42908  aks4d1p8d2  42910  aks4d1p8  42912  aks4d1p9  42913  primrootscoprbij  42927  primrootspoweq0  42931  hashscontpow1  42946  aks6d1c5lem1  42961  sticksstones6  42976  sticksstones7  42977  sticksstones9  42979  sticksstones10  42980  sticksstones11  42981  sticksstones12a  42982  sticksstones12  42983  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c7lem1  43005  aks6d1c7lem2  43006  grpods  43019  unitscyglem2  43021  unitscyglem4  43023  unitscyglem5  43024  fzsplit1nn0  43543  eldioph2lem1  43549  pellexlem6  43619  rmspecnonsq  43692  jm2.22  43780  jm2.23  43781  jm2.25  43784  dvradcnv2  45115  binomcxplemnn0  45117  binomcxplemrat  45118  binomcxplemnotnn0  45124  oddfl  46055  uzubioo  46339  fmuldfeq  46357  fmul01lt1lem2  46359  fmul01lt1  46360  clim1fr1  46375  sumnnodd  46404  limsup10exlem  46544  fprodsubrecnncnvlem  46679  fprodaddrecnncnvlem  46681  dvnmul  46715  stoweidlem3  46775  stoweidlem7  46779  stoweidlem11  46783  stoweidlem14  46786  stoweidlem20  46792  stoweidlem26  46798  stoweidlem34  46806  stoweidlem51  46823  wallispilem5  46841  wallispi  46842  stirlinglem1  46846  stirlinglem5  46850  stirlinglem7  46852  stirlinglem8  46853  stirlinglem10  46855  stirlinglem12  46857  stirlinglem13  46858  stirlinglem14  46859  stirlinglem15  46860  stirlingr  46862  fourierdlem4  46883  fourierdlem11  46890  fourierdlem26  46905  fourierdlem41  46920  fourierdlem42  46921  fourierdlem48  46926  fourierdlem49  46927  fourierdlem79  46957  fourierdlem97  46975  fourierdlem103  46981  fourierdlem104  46982  fourierdlem112  46990  sqwvfoura  47000  sqwvfourb  47001  fouriersw  47003  etransclem15  47021  etransclem28  47034  etransclem35  47041  etransclem38  47044  etransclem44  47050  etransclem48  47054  sge0ad2en  47203  voliunsge0lem  47244  caragenunicl  47296  caratheodorylem2  47299  ovolval2lem  47415  ovolval2  47416  vonioolem2  47453  vonicclem2  47456  cos5t  47674  addmodne  48145  m1modne  48149  m1modnep2mod  48153  modm2nep1  48167  modp2nep1  48168  modm1nep2  48169  modm1nem2  48170  modm1p1ne  48171  iccpartiltu  48229  iccpartgt  48234  fmtnoge3  48340  fmtnoprmfac1lem  48374  2pwp1prm  48399  sfprmdvdsmersenne  48413  lighneallem2  48416  perfectALTVlem2  48545  fpprwpprb  48563  nnsum3primesprm  48613  bgoldbtbndlem3  48630  gpgvtx0  48876  gpgprismgrusgra  48881  gpgedgvtx1  48885  gpgedg2ov  48889  gpg3nbgrvtx0  48899  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  2even  49061  fldivexpfllog2  49402  nnlog2ge0lt1  49403  logbpw2m1  49404  blenpw2m1  49416  blennnt2  49426  nnolog2flm1  49427  blennn0e2  49431  digexp  49444  dignn0flhalflem1  49452  dignn0flhalflem2  49453