Theorem 1zzd 12016

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

Syntax hints:   → wi 4   ∈ wcel 2114  1c1 10540  ℤcz 11984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-i2m1 10607  ax-1ne0 10608  ax-rrecex 10611  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-neg 10875  df-nn 11641  df-z 11985

This theorem is referenced by:  fzm1  12990  fzoss2  13068  fzo1fzo0n0  13091  elfznelfzo  13145  negmod  13287  addmodid  13290  modnegd  13297  2submod  13303  sermono  13405  seqf1olem2  13413  bcp1nk  13680  eqwrds3  14327  climuni  14911  isercoll  15026  telfsumo  15159  fsumparts  15163  binomlem  15186  climcndslem2  15207  climcnds  15208  divcnv  15210  supcvg  15213  arisum  15217  trireciplem  15219  trirecip  15220  expcnv  15221  pwdif  15225  geo2sum  15231  geo2lim  15233  geoisum1  15237  geoisum1c  15238  mertenslem1  15242  mertenslem2  15243  fprodser  15305  fprodzcl  15310  risefacval2  15366  fallfacval2  15367  binomfallfaclem2  15396  bpolydiflem  15410  ege2le3  15445  rpnnen2lem12  15580  modm1div  15621  nn0o1gt2  15734  pwp1fsum  15744  bitscmp  15789  dvdsnprmd  16036  2mulprm  16039  hashdvds  16114  phiprmpw  16115  prmdiv  16124  odzdvds  16134  odzphi  16135  iserodd  16174  pcid  16211  pcmptcl  16229  pockthlem  16243  prmreclem4  16257  prmreclem6  16259  vdwapun  16312  prmdvdsprmo  16380  prmodvdslcmf  16385  prmgapprmo  16400  gsumpr12val  17901  mulgpropd  18271  cycsubggend  18350  sylow1lem1  18725  sylow3lem6  18759  pgpfac1lem2  19199  ablsimpgfindlem1  19231  zringcyg  20640  mulgrhm2  20648  znunit  20712  znrrg  20714  frgpcyg  20722  cpmadugsumlemF  21486  lmcnp  21914  lmmo  21990  1stcelcls  22071  1stccnp  22072  1stckgenlem  22163  1stckgen  22164  clmvneg1  23705  clmmulg  23707  lmnn  23868  cmetcaulem  23893  iscmet2  23899  causs  23903  nglmle  23907  caubl  23913  iscmet3i  23917  ovolsf  24075  ovoliunlem1  24105  ovoliun  24108  ovoliun2  24109  ovolicc2lem2  24121  ovolicc2lem3  24122  ovolicc2lem4  24123  voliunlem2  24154  voliunlem3  24155  ioombl1lem4  24164  uniioombllem2  24186  uniioombllem3  24188  uniioombllem6  24191  vitalilem4  24214  itg1climres  24317  mbfi1fseqlem6  24323  mbfi1flimlem  24325  mbfmullem2  24327  itg2monolem1  24353  itg2i1fseq  24358  itg2i1fseq2  24359  itg2addlem  24361  plyeq0lem  24802  dvply1  24875  dvtaylp  24960  pserdvlem2  25018  pserdv2  25020  advlogexp  25240  logtayl  25245  logtaylsum  25246  logtayl2  25247  atantayl  25517  leibpilem2  25521  leibpi  25522  birthdaylem2  25532  dfef2  25550  divsqrtsumlem  25559  emcllem4  25578  emcllem6  25580  emcllem7  25581  zetacvg  25594  lgamgulmlem4  25611  lgamgulmlem6  25613  lgamgulm2  25615  lgamcvglem  25619  lgamcvg2  25634  gamcvg  25635  regamcl  25640  relgamcl  25641  wilthlem1  25647  wilthlem2  25648  basellem6  25665  basellem7  25666  basellem8  25667  basellem9  25668  mersenne  25805  perfectlem1  25807  perfectlem2  25808  lgslem1  25875  lgsqrlem1  25924  gausslemma2dlem4  25947  gausslemma2dlem6  25950  gausslemma2dlem7  25951  lgseisenlem1  25953  lgsquad2lem1  25962  lgsquad3  25965  m1lgs  25966  2sqlem11  26007  dchrisumlema  26066  dchrisumlem3  26069  dchrmusum2  26072  dchrvmasumiflem1  26079  dchrvmaeq0  26082  dchrisum0re  26091  dchrisum0lem1b  26093  dchrisum0lem2a  26095  logdivsum  26111  pntrlog2bndlem1  26155  pntpbnd2  26165  axlowdimlem6  26735  axlowdim  26749  upgrewlkle2  27390  redwlk  27456  pthdadjvtx  27513  pthdlem1  27549  wwlksnextproplem2  27691  clwwlkccatlem  27769  minvecolem3  28655  minvecolem4b  28657  minvecolem4  28659  h2hcau  28758  h2hlm  28759  hlimadd  28972  hhsscms  29057  occllem  29082  nlelchi  29840  opsqrlem4  29922  hmopidmchi  29930  fzm1ne1  30514  fzspl  30515  fzsplit3  30519  prmdvdsbc  30534  pfxlsw2ccat  30628  tocycfvres1  30754  tocycfvres2  30755  cycpmfvlem  30756  cycpmfv1  30757  cycpmfv2  30758  cycpmfv3  30759  cycpmcl  30760  tocyc01  30762  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmconjv  30786  cycpmrn  30787  cycpmconjslem1  30798  cycpmconjslem2  30799  archirngz  30820  archiabllem1a  30822  smatrcl  31063  submateqlem1  31074  submateqlem2  31075  mdetlap  31099  rge0scvg  31194  lmxrge0  31197  lmdvg  31198  qqhval2lem  31224  esumfsupre  31332  esumpcvgval  31339  esumcvg  31347  eulerpartlems  31620  fiblem  31658  ballotlemfp1  31751  ballotlemimin  31765  ballotlemic  31766  ballotlem1c  31767  ballotlemsdom  31771  ballotlemsel1i  31772  ballotlemsima  31775  ballotlemfrceq  31788  ballotlemfrcn0  31789  chtvalz  31902  sinccvg  32918  circum  32919  divcnvlin  32966  bcprod  32972  iprodgam  32976  faclimlem2  32978  faclim  32980  iprodfac  32981  faclim2  32982  fwddifnp1  33628  lmclim2  35035  geomcau  35036  heibor1lem  35089  heibor1  35090  bfplem1  35102  bfplem2  35103  rrncmslem  35112  rrncms  35113  fzsplit1nn0  39358  eldioph2lem1  39364  pellexlem6  39438  rmspecnonsq  39511  jm2.22  39599  jm2.23  39600  jm2.25  39603  dvradcnv2  40686  binomcxplemnn0  40688  binomcxplemrat  40689  binomcxplemnotnn0  40695  oddfl  41550  uzubioo  41850  fmuldfeq  41871  fmul01lt1lem2  41873  fmul01lt1  41874  clim1fr1  41889  sumnnodd  41918  limsup10exlem  42060  fprodsubrecnncnvlem  42198  fprodaddrecnncnvlem  42200  dvnmul  42235  stoweidlem3  42295  stoweidlem7  42299  stoweidlem11  42303  stoweidlem14  42306  stoweidlem20  42312  stoweidlem26  42318  stoweidlem34  42326  stoweidlem51  42343  wallispilem5  42361  wallispi  42362  stirlinglem1  42366  stirlinglem5  42370  stirlinglem7  42372  stirlinglem8  42373  stirlinglem10  42375  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  stirlingr  42382  fourierdlem4  42403  fourierdlem11  42410  fourierdlem26  42425  fourierdlem41  42440  fourierdlem42  42441  fourierdlem48  42446  fourierdlem49  42447  fourierdlem79  42477  fourierdlem97  42495  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  etransclem15  42541  etransclem28  42554  etransclem35  42561  etransclem38  42564  etransclem44  42570  etransclem48  42574  sge0ad2en  42720  voliunsge0lem  42761  caragenunicl  42813  caratheodorylem2  42816  ovolval2lem  42932  ovolval2  42933  vonioolem2  42970  vonicclem2  42973  iccpartiltu  43589  iccpartgt  43594  fmtnoge3  43699  fmtnoprmfac1lem  43733  2pwp1prm  43758  sfprmdvdsmersenne  43775  lighneallem2  43778  perfectALTVlem2  43894  fpprwpprb  43912  nnsum3primesprm  43962  bgoldbtbndlem3  43979  2even  44211  fldivexpfllog2  44632  nnlog2ge0lt1  44633  logbpw2m1  44634  blenpw2m1  44646  blennnt2  44656  nnolog2flm1  44657  blennn0e2  44661  digexp  44674  dignn0flhalflem1  44682  dignn0flhalflem2  44683