Theorem 1zzd 12173

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

Syntax hints:   → wi 4   ∈ wcel 2112  1c1 10695  ℤcz 12141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-neg 11030  df-nn 11796  df-z 12142

This theorem is referenced by:  fzm1  13157  fzoss2  13235  fzo1fzo0n0  13258  elfznelfzo  13312  negmod  13454  addmodid  13457  modnegd  13464  2submod  13470  sermono  13573  seqf1olem2  13581  bcp1nk  13848  eqwrds3  14493  climuni  15078  isercoll  15196  telfsumo  15329  fsumparts  15333  binomlem  15356  climcndslem2  15377  climcnds  15378  divcnv  15380  supcvg  15383  arisum  15387  trireciplem  15389  trirecip  15390  expcnv  15391  pwdif  15395  geo2sum  15400  geo2lim  15402  geoisum1  15406  geoisum1c  15407  mertenslem1  15411  mertenslem2  15412  fprodser  15474  fprodzcl  15479  risefacval2  15535  fallfacval2  15536  binomfallfaclem2  15565  bpolydiflem  15579  ege2le3  15614  rpnnen2lem12  15749  modm1div  15790  nn0o1gt2  15905  pwp1fsum  15915  bitscmp  15960  dvdsnprmd  16210  2mulprm  16213  hashdvds  16291  phiprmpw  16292  prmdiv  16301  odzdvds  16311  odzphi  16312  iserodd  16351  pcid  16389  pcmptcl  16407  pockthlem  16421  prmreclem4  16435  prmreclem6  16437  vdwapun  16490  prmdvdsprmo  16558  prmodvdslcmf  16563  prmgapprmo  16578  gsumpr12val  18115  mulgpropd  18487  cycsubggend  18566  sylow1lem1  18941  sylow3lem6  18975  pgpfac1lem2  19416  ablsimpgfindlem1  19448  zringcyg  20410  mulgrhm2  20419  znunit  20482  znrrg  20484  frgpcyg  20492  cpmadugsumlemF  21727  lmcnp  22155  lmmo  22231  1stcelcls  22312  1stccnp  22313  1stckgenlem  22404  1stckgen  22405  clmvneg1  23950  clmmulg  23952  lmnn  24114  cmetcaulem  24139  iscmet2  24145  causs  24149  nglmle  24153  caubl  24159  iscmet3i  24163  ovolsf  24323  ovoliunlem1  24353  ovoliun  24356  ovoliun2  24357  ovolicc2lem2  24369  ovolicc2lem3  24370  ovolicc2lem4  24371  voliunlem2  24402  voliunlem3  24403  ioombl1lem4  24412  uniioombllem2  24434  uniioombllem3  24436  uniioombllem6  24439  vitalilem4  24462  itg1climres  24566  mbfi1fseqlem6  24572  mbfi1flimlem  24574  mbfmullem2  24576  itg2monolem1  24602  itg2i1fseq  24607  itg2i1fseq2  24608  itg2addlem  24610  plyeq0lem  25058  dvply1  25131  dvtaylp  25216  pserdvlem2  25274  pserdv2  25276  advlogexp  25497  logtayl  25502  logtaylsum  25503  logtayl2  25504  atantayl  25774  leibpilem2  25778  leibpi  25779  birthdaylem2  25789  dfef2  25807  divsqrtsumlem  25816  emcllem4  25835  emcllem6  25837  emcllem7  25838  zetacvg  25851  lgamgulmlem4  25868  lgamgulmlem6  25870  lgamgulm2  25872  lgamcvglem  25876  lgamcvg2  25891  gamcvg  25892  regamcl  25897  relgamcl  25898  wilthlem1  25904  wilthlem2  25905  basellem6  25922  basellem7  25923  basellem8  25924  basellem9  25925  mersenne  26062  perfectlem1  26064  perfectlem2  26065  lgslem1  26132  lgsqrlem1  26181  gausslemma2dlem4  26204  gausslemma2dlem6  26207  gausslemma2dlem7  26208  lgseisenlem1  26210  lgsquad2lem1  26219  lgsquad3  26222  m1lgs  26223  2sqlem11  26264  dchrisumlema  26323  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasumiflem1  26336  dchrvmaeq0  26339  dchrisum0re  26348  dchrisum0lem1b  26350  dchrisum0lem2a  26352  logdivsum  26368  pntrlog2bndlem1  26412  pntpbnd2  26422  axlowdimlem6  26992  axlowdim  27006  upgrewlkle2  27648  redwlk  27714  pthdadjvtx  27771  pthdlem1  27807  wwlksnextproplem2  27948  clwwlkccatlem  28026  minvecolem3  28911  minvecolem4b  28913  minvecolem4  28915  h2hcau  29014  h2hlm  29015  hlimadd  29228  hhsscms  29313  occllem  29338  nlelchi  30096  opsqrlem4  30178  hmopidmchi  30186  fzm1ne1  30784  fzspl  30785  fzsplit3  30789  prmdvdsbc  30804  pfxlsw2ccat  30898  tocycfvres1  31050  tocycfvres2  31051  cycpmfvlem  31052  cycpmfv1  31053  cycpmfv2  31054  cycpmfv3  31055  cycpmcl  31056  tocyc01  31058  cycpmco2lem6  31071  cycpmco2lem7  31072  cycpmconjv  31082  cycpmrn  31083  cycpmconjslem1  31094  cycpmconjslem2  31095  archirngz  31116  archiabllem1a  31118  smatrcl  31414  submateqlem1  31425  submateqlem2  31426  mdetlap  31450  rge0scvg  31567  lmxrge0  31570  lmdvg  31571  qqhval2lem  31597  esumfsupre  31705  esumpcvgval  31712  esumcvg  31720  eulerpartlems  31993  fiblem  32031  ballotlemfp1  32124  ballotlemimin  32138  ballotlemic  32139  ballotlem1c  32140  ballotlemsdom  32144  ballotlemsel1i  32145  ballotlemsima  32148  ballotlemfrceq  32161  ballotlemfrcn0  32162  chtvalz  32275  sinccvg  33298  circum  33299  divcnvlin  33367  bcprod  33373  iprodgam  33377  faclimlem2  33379  faclim  33381  iprodfac  33382  faclim2  33383  fwddifnp1  34153  lmclim2  35602  geomcau  35603  heibor1lem  35653  heibor1  35654  bfplem1  35666  bfplem2  35667  rrncmslem  35676  rrncms  35677  fzsplitnd  39674  lcmineqlem4  39723  lcmineqlem13  39732  lcmineqlem23  39742  dvrelogpow2b  39758  aks4d1p1p7  39764  aks4d1p1  39766  sticksstones6  39776  sticksstones7  39777  sticksstones9  39779  sticksstones10  39780  sticksstones11  39781  sticksstones12a  39782  sticksstones12  39783  metakunt1  39788  metakunt2  39789  metakunt3  39790  metakunt5  39792  metakunt7  39794  metakunt10  39797  metakunt15  39802  metakunt16  39803  metakunt19  39806  metakunt21  39808  metakunt22  39809  metakunt24  39811  metakunt25  39812  metakunt26  39813  metakunt28  39815  metakunt29  39816  metakunt30  39817  metakunt32  39819  metakunt33  39820  fzsplit1nn0  40220  eldioph2lem1  40226  pellexlem6  40300  rmspecnonsq  40373  jm2.22  40461  jm2.23  40462  jm2.25  40465  dvradcnv2  41579  binomcxplemnn0  41581  binomcxplemrat  41582  binomcxplemnotnn0  41588  oddfl  42429  uzubioo  42721  fmuldfeq  42742  fmul01lt1lem2  42744  fmul01lt1  42745  clim1fr1  42760  sumnnodd  42789  limsup10exlem  42931  fprodsubrecnncnvlem  43066  fprodaddrecnncnvlem  43068  dvnmul  43102  stoweidlem3  43162  stoweidlem7  43166  stoweidlem11  43170  stoweidlem14  43173  stoweidlem20  43179  stoweidlem26  43185  stoweidlem34  43193  stoweidlem51  43210  wallispilem5  43228  wallispi  43229  stirlinglem1  43233  stirlinglem5  43237  stirlinglem7  43239  stirlinglem8  43240  stirlinglem10  43242  stirlinglem12  43244  stirlinglem13  43245  stirlinglem14  43246  stirlinglem15  43247  stirlingr  43249  fourierdlem4  43270  fourierdlem11  43277  fourierdlem26  43292  fourierdlem41  43307  fourierdlem42  43308  fourierdlem48  43313  fourierdlem49  43314  fourierdlem79  43344  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  sqwvfoura  43387  sqwvfourb  43388  fouriersw  43390  etransclem15  43408  etransclem28  43421  etransclem35  43428  etransclem38  43431  etransclem44  43437  etransclem48  43441  sge0ad2en  43587  voliunsge0lem  43628  caragenunicl  43680  caratheodorylem2  43683  ovolval2lem  43799  ovolval2  43800  vonioolem2  43837  vonicclem2  43840  iccpartiltu  44490  iccpartgt  44495  fmtnoge3  44598  fmtnoprmfac1lem  44632  2pwp1prm  44657  sfprmdvdsmersenne  44671  lighneallem2  44674  perfectALTVlem2  44790  fpprwpprb  44808  nnsum3primesprm  44858  bgoldbtbndlem3  44875  2even  45107  fldivexpfllog2  45527  nnlog2ge0lt1  45528  logbpw2m1  45529  blenpw2m1  45541  blennnt2  45551  nnolog2flm1  45552  blennn0e2  45556  digexp  45569  dignn0flhalflem1  45577  dignn0flhalflem2  45578