Theorem 1zzd 12767

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 12766	. 2 ⊢ 1 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  1c1 11240  ℤcz 12733

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-neg 11583  df-nn 12376  df-z 12734

This theorem is used by:  fzm1  13781  fzoss2  13862  fzo1fzo0n0  13890  elfznelfzo  13948  negmod  14099  addmodid  14102  modnegd  14109  2submod  14115  sermono  14217  seqf1olem2  14225  bcp1nk  14502  eqwrds3  15157  climuni  15763  isercoll  15879  telfsumo  16013  fsumparts  16017  binomlem  16042  climcndslem2  16063  climcnds  16064  divcnv  16066  supcvg  16069  arisum  16073  trireciplem  16075  trirecip  16076  expcnv  16077  pwdif  16081  geo2sum  16086  geo2lim  16088  geoisum1  16092  geoisum1c  16093  mertenslem1  16097  mertenslem2  16098  fprodser  16160  fprodzcl  16165  risefacval2  16221  fallfacval2  16222  binomfallfaclem2  16250  bpolydiflem  16264  ege2le3  16300  rpnnen2lem12  16437  modm1div  16478  nn0o1gt2  16595  pwp1fsum  16605  bitscmp  16652  dvdsnprmd  16909  2mulprm  16912  prmdvdsbc  16946  hashdvds  16996  phiprmpw  16997  prmdiv  17006  odzdvds  17017  odzphi  17018  iserodd  17057  pcid  17095  pcmptcl  17113  pockthlem  17127  prmreclem4  17141  prmreclem6  17143  vdwapun  17196  prmdvdsprmo  17264  prmodvdslcmf  17269  prmgapprmo  17284  chnub  18846  gsumpr12val  18928  mulgpropd  19376  cycsubggend  19470  odm1inv  19818  sylow1lem1  19863  sylow3lem6  19897  pgpfac1lem2  20342  ablsimpgfindlem1  20374  zringcyg  21830  mulgrhm2  21839  pzriprnglem6  21847  znunit  21924  znrrg  21926  frgpcyg  21934  cpmadugsumlemF  23249  lmcnp  23677  lmmo  23753  1stcelcls  23835  1stccnp  23836  1stckgenlem  23927  1stckgen  23928  clmvneg1  25475  clmmulg  25477  lmnn  25639  cmetcaulem  25664  iscmet2  25670  causs  25674  nglmle  25678  caubl  25684  iscmet3i  25688  ovolsf  25848  ovoliunlem1  25878  ovoliun  25881  ovoliun2  25882  ovolicc2lem2  25894  ovolicc2lem3  25895  ovolicc2lem4  25896  voliunlem2  25927  voliunlem3  25928  ioombl1lem4  25937  uniioombllem2  25959  uniioombllem3  25961  uniioombllem6  25964  vitalilem4  25987  itg1climres  26090  mbfi1fseqlem6  26096  mbfi1flimlem  26098  mbfmullem2  26100  itg2monolem1  26126  itg2i1fseq  26131  itg2i1fseq2  26132  itg2addlem  26134  plyeq0lem  26584  dvply1  26660  dvtaylp  26754  pserdvlem2  26812  pserdv2  26814  advlogexp  27040  logtayl  27045  logtaylsum  27046  logtayl2  27047  atantayl  27322  leibpilem2  27326  leibpi  27327  birthdaylem2  27337  dfef2  27355  divsqrtsumlem  27364  emcllem4  27383  emcllem6  27385  emcllem7  27386  zetacvg  27399  lgamgulmlem4  27416  lgamgulmlem6  27418  lgamgulm2  27420  lgamcvglem  27424  lgamcvg2  27439  gamcvg  27440  regamcl  27445  relgamcl  27446  wilthlem1  27452  wilthlem2  27453  basellem6  27470  basellem7  27471  basellem8  27472  basellem9  27473  ppiub  27588  mersenne  27611  perfectlem1  27613  perfectlem2  27614  lgslem1  27681  lgsqrlem1  27730  gausslemma2dlem4  27753  gausslemma2dlem6  27756  gausslemma2dlem7  27757  lgseisenlem1  27759  lgsquad2lem1  27768  lgsquad3  27771  m1lgs  27772  2sqlem11  27813  dchrisumlema  27872  dchrisumlem3  27875  dchrmusum2  27878  dchrvmasumiflem1  27885  dchrvmaeq0  27888  dchrisum0re  27897  dchrisum0lem1b  27899  dchrisum0lem2a  27901  logdivsum  27917  pntrlog2bndlem1  27961  pntpbnd2  27971  fltoprmlem2  28051  axlowdimlem6  29582  axlowdim  29596  upgrewlkle2  30244  redwlk  30308  pthdadjvtx  30370  pthdlem1  30409  wwlksnextproplem2  30556  clwwlkccatlem  30637  minvecolem3  31535  minvecolem4b  31537  minvecolem4  31539  h2hcau  31638  h2hlm  31639  hlimadd  31852  hhsscms  31937  occllem  31962  nlelchi  32720  opsqrlem4  32802  hmopidmchi  32810  fzm1ne1  33476  fzspl  33477  fzsplit3  33481  pfxlsw2ccat  33609  tocycfvres1  33770  tocycfvres2  33771  cycpmfvlem  33772  cycpmfv1  33773  cycpmfv2  33774  cycpmfv3  33775  cycpmcl  33776  tocyc01  33778  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmconjv  33802  cycpmrn  33803  cycpmconjslem1  33814  cycpmconjslem2  33815  archirngz  33849  archiabllem1a  33851  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnsubrunlem1  33907  zringfrac  34189  esplyfval0  34307  esplympl  34310  esplyfval3  34315  vieta  34323  rtelextdg2  34470  constrrecl  34512  constrimcl  34513  constrmulcl  34514  constrreinvcl  34515  constrinvcl  34516  constrsdrg  34518  constrresqrtcl  34520  constrabscl  34521  cos9thpiminplylem2  34526  cos9thpiminplylem6  34530  cos9thpiminply  34531  cos9thpinconstrlem1  34532  smatrcl  34539  submateqlem1  34550  submateqlem2  34551  mdetlap  34575  rge0scvg  34692  lmxrge0  34695  lmdvg  34696  zrhcntr  34722  qqhval2lem  34724  esumfsupre  34814  esumpcvgval  34821  esumcvg  34829  eulerpartlems  35103  fiblem  35141  ballotlemfp1  35235  ballotlemimin  35249  ballotlemic  35250  ballotlem1c  35251  ballotlemsdom  35255  ballotlemsel1i  35256  ballotlemsima  35259  ballotlemfrceq  35272  ballotlemfrcn0  35273  chtvalz  35369  sinccvg  36646  circum  36647  divcnvlin  36713  bcprod  36718  iprodgam  36722  faclimlem2  36724  faclim  36726  iprodfac  36727  faclim2  36728  fwddifnp1  37145  lmclim2  38958  geomcau  38959  heibor1lem  39009  heibor1  39010  bfplem1  39022  bfplem2  39023  rrncmslem  39032  rrncms  39033  fzsplitnd  43298  lcmineqlem4  43348  lcmineqlem13  43357  lcmineqlem23  43367  dvrelogpow2b  43384  aks4d1p1p7  43390  aks4d1p1  43392  aks4d1p3  43394  aks4d1p5  43396  aks4d1p7  43399  aks4d1p8d2  43401  aks4d1p8  43403  aks4d1p9  43404  primrootscoprbij  43418  primrootspoweq0  43422  hashscontpow1  43437  aks6d1c5lem1  43452  sticksstones6  43467  sticksstones7  43468  sticksstones9  43470  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c7lem1  43496  aks6d1c7lem2  43497  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  unitscyglem5  43515  fzsplit1nn0  44031  eldioph2lem1  44037  pellexlem6  44107  rmspecnonsq  44180  jm2.22  44268  jm2.23  44269  jm2.25  44272  dvradcnv2  45592  binomcxplemnn0  45594  binomcxplemrat  45595  binomcxplemnotnn0  45601  oddfl  46567  uzubioo  46850  fmuldfeq  46868  fmul01lt1lem2  46870  fmul01lt1  46871  clim1fr1  46886  sumnnodd  46915  limsup10exlem  47055  fprodsubrecnncnvlem  47190  fprodaddrecnncnvlem  47192  dvnmul  47226  stoweidlem3  47286  stoweidlem7  47290  stoweidlem11  47294  stoweidlem14  47297  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  stoweidlem51  47334  wallispilem5  47352  wallispi  47353  stirlinglem1  47357  stirlinglem5  47361  stirlinglem7  47363  stirlinglem8  47364  stirlinglem10  47366  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  stirlingr  47373  fourierdlem4  47394  fourierdlem11  47401  fourierdlem26  47416  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem79  47468  fourierdlem97  47486  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  sqwvfoura  47511  sqwvfourb  47512  fouriersw  47514  etransclem15  47532  etransclem28  47545  etransclem35  47552  etransclem38  47555  etransclem44  47561  etransclem48  47565  sge0ad2en  47714  voliunsge0lem  47755  caragenunicl  47807  caratheodorylem2  47810  ovolval2lem  47926  ovolval2  47927  vonioolem2  47964  vonicclem2  47967  cos5t  48198  addmodne  48693  m1modne  48697  m1modnep2mod  48701  modm2nep1  48715  modp2nep1  48716  modm1nep2  48717  modm1nem2  48718  modm1p1ne  48719  iccpartiltu  48777  iccpartgt  48782  fmtnoge3  48888  fmtnoprmfac1lem  48922  2pwp1prm  48947  sfprmdvdsmersenne  48961  lighneallem2  48964  perfectALTVlem2  49093  fpprwpprb  49111  nnsum3primesprm  49161  bgoldbtbndlem3  49178  gpgvtx0  49424  gpgprismgrusgra  49429  gpgedgvtx1  49433  gpgedg2ov  49437  gpg3nbgrvtx0  49447  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  2even  49609  fldivexpfllog2  50008  nnlog2ge0lt1  50009  logbpw2m1  50010  blenpw2m1  50022  blennnt2  50032  nnolog2flm1  50033  blennn0e2  50037  digexp  50050  dignn0flhalflem1  50058  dignn0flhalflem2  50059  veronesev1lem  51401  veronesev2lem  51402  veronesev3lem  51403  veronesev4lem  51404  veronesev5lem  51405  veronesev6lem  51406