Theorem 1zzd 12649

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  1c1 11125  ℤcz 12615

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rrecex 11196  ax-cnre 11197

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11468  df-nn 12258  df-z 12616

This theorem is used by:  fzm1  13662  fzoss2  13743  fzo1fzo0n0  13771  elfznelfzo  13829  negmod  13980  addmodid  13983  modnegd  13990  2submod  13996  sermono  14098  seqf1olem2  14106  bcp1nk  14381  eqwrds3  15034  climuni  15639  isercoll  15755  telfsumo  15889  fsumparts  15893  binomlem  15918  climcndslem2  15939  climcnds  15940  divcnv  15942  supcvg  15945  arisum  15949  trireciplem  15951  trirecip  15952  expcnv  15953  pwdif  15957  geo2sum  15962  geo2lim  15964  geoisum1  15968  geoisum1c  15969  mertenslem1  15973  mertenslem2  15974  fprodser  16036  fprodzcl  16041  risefacval2  16097  fallfacval2  16098  binomfallfaclem2  16126  bpolydiflem  16140  ege2le3  16176  rpnnen2lem12  16313  modm1div  16354  nn0o1gt2  16471  pwp1fsum  16481  bitscmp  16528  dvdsnprmd  16780  2mulprm  16783  prmdvdsbc  16817  hashdvds  16866  phiprmpw  16867  prmdiv  16876  odzdvds  16887  odzphi  16888  iserodd  16927  pcid  16965  pcmptcl  16983  pockthlem  16997  prmreclem4  17011  prmreclem6  17013  vdwapun  17066  prmdvdsprmo  17134  prmodvdslcmf  17139  prmgapprmo  17154  chnub  18710  gsumpr12val  18791  mulgpropd  19239  cycsubggend  19333  odm1inv  19680  sylow1lem1  19725  sylow3lem6  19759  pgpfac1lem2  20204  ablsimpgfindlem1  20236  zringcyg  21682  mulgrhm2  21691  pzriprnglem6  21699  znunit  21776  znrrg  21778  frgpcyg  21786  cpmadugsumlemF  23101  lmcnp  23529  lmmo  23605  1stcelcls  23687  1stccnp  23688  1stckgenlem  23779  1stckgen  23780  clmvneg1  25327  clmmulg  25329  lmnn  25491  cmetcaulem  25516  iscmet2  25522  causs  25526  nglmle  25530  caubl  25536  iscmet3i  25540  ovolsf  25700  ovoliunlem1  25730  ovoliun  25733  ovoliun2  25734  ovolicc2lem2  25746  ovolicc2lem3  25747  ovolicc2lem4  25748  voliunlem2  25779  voliunlem3  25780  ioombl1lem4  25789  uniioombllem2  25811  uniioombllem3  25813  uniioombllem6  25816  vitalilem4  25839  itg1climres  25942  mbfi1fseqlem6  25948  mbfi1flimlem  25950  mbfmullem2  25952  itg2monolem1  25978  itg2i1fseq  25983  itg2i1fseq2  25984  itg2addlem  25986  plyeq0lem  26436  dvply1  26514  dvtaylp  26606  pserdvlem2  26664  pserdv2  26666  advlogexp  26892  logtayl  26897  logtaylsum  26898  logtayl2  26899  atantayl  27174  leibpilem2  27178  leibpi  27179  birthdaylem2  27189  dfef2  27207  divsqrtsumlem  27216  emcllem4  27235  emcllem6  27237  emcllem7  27238  zetacvg  27251  lgamgulmlem4  27268  lgamgulmlem6  27270  lgamgulm2  27272  lgamcvglem  27276  lgamcvg2  27291  gamcvg  27292  regamcl  27297  relgamcl  27298  wilthlem1  27304  wilthlem2  27305  basellem6  27322  basellem7  27323  basellem8  27324  basellem9  27325  ppiub  27440  mersenne  27463  perfectlem1  27465  perfectlem2  27466  lgslem1  27533  lgsqrlem1  27582  gausslemma2dlem4  27605  gausslemma2dlem6  27608  gausslemma2dlem7  27609  lgseisenlem1  27611  lgsquad2lem1  27620  lgsquad3  27623  m1lgs  27624  2sqlem11  27665  dchrisumlema  27724  dchrisumlem3  27727  dchrmusum2  27730  dchrvmasumiflem1  27737  dchrvmaeq0  27740  dchrisum0re  27749  dchrisum0lem1b  27751  dchrisum0lem2a  27753  logdivsum  27769  pntrlog2bndlem1  27813  pntpbnd2  27823  axlowdimlem6  29404  axlowdim  29418  upgrewlkle2  30066  redwlk  30130  pthdadjvtx  30192  pthdlem1  30231  wwlksnextproplem2  30378  clwwlkccatlem  30459  minvecolem3  31357  minvecolem4b  31359  minvecolem4  31361  h2hcau  31460  h2hlm  31461  hlimadd  31674  hhsscms  31759  occllem  31784  nlelchi  32542  opsqrlem4  32624  hmopidmchi  32632  fzm1ne1  33259  fzspl  33260  fzsplit3  33264  pfxlsw2ccat  33392  tocycfvres1  33550  tocycfvres2  33551  cycpmfvlem  33552  cycpmfv1  33553  cycpmfv2  33554  cycpmfv3  33555  cycpmcl  33556  tocyc01  33558  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmconjv  33582  cycpmrn  33583  cycpmconjslem1  33594  cycpmconjslem2  33595  archirngz  33629  archiabllem1a  33631  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnsubrunlem1  33687  zringfrac  33964  esplyfval0  34074  esplympl  34077  esplyfval3  34082  vieta  34090  rtelextdg2  34237  constrrecl  34279  constrimcl  34280  constrmulcl  34281  constrreinvcl  34282  constrinvcl  34283  constrsdrg  34285  constrresqrtcl  34287  constrabscl  34288  cos9thpiminplylem2  34293  cos9thpiminplylem6  34297  cos9thpiminply  34298  cos9thpinconstrlem1  34299  smatrcl  34306  submateqlem1  34317  submateqlem2  34318  mdetlap  34342  rge0scvg  34459  lmxrge0  34462  lmdvg  34463  zrhcntr  34489  qqhval2lem  34491  esumfsupre  34581  esumpcvgval  34588  esumcvg  34596  eulerpartlems  34871  fiblem  34909  ballotlemfp1  35003  ballotlemimin  35017  ballotlemic  35018  ballotlem1c  35019  ballotlemsdom  35023  ballotlemsel1i  35024  ballotlemsima  35027  ballotlemfrceq  35040  ballotlemfrcn0  35041  chtvalz  35137  sinccvg  36252  circum  36253  divcnvlin  36312  bcprod  36317  iprodgam  36321  faclimlem2  36323  faclim  36325  iprodfac  36326  faclim2  36327  fwddifnp1  36745  lmclim2  38508  geomcau  38509  heibor1lem  38559  heibor1  38560  bfplem1  38572  bfplem2  38573  rrncmslem  38582  rrncms  38583  fzsplitnd  42848  lcmineqlem4  42898  lcmineqlem13  42907  lcmineqlem23  42917  dvrelogpow2b  42934  aks4d1p1p7  42940  aks4d1p1  42942  aks4d1p3  42944  aks4d1p5  42946  aks4d1p7  42949  aks4d1p8d2  42951  aks4d1p8  42953  aks4d1p9  42954  primrootscoprbij  42968  primrootspoweq0  42972  hashscontpow1  42987  aks6d1c5lem1  43002  sticksstones6  43017  sticksstones7  43018  sticksstones9  43020  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c7lem1  43046  aks6d1c7lem2  43047  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  unitscyglem5  43065  fzsplit1nn0  43599  eldioph2lem1  43605  pellexlem6  43675  rmspecnonsq  43748  jm2.22  43836  jm2.23  43837  jm2.25  43840  dvradcnv2  45171  binomcxplemnn0  45173  binomcxplemrat  45174  binomcxplemnotnn0  45180  oddfl  46111  uzubioo  46395  fmuldfeq  46413  fmul01lt1lem2  46415  fmul01lt1  46416  clim1fr1  46431  sumnnodd  46460  limsup10exlem  46600  fprodsubrecnncnvlem  46735  fprodaddrecnncnvlem  46737  dvnmul  46771  stoweidlem3  46831  stoweidlem7  46835  stoweidlem11  46839  stoweidlem14  46842  stoweidlem20  46848  stoweidlem26  46854  stoweidlem34  46862  stoweidlem51  46879  wallispilem5  46897  wallispi  46898  stirlinglem1  46902  stirlinglem5  46906  stirlinglem7  46908  stirlinglem8  46909  stirlinglem10  46911  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  stirlingr  46918  fourierdlem4  46939  fourierdlem11  46946  fourierdlem26  46961  fourierdlem41  46976  fourierdlem42  46977  fourierdlem48  46982  fourierdlem49  46983  fourierdlem79  47013  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  fourierdlem112  47046  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem15  47077  etransclem28  47090  etransclem35  47097  etransclem38  47100  etransclem44  47106  etransclem48  47110  sge0ad2en  47259  voliunsge0lem  47300  caragenunicl  47352  caratheodorylem2  47355  ovolval2lem  47471  ovolval2  47472  vonioolem2  47509  vonicclem2  47512  cos5t  47743  addmodne  48238  m1modne  48242  m1modnep2mod  48246  modm2nep1  48260  modp2nep1  48261  modm1nep2  48262  modm1nem2  48263  modm1p1ne  48264  iccpartiltu  48322  iccpartgt  48327  fmtnoge3  48433  fmtnoprmfac1lem  48467  2pwp1prm  48492  sfprmdvdsmersenne  48506  lighneallem2  48509  perfectALTVlem2  48638  fpprwpprb  48656  nnsum3primesprm  48706  bgoldbtbndlem3  48723  gpgvtx0  48969  gpgprismgrusgra  48974  gpgedgvtx1  48978  gpgedg2ov  48982  gpg3nbgrvtx0  48992  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  2even  49154  fldivexpfllog2  49495  nnlog2ge0lt1  49496  logbpw2m1  49497  blenpw2m1  49509  blennnt2  49519  nnolog2flm1  49520  blennn0e2  49524  digexp  49537  dignn0flhalflem1  49545  dignn0flhalflem2  49546  veronesev1lem  50806  veronesev2lem  50807  veronesev3lem  50808  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811