Theorem 1zzd 12734

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  1c1 11208  ℤcz 12700

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rrecex 11279  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-neg 11551  df-nn 12343  df-z 12701

This theorem is used by:  fzm1  13748  fzoss2  13829  fzo1fzo0n0  13857  elfznelfzo  13915  negmod  14066  addmodid  14069  modnegd  14076  2submod  14082  sermono  14184  seqf1olem2  14192  bcp1nk  14468  eqwrds3  15123  climuni  15728  isercoll  15844  telfsumo  15978  fsumparts  15982  binomlem  16007  climcndslem2  16028  climcnds  16029  divcnv  16031  supcvg  16034  arisum  16038  trireciplem  16040  trirecip  16041  expcnv  16042  pwdif  16046  geo2sum  16051  geo2lim  16053  geoisum1  16057  geoisum1c  16058  mertenslem1  16062  mertenslem2  16063  fprodser  16125  fprodzcl  16130  risefacval2  16186  fallfacval2  16187  binomfallfaclem2  16215  bpolydiflem  16229  ege2le3  16265  rpnnen2lem12  16402  modm1div  16443  nn0o1gt2  16560  pwp1fsum  16570  bitscmp  16617  dvdsnprmd  16874  2mulprm  16877  prmdvdsbc  16911  hashdvds  16961  phiprmpw  16962  prmdiv  16971  odzdvds  16982  odzphi  16983  iserodd  17022  pcid  17060  pcmptcl  17078  pockthlem  17092  prmreclem4  17106  prmreclem6  17108  vdwapun  17161  prmdvdsprmo  17229  prmodvdslcmf  17234  prmgapprmo  17249  chnub  18805  gsumpr12val  18887  mulgpropd  19335  cycsubggend  19429  odm1inv  19776  sylow1lem1  19821  sylow3lem6  19855  pgpfac1lem2  20300  ablsimpgfindlem1  20332  zringcyg  21784  mulgrhm2  21793  pzriprnglem6  21801  znunit  21878  znrrg  21880  frgpcyg  21888  cpmadugsumlemF  23203  lmcnp  23631  lmmo  23707  1stcelcls  23789  1stccnp  23790  1stckgenlem  23881  1stckgen  23882  clmvneg1  25429  clmmulg  25431  lmnn  25593  cmetcaulem  25618  iscmet2  25624  causs  25628  nglmle  25632  caubl  25638  iscmet3i  25642  ovolsf  25802  ovoliunlem1  25832  ovoliun  25835  ovoliun2  25836  ovolicc2lem2  25848  ovolicc2lem3  25849  ovolicc2lem4  25850  voliunlem2  25881  voliunlem3  25882  ioombl1lem4  25891  uniioombllem2  25913  uniioombllem3  25915  uniioombllem6  25918  vitalilem4  25941  itg1climres  26044  mbfi1fseqlem6  26050  mbfi1flimlem  26052  mbfmullem2  26054  itg2monolem1  26080  itg2i1fseq  26085  itg2i1fseq2  26086  itg2addlem  26088  plyeq0lem  26538  dvply1  26614  dvtaylp  26706  pserdvlem2  26764  pserdv2  26766  advlogexp  26992  logtayl  26997  logtaylsum  26998  logtayl2  26999  atantayl  27274  leibpilem2  27278  leibpi  27279  birthdaylem2  27289  dfef2  27307  divsqrtsumlem  27316  emcllem4  27335  emcllem6  27337  emcllem7  27338  zetacvg  27351  lgamgulmlem4  27368  lgamgulmlem6  27370  lgamgulm2  27372  lgamcvglem  27376  lgamcvg2  27391  gamcvg  27392  regamcl  27397  relgamcl  27398  wilthlem1  27404  wilthlem2  27405  basellem6  27422  basellem7  27423  basellem8  27424  basellem9  27425  ppiub  27540  mersenne  27563  perfectlem1  27565  perfectlem2  27566  lgslem1  27633  lgsqrlem1  27682  gausslemma2dlem4  27705  gausslemma2dlem6  27708  gausslemma2dlem7  27709  lgseisenlem1  27711  lgsquad2lem1  27720  lgsquad3  27723  m1lgs  27724  2sqlem11  27765  dchrisumlema  27824  dchrisumlem3  27827  dchrmusum2  27830  dchrvmasumiflem1  27837  dchrvmaeq0  27840  dchrisum0re  27849  dchrisum0lem1b  27851  dchrisum0lem2a  27853  logdivsum  27869  pntrlog2bndlem1  27913  pntpbnd2  27923  fltoprmlem2  28003  axlowdimlem6  29534  axlowdim  29548  upgrewlkle2  30196  redwlk  30260  pthdadjvtx  30322  pthdlem1  30361  wwlksnextproplem2  30508  clwwlkccatlem  30589  minvecolem3  31487  minvecolem4b  31489  minvecolem4  31491  h2hcau  31590  h2hlm  31591  hlimadd  31804  hhsscms  31889  occllem  31914  nlelchi  32672  opsqrlem4  32754  hmopidmchi  32762  fzm1ne1  33430  fzspl  33431  fzsplit3  33435  pfxlsw2ccat  33563  tocycfvres1  33721  tocycfvres2  33722  cycpmfvlem  33723  cycpmfv1  33724  cycpmfv2  33725  cycpmfv3  33726  cycpmcl  33727  tocyc01  33729  cycpmco2lem6  33742  cycpmco2lem7  33743  cycpmconjv  33753  cycpmrn  33754  cycpmconjslem1  33765  cycpmconjslem2  33766  archirngz  33800  archiabllem1a  33802  elrgspnlem2  33854  elrgspnlem3  33855  elrgspnsubrunlem1  33858  zringfrac  34136  esplyfval0  34246  esplympl  34249  esplyfval3  34254  vieta  34262  rtelextdg2  34409  constrrecl  34451  constrimcl  34452  constrmulcl  34453  constrreinvcl  34454  constrinvcl  34455  constrsdrg  34457  constrresqrtcl  34459  constrabscl  34460  cos9thpiminplylem2  34465  cos9thpiminplylem6  34469  cos9thpiminply  34470  cos9thpinconstrlem1  34471  smatrcl  34478  submateqlem1  34489  submateqlem2  34490  mdetlap  34514  rge0scvg  34631  lmxrge0  34634  lmdvg  34635  zrhcntr  34661  qqhval2lem  34663  esumfsupre  34753  esumpcvgval  34760  esumcvg  34768  eulerpartlems  35042  fiblem  35080  ballotlemfp1  35174  ballotlemimin  35188  ballotlemic  35189  ballotlem1c  35190  ballotlemsdom  35194  ballotlemsel1i  35195  ballotlemsima  35198  ballotlemfrceq  35211  ballotlemfrcn0  35212  chtvalz  35308  sinccvg  36528  circum  36529  divcnvlin  36594  bcprod  36599  iprodgam  36603  faclimlem2  36605  faclim  36607  iprodfac  36608  faclim2  36609  fwddifnp1  37026  lmclim2  38801  geomcau  38802  heibor1lem  38852  heibor1  38853  bfplem1  38865  bfplem2  38866  rrncmslem  38875  rrncms  38876  fzsplitnd  43141  lcmineqlem4  43191  lcmineqlem13  43200  lcmineqlem23  43210  dvrelogpow2b  43227  aks4d1p1p7  43233  aks4d1p1  43235  aks4d1p3  43237  aks4d1p5  43239  aks4d1p7  43242  aks4d1p8d2  43244  aks4d1p8  43246  aks4d1p9  43247  primrootscoprbij  43261  primrootspoweq0  43265  hashscontpow1  43280  aks6d1c5lem1  43295  sticksstones6  43310  sticksstones7  43311  sticksstones9  43313  sticksstones10  43314  sticksstones11  43315  sticksstones12a  43316  sticksstones12  43317  aks6d1c6lem3  43331  aks6d1c6lem4  43332  aks6d1c7lem1  43339  aks6d1c7lem2  43340  grpods  43353  unitscyglem2  43355  unitscyglem4  43357  unitscyglem5  43358  fzsplit1nn0  43874  eldioph2lem1  43880  pellexlem6  43950  rmspecnonsq  44023  jm2.22  44111  jm2.23  44112  jm2.25  44115  dvradcnv2  45440  binomcxplemnn0  45442  binomcxplemrat  45443  binomcxplemnotnn0  45449  oddfl  46402  uzubioo  46685  fmuldfeq  46703  fmul01lt1lem2  46705  fmul01lt1  46706  clim1fr1  46721  sumnnodd  46750  limsup10exlem  46890  fprodsubrecnncnvlem  47025  fprodaddrecnncnvlem  47027  dvnmul  47061  stoweidlem3  47121  stoweidlem7  47125  stoweidlem11  47129  stoweidlem14  47132  stoweidlem20  47138  stoweidlem26  47144  stoweidlem34  47152  stoweidlem51  47169  wallispilem5  47187  wallispi  47188  stirlinglem1  47192  stirlinglem5  47196  stirlinglem7  47198  stirlinglem8  47199  stirlinglem10  47201  stirlinglem12  47203  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  stirlingr  47208  fourierdlem4  47229  fourierdlem11  47236  fourierdlem26  47251  fourierdlem41  47266  fourierdlem42  47267  fourierdlem48  47272  fourierdlem49  47273  fourierdlem79  47303  fourierdlem97  47321  fourierdlem103  47327  fourierdlem104  47328  fourierdlem112  47336  sqwvfoura  47346  sqwvfourb  47347  fouriersw  47349  etransclem15  47367  etransclem28  47380  etransclem35  47387  etransclem38  47390  etransclem44  47396  etransclem48  47400  sge0ad2en  47549  voliunsge0lem  47590  caragenunicl  47642  caratheodorylem2  47645  ovolval2lem  47761  ovolval2  47762  vonioolem2  47799  vonicclem2  47802  cos5t  48033  addmodne  48528  m1modne  48532  m1modnep2mod  48536  modm2nep1  48550  modp2nep1  48551  modm1nep2  48552  modm1nem2  48553  modm1p1ne  48554  iccpartiltu  48612  iccpartgt  48617  fmtnoge3  48723  fmtnoprmfac1lem  48757  2pwp1prm  48782  sfprmdvdsmersenne  48796  lighneallem2  48799  perfectALTVlem2  48928  fpprwpprb  48946  nnsum3primesprm  48996  bgoldbtbndlem3  49013  gpgvtx0  49259  gpgprismgrusgra  49264  gpgedgvtx1  49268  gpgedg2ov  49272  gpg3nbgrvtx0  49282  pgnbgreunbgrlem2lem1  49320  pgnbgreunbgrlem2lem2  49321  2even  49444  fldivexpfllog2  49785  nnlog2ge0lt1  49786  logbpw2m1  49787  blenpw2m1  49799  blennnt2  49809  nnolog2flm1  49810  blennn0e2  49814  digexp  49827  dignn0flhalflem1  49835  dignn0flhalflem2  49836  veronesev1lem  51156  veronesev2lem  51157  veronesev3lem  51158  veronesev4lem  51159  veronesev5lem  51160  veronesev6lem  51161