Theorem 1zzd 12281

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

Syntax hints:   → wi 4   ∈ wcel 2108  1c1 10803  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-neg 11138  df-nn 11904  df-z 12250

This theorem is referenced by:  fzm1  13265  fzoss2  13343  fzo1fzo0n0  13366  elfznelfzo  13420  negmod  13564  addmodid  13567  modnegd  13574  2submod  13580  sermono  13683  seqf1olem2  13691  bcp1nk  13959  eqwrds3  14604  climuni  15189  isercoll  15307  telfsumo  15442  fsumparts  15446  binomlem  15469  climcndslem2  15490  climcnds  15491  divcnv  15493  supcvg  15496  arisum  15500  trireciplem  15502  trirecip  15503  expcnv  15504  pwdif  15508  geo2sum  15513  geo2lim  15515  geoisum1  15519  geoisum1c  15520  mertenslem1  15524  mertenslem2  15525  fprodser  15587  fprodzcl  15592  risefacval2  15648  fallfacval2  15649  binomfallfaclem2  15678  bpolydiflem  15692  ege2le3  15727  rpnnen2lem12  15862  modm1div  15903  nn0o1gt2  16018  pwp1fsum  16028  bitscmp  16073  dvdsnprmd  16323  2mulprm  16326  hashdvds  16404  phiprmpw  16405  prmdiv  16414  odzdvds  16424  odzphi  16425  iserodd  16464  pcid  16502  pcmptcl  16520  pockthlem  16534  prmreclem4  16548  prmreclem6  16550  vdwapun  16603  prmdvdsprmo  16671  prmodvdslcmf  16676  prmgapprmo  16691  gsumpr12val  18288  mulgpropd  18660  cycsubggend  18739  sylow1lem1  19118  sylow3lem6  19152  pgpfac1lem2  19593  ablsimpgfindlem1  19625  zringcyg  20603  mulgrhm2  20612  znunit  20683  znrrg  20685  frgpcyg  20693  cpmadugsumlemF  21933  lmcnp  22363  lmmo  22439  1stcelcls  22520  1stccnp  22521  1stckgenlem  22612  1stckgen  22613  clmvneg1  24168  clmmulg  24170  lmnn  24332  cmetcaulem  24357  iscmet2  24363  causs  24367  nglmle  24371  caubl  24377  iscmet3i  24381  ovolsf  24541  ovoliunlem1  24571  ovoliun  24574  ovoliun2  24575  ovolicc2lem2  24587  ovolicc2lem3  24588  ovolicc2lem4  24589  voliunlem2  24620  voliunlem3  24621  ioombl1lem4  24630  uniioombllem2  24652  uniioombllem3  24654  uniioombllem6  24657  vitalilem4  24680  itg1climres  24784  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfmullem2  24794  itg2monolem1  24820  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  plyeq0lem  25276  dvply1  25349  dvtaylp  25434  pserdvlem2  25492  pserdv2  25494  advlogexp  25715  logtayl  25720  logtaylsum  25721  logtayl2  25722  atantayl  25992  leibpilem2  25996  leibpi  25997  birthdaylem2  26007  dfef2  26025  divsqrtsumlem  26034  emcllem4  26053  emcllem6  26055  emcllem7  26056  zetacvg  26069  lgamgulmlem4  26086  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvglem  26094  lgamcvg2  26109  gamcvg  26110  regamcl  26115  relgamcl  26116  wilthlem1  26122  wilthlem2  26123  basellem6  26140  basellem7  26141  basellem8  26142  basellem9  26143  mersenne  26280  perfectlem1  26282  perfectlem2  26283  lgslem1  26350  lgsqrlem1  26399  gausslemma2dlem4  26422  gausslemma2dlem6  26425  gausslemma2dlem7  26426  lgseisenlem1  26428  lgsquad2lem1  26437  lgsquad3  26440  m1lgs  26441  2sqlem11  26482  dchrisumlema  26541  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem2a  26570  logdivsum  26586  pntrlog2bndlem1  26630  pntpbnd2  26640  axlowdimlem6  27218  axlowdim  27232  upgrewlkle2  27876  redwlk  27942  pthdadjvtx  27999  pthdlem1  28035  wwlksnextproplem2  28176  clwwlkccatlem  28254  minvecolem3  29139  minvecolem4b  29141  minvecolem4  29143  h2hcau  29242  h2hlm  29243  hlimadd  29456  hhsscms  29541  occllem  29566  nlelchi  30324  opsqrlem4  30406  hmopidmchi  30414  fzm1ne1  31012  fzspl  31013  fzsplit3  31017  prmdvdsbc  31032  pfxlsw2ccat  31126  tocycfvres1  31279  tocycfvres2  31280  cycpmfvlem  31281  cycpmfv1  31282  cycpmfv2  31283  cycpmfv3  31284  cycpmcl  31285  tocyc01  31287  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmconjv  31311  cycpmrn  31312  cycpmconjslem1  31323  cycpmconjslem2  31324  archirngz  31345  archiabllem1a  31347  smatrcl  31648  submateqlem1  31659  submateqlem2  31660  mdetlap  31684  rge0scvg  31801  lmxrge0  31804  lmdvg  31805  qqhval2lem  31831  esumfsupre  31939  esumpcvgval  31946  esumcvg  31954  eulerpartlems  32227  fiblem  32265  ballotlemfp1  32358  ballotlemimin  32372  ballotlemic  32373  ballotlem1c  32374  ballotlemsdom  32378  ballotlemsel1i  32379  ballotlemsima  32382  ballotlemfrceq  32395  ballotlemfrcn0  32396  chtvalz  32509  sinccvg  33531  circum  33532  divcnvlin  33604  bcprod  33610  iprodgam  33614  faclimlem2  33616  faclim  33618  iprodfac  33619  faclim2  33620  fwddifnp1  34394  lmclim2  35843  geomcau  35844  heibor1lem  35894  heibor1  35895  bfplem1  35907  bfplem2  35908  rrncmslem  35917  rrncms  35918  fzsplitnd  39919  lcmineqlem4  39968  lcmineqlem13  39977  lcmineqlem23  39987  dvrelogpow2b  40004  aks4d1p1p7  40010  aks4d1p1  40012  aks4d1p3  40014  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  sticksstones6  40035  sticksstones7  40036  sticksstones9  40038  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  metakunt1  40053  metakunt2  40054  metakunt3  40055  metakunt5  40057  metakunt7  40059  metakunt10  40062  metakunt15  40067  metakunt16  40068  metakunt19  40071  metakunt21  40073  metakunt22  40074  metakunt24  40076  metakunt25  40077  metakunt26  40078  metakunt28  40080  metakunt29  40081  metakunt30  40082  metakunt32  40084  metakunt33  40085  fzsplit1nn0  40492  eldioph2lem1  40498  pellexlem6  40572  rmspecnonsq  40645  jm2.22  40733  jm2.23  40734  jm2.25  40737  dvradcnv2  41854  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemnotnn0  41863  oddfl  42705  uzubioo  42995  fmuldfeq  43014  fmul01lt1lem2  43016  fmul01lt1  43017  clim1fr1  43032  sumnnodd  43061  limsup10exlem  43203  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvnmul  43374  stoweidlem3  43434  stoweidlem7  43438  stoweidlem11  43442  stoweidlem14  43445  stoweidlem20  43451  stoweidlem26  43457  stoweidlem34  43465  stoweidlem51  43482  wallispilem5  43500  wallispi  43501  stirlinglem1  43505  stirlinglem5  43509  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  fourierdlem4  43542  fourierdlem11  43549  fourierdlem26  43564  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem79  43616  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  etransclem15  43680  etransclem28  43693  etransclem35  43700  etransclem38  43703  etransclem44  43709  etransclem48  43713  sge0ad2en  43859  voliunsge0lem  43900  caragenunicl  43952  caratheodorylem2  43955  ovolval2lem  44071  ovolval2  44072  vonioolem2  44109  vonicclem2  44112  iccpartiltu  44762  iccpartgt  44767  fmtnoge3  44870  fmtnoprmfac1lem  44904  2pwp1prm  44929  sfprmdvdsmersenne  44943  lighneallem2  44946  perfectALTVlem2  45062  fpprwpprb  45080  nnsum3primesprm  45130  bgoldbtbndlem3  45147  2even  45379  fldivexpfllog2  45799  nnlog2ge0lt1  45800  logbpw2m1  45801  blenpw2m1  45813  blennnt2  45823  nnolog2flm1  45824  blennn0e2  45828  digexp  45841  dignn0flhalflem1  45849  dignn0flhalflem2  45850