Theorem 1zzd 12014

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

Syntax hints:   → wi 4   ∈ wcel 2114  1c1 10538  ℤcz 11982

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 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-neg 10873  df-nn 11639  df-z 11983

This theorem is referenced by:  fzm1  12988  fzoss2  13066  fzo1fzo0n0  13089  elfznelfzo  13143  negmod  13285  addmodid  13288  modnegd  13295  2submod  13301  sermono  13403  seqf1olem2  13411  bcp1nk  13678  eqwrds3  14325  climuni  14909  isercoll  15024  telfsumo  15157  fsumparts  15161  binomlem  15184  climcndslem2  15205  climcnds  15206  divcnv  15208  supcvg  15211  arisum  15215  trireciplem  15217  trirecip  15218  expcnv  15219  pwdif  15223  geo2sum  15229  geo2lim  15231  geoisum1  15235  geoisum1c  15236  mertenslem1  15240  mertenslem2  15241  fprodser  15303  fprodzcl  15308  risefacval2  15364  fallfacval2  15365  binomfallfaclem2  15394  bpolydiflem  15408  ege2le3  15443  rpnnen2lem12  15578  modm1div  15619  nn0o1gt2  15732  pwp1fsum  15742  bitscmp  15787  dvdsnprmd  16034  2mulprm  16037  hashdvds  16112  phiprmpw  16113  prmdiv  16122  odzdvds  16132  odzphi  16133  iserodd  16172  pcid  16209  pcmptcl  16227  pockthlem  16241  prmreclem4  16255  prmreclem6  16257  vdwapun  16310  prmdvdsprmo  16378  prmodvdslcmf  16383  prmgapprmo  16398  gsumpr12val  17899  mulgpropd  18269  cycsubggend  18348  sylow1lem1  18723  sylow3lem6  18757  pgpfac1lem2  19197  ablsimpgfindlem1  19229  zringcyg  20638  mulgrhm2  20646  znunit  20710  znrrg  20712  frgpcyg  20720  cpmadugsumlemF  21484  lmcnp  21912  lmmo  21988  1stcelcls  22069  1stccnp  22070  1stckgenlem  22161  1stckgen  22162  clmvneg1  23703  clmmulg  23705  lmnn  23866  cmetcaulem  23891  iscmet2  23897  causs  23901  nglmle  23905  caubl  23911  iscmet3i  23915  ovolsf  24073  ovoliunlem1  24103  ovoliun  24106  ovoliun2  24107  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  voliunlem2  24152  voliunlem3  24153  ioombl1lem4  24162  uniioombllem2  24184  uniioombllem3  24186  uniioombllem6  24189  vitalilem4  24212  itg1climres  24315  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfmullem2  24325  itg2monolem1  24351  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  plyeq0lem  24800  dvply1  24873  dvtaylp  24958  pserdvlem2  25016  pserdv2  25018  advlogexp  25238  logtayl  25243  logtaylsum  25244  logtayl2  25245  atantayl  25515  leibpilem2  25519  leibpi  25520  birthdaylem2  25530  dfef2  25548  divsqrtsumlem  25557  emcllem4  25576  emcllem6  25578  emcllem7  25579  zetacvg  25592  lgamgulmlem4  25609  lgamgulmlem6  25611  lgamgulm2  25613  lgamcvglem  25617  lgamcvg2  25632  gamcvg  25633  regamcl  25638  relgamcl  25639  wilthlem1  25645  wilthlem2  25646  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  mersenne  25803  perfectlem1  25805  perfectlem2  25806  lgslem1  25873  lgsqrlem1  25922  gausslemma2dlem4  25945  gausslemma2dlem6  25948  gausslemma2dlem7  25949  lgseisenlem1  25951  lgsquad2lem1  25960  lgsquad3  25963  m1lgs  25964  2sqlem11  26005  dchrisumlema  26064  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumiflem1  26077  dchrvmaeq0  26080  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem2a  26093  logdivsum  26109  pntrlog2bndlem1  26153  pntpbnd2  26163  axlowdimlem6  26733  axlowdim  26747  upgrewlkle2  27388  redwlk  27454  pthdadjvtx  27511  pthdlem1  27547  wwlksnextproplem2  27689  clwwlkccatlem  27767  minvecolem3  28653  minvecolem4b  28655  minvecolem4  28657  h2hcau  28756  h2hlm  28757  hlimadd  28970  hhsscms  29055  occllem  29080  nlelchi  29838  opsqrlem4  29920  hmopidmchi  29928  fzm1ne1  30512  fzspl  30513  fzsplit3  30517  prmdvdsbc  30532  pfxlsw2ccat  30626  tocycfvres1  30752  tocycfvres2  30753  cycpmfvlem  30754  cycpmfv1  30755  cycpmfv2  30756  cycpmfv3  30757  cycpmcl  30758  tocyc01  30760  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmconjv  30784  cycpmrn  30785  cycpmconjslem1  30796  cycpmconjslem2  30797  archirngz  30818  archiabllem1a  30820  smatrcl  31061  submateqlem1  31072  submateqlem2  31073  mdetlap  31097  rge0scvg  31192  lmxrge0  31195  lmdvg  31196  qqhval2lem  31222  esumfsupre  31330  esumpcvgval  31337  esumcvg  31345  eulerpartlems  31618  fiblem  31656  ballotlemfp1  31749  ballotlemimin  31763  ballotlemic  31764  ballotlem1c  31765  ballotlemsdom  31769  ballotlemsel1i  31770  ballotlemsima  31773  ballotlemfrceq  31786  ballotlemfrcn0  31787  chtvalz  31900  sinccvg  32916  circum  32917  divcnvlin  32964  bcprod  32970  iprodgam  32974  faclimlem2  32976  faclim  32978  iprodfac  32979  faclim2  32980  fwddifnp1  33626  lmclim2  35048  geomcau  35049  heibor1lem  35102  heibor1  35103  bfplem1  35115  bfplem2  35116  rrncmslem  35125  rrncms  35126  fzsplit1nn0  39371  eldioph2lem1  39377  pellexlem6  39451  rmspecnonsq  39524  jm2.22  39612  jm2.23  39613  jm2.25  39616  dvradcnv2  40699  binomcxplemnn0  40701  binomcxplemrat  40702  binomcxplemnotnn0  40708  oddfl  41563  uzubioo  41863  fmuldfeq  41884  fmul01lt1lem2  41886  fmul01lt1  41887  clim1fr1  41902  sumnnodd  41931  limsup10exlem  42073  fprodsubrecnncnvlem  42211  fprodaddrecnncnvlem  42213  dvnmul  42248  stoweidlem3  42308  stoweidlem7  42312  stoweidlem11  42316  stoweidlem14  42319  stoweidlem20  42325  stoweidlem26  42331  stoweidlem34  42339  stoweidlem51  42356  wallispilem5  42374  wallispi  42375  stirlinglem1  42379  stirlinglem5  42383  stirlinglem7  42385  stirlinglem8  42386  stirlinglem10  42388  stirlinglem12  42390  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  stirlingr  42395  fourierdlem4  42416  fourierdlem11  42423  fourierdlem26  42438  fourierdlem41  42453  fourierdlem42  42454  fourierdlem48  42459  fourierdlem49  42460  fourierdlem79  42490  fourierdlem97  42508  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  sqwvfoura  42533  sqwvfourb  42534  fouriersw  42536  etransclem15  42554  etransclem28  42567  etransclem35  42574  etransclem38  42577  etransclem44  42583  etransclem48  42587  sge0ad2en  42733  voliunsge0lem  42774  caragenunicl  42826  caratheodorylem2  42829  ovolval2lem  42945  ovolval2  42946  vonioolem2  42983  vonicclem2  42986  iccpartiltu  43602  iccpartgt  43607  fmtnoge3  43712  fmtnoprmfac1lem  43746  2pwp1prm  43771  sfprmdvdsmersenne  43788  lighneallem2  43791  perfectALTVlem2  43907  fpprwpprb  43925  nnsum3primesprm  43975  bgoldbtbndlem3  43992  2even  44224  fldivexpfllog2  44645  nnlog2ge0lt1  44646  logbpw2m1  44647  blenpw2m1  44659  blennnt2  44669  nnolog2flm1  44670  blennn0e2  44674  digexp  44687  dignn0flhalflem1  44695  dignn0flhalflem2  44696