Theorem 2z 12632

Description: 2 is an integer. (Contributed by NM, 10-May-2004.)

Assertion

Ref	Expression
2z	⊢ 2 ∈ ℤ

Proof of Theorem 2z

Step	Hyp	Ref	Expression
1		2nn 12320	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 12624	1 ⊢ 2 ∈ ℤ

This proof depends on syntax axioms:   ∈ wcel 2142  2c2 12301  ℤcz 12597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-neg 11450  df-nn 12240  df-2 12309  df-z 12598

This theorem is used by:  nn0lt2  12665  nn0le2is012  12666  zadd2cl  12714  2eluzge1  12912  uzuzle23  12914  uzuzle24  12915  eluz2b1  12949  nn01to3  12971  nn0ge2m1nnALT  12972  ige2m1fz  13652  fz0to3un2pr  13664  fz0to4untppr  13665  fz0to5un2tp  13666  fzctr  13675  fzo0to2pr  13786  fzo0to42pr  13789  2tnp1ge0ge0  13869  flhalf  13870  m1modge3gt1  13961  2txmodxeq0  13974  f13idfv  14043  sqrecd  14193  znsqcld  14205  sq1  14238  expnass  14251  sqoddm1div8  14286  bcn2m1  14367  bcn2p1  14368  4bc2eq6  14372  hashtpg  14529  ccat2s1p2  14675  pfxtrcfv0  14738  pfxtrcfvl  14741  eqwrds3  15005  iseraltlem2  15741  iseraltlem3  15742  climcndslem1  15910  climcnds  15912  bpolydiflem  16114  efgt0  16165  tanval3  16196  cos01bnd  16248  cos01gt0  16253  odd2np1  16405  even2n  16406  oddm1even  16407  oddp1even  16408  oexpneg  16409  mod2eq1n2dvds  16411  2tp1odd  16416  2teven  16419  evend2  16421  oddp1d2  16422  ltoddhalfle  16425  opoe  16427  omoe  16428  opeo  16429  omeo  16430  z0even  16431  z2even  16434  z4even  16436  4dvdseven  16437  m1expo  16439  m1exp1  16440  nn0o  16447  sumeven  16451  flodddiv4  16479  bits0e  16493  bits0o  16494  bitsp1e  16496  bitsp1o  16497  bitsfzo  16499  bitsmod  16500  bitscmp  16502  bitsinv1lem  16505  bitsinv1  16506  6gcd4e2  16602  3lcm2e6woprm  16679  lcmf2a3a4e12  16711  isprm3  16747  dvdsnprmd  16754  2prm  16756  2mulprm  16757  oddprmge3  16765  ge2nprmge4  16766  isprm7  16773  divgcdodd  16775  oddprm  16876  pythagtriplem4  16885  pythagtriplem11  16891  pythagtriplem13  16893  iserodd  16901  prmgaplem3  17119  prmgaplem7  17123  dec2dvds  17129  prmlem0  17171  4001lem1  17207  ex-chn1  18699  psgnunilem4  19573  efgredleme  19819  lt6abl  19971  ablsimpgfindlem1  20185  ablsimpgfindlem2  20186  zringndrg  21629  znidomb  21722  chfacfscmulfsupp  23027  chfacfpmmulfsupp  23031  minveclem2  25596  minveclem3  25599  pjthlem1  25607  dyaddisjlem  25765  mbfi1fseqlem5  25889  dvrecg  26143  dvexp3  26148  aaliou3lem6  26522  tanregt0  26715  efif1olem4  26721  tanarg  26795  cxpsqrtth  26906  2irrexpq  26907  2logb9irr  26971  2logb9irrALT  26974  sqrt2cxp2logb9e3  26975  cubic2  27024  asinlem3  27047  atantayl2  27114  cxp2limlem  27151  lgamgulmlem3  27206  lgamgulmlem4  27207  basellem2  27257  basellem3  27258  basellem4  27259  basellem5  27260  basellem8  27263  basellem9  27264  ppisval  27279  ppiprm  27326  ppinprm  27327  chtprm  27328  chtnprm  27329  chtdif  27333  ppidif  27338  ppi1  27339  cht1  27340  cht3  27348  ppieq0  27351  ppiublem1  27377  chpeq0  27383  chtub  27387  chpval2  27393  chpub  27395  mersenne  27402  perfect1  27403  perfectlem1  27404  perfectlem2  27405  bposlem1  27459  bposlem2  27460  bposlem3  27461  bposlem5  27463  bposlem6  27464  lgslem1  27472  lgsdir2lem2  27501  lgsdir2  27505  lgsqr  27526  gausslemma2dlem0i  27539  gausslemma2dlem1a  27540  gausslemma2dlem5a  27545  gausslemma2dlem5  27546  gausslemma2dlem6  27547  gausslemma2dlem7  27548  gausslemma2d  27549  lgseisenlem1  27550  lgseisenlem2  27551  lgseisenlem3  27552  lgseisenlem4  27553  lgsquadlem1  27555  lgsquadlem2  27556  lgsquad2lem1  27559  lgsquad2lem2  27560  lgsquad2  27561  lgsquad3  27562  m1lgs  27563  2lgslem1a1  27564  2lgslem1a2  27565  2lgslem1b  27567  2lgslem3b1  27576  2lgslem3c1  27577  2lgs2  27580  2lgs  27582  2lgsoddprmlem2  27584  2lgsoddprmlem3  27589  2lgsoddprm  27591  2sqblem  27606  2sqmod  27611  chebbnd1lem1  27644  chebbnd1lem3  27646  chebbnd1  27647  dchrisum0lem1a  27661  dchrvmasumiflem1  27676  dchrisum0flblem1  27683  dchrisum0flblem2  27684  dchrisum0lem1b  27690  dchrisum0lem1  27691  dchrisum0lem2a  27692  dchrisum0lem2  27693  dchrisum0lem3  27694  mulog2sumlem2  27710  pntlemd  27769  pntlema  27771  pntlemb  27772  pntlemh  27774  pntlemr  27777  pntlemf  27780  pntlemo  27782  istrkg2ld  28740  istrkg3ld  28741  axlowdimlem3  29305  axlowdimlem6  29308  axlowdimlem16  29318  axlowdimlem17  29319  axlowdim  29322  usgrexmpldifpr  29619  usgrexmplef  29620  cusgrsizeindb1  29811  pthdlem1  30126  clwlkclwwlklem2a1  30354  clwlkclwwlklem2fv1  30357  clwlkclwwlklem2fv2  30358  clwlkclwwlklem2a4  30359  clwlkclwwlklem2a  30360  clwwisshclwwslem  30376  eupth2lem3lem3  30592  konigsberglem5  30618  2clwwlk2  30710  numclwwlk2lem1  30738  numclwlk2lem2f  30739  frgrreggt1  30755  ex-fl  30809  ex-mod  30811  ex-hash  30815  ex-dvds  30818  ex-ind-dvds  30823  minvecolem3  31239  pjhthlem1  31754  wrdt2ind  33282  archirngz  33518  archiabllem2c  33524  evl1deg2  33876  rtelextdg2  34126  constrext2chnlem  34149  constrresqrtcl  34176  2sqr3minply  34179  cos9thpiminplylem2  34182  cos9thpiminplylem5  34185  lmat22det  34221  dya2ub  34669  dya2icoseg  34676  oddpwdc  34753  eulerpartlemd  34765  eulerpartlemt  34770  ballotlem2  34888  signslema  34958  prodfzo03  34999  hgt750leme  35054  tgoldbachgtde  35056  nn0prpwlem  36861  knoppndvlem2  37130  knoppndvlem8  37136  irrdifflemf  37997  qdiff  37999  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  logblebd  42772  lcm2un  42809  lcm3un  42810  lcmineqlem18  42841  lcmineqlem19  42842  lcmineqlem21  42844  lcmineqlem22  42845  3lexlogpow5ineq2  42850  3lexlogpow2ineq1  42853  aks4d1p1p3  42864  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p3  42873  aks4d1p6  42876  aks4d1p7d1  42877  aks4d1p7  42878  aks4d1p8  42882  aks4d1p9  42883  posbezout  42895  5bc2eq10  42937  2np3bcnp1  42939  2ap1caineq  42940  aks6d1c6lem4  42968  aks6d1c7lem1  42975  aks6d1c7lem2  42976  flt4lem2  43407  flt4lem5  43410  flt4lem7  43419  nna4b4nsq  43420  acongrep  43735  acongeq  43738  jm2.18  43743  jm2.22  43750  jm2.23  43751  jm2.20nn  43752  jm2.26a  43755  jm2.26  43757  jm2.15nn0  43758  jm2.27a  43760  jm2.27c  43762  rmydioph  43769  jm3.1lem1  43772  jm3.1lem3  43774  expdiophlem1  43776  expdiophlem2  43777  hashnzfz2  45059  sumnnodd  46374  coskpi2  46608  cosknegpi  46611  dvdivbd  46665  stoweidlem26  46768  wallispilem4  46810  wallispi2lem1  46813  wallispi2lem2  46814  wallispi2  46815  stirlinglem1  46816  stirlinglem3  46818  stirlinglem7  46822  stirlinglem8  46823  stirlinglem10  46825  stirlinglem11  46826  stirlinglem15  46830  dirkertrigeqlem1  46840  dirkercncflem2  46846  fourierdlem54  46902  fourierdlem56  46904  fourierdlem57  46905  fourierdlem102  46950  fourierdlem114  46962  fourierswlem  46972  fouriersw  46973  smfmullem4  47536  evenwodadd  47630  nnmul2  48095  ceil5half3  48111  addmodne  48115  m1modnep2mod  48123  minusmodnep2tmod  48124  modmkpkne  48132  modmknepk  48133  modm2nep1  48137  modp2nep1  48138  modm1nep2  48139  modm1nem2  48140  2timesltsq  48143  2timesltsqm1  48144  fmtnorec1  48317  goldbachthlem2  48326  odz2prm2pw  48343  fmtnoprmfac1  48345  fmtnoprmfac2lem1  48346  fmtnoprmfac2  48347  fmtno4prmfac  48352  31prm  48377  sfprmdvdsmersenne  48383  lighneallem1  48385  lighneallem4a  48388  lighneallem4b  48389  lighneallem4  48390  proththdlem  48393  proththd  48394  3exp4mod41  48396  41prothprmlem2  48398  nprmdvdsfacm1lem1  48400  nprmdvdsfacm1lem2  48401  nprmdvdsfacm1lem4  48403  ppivalnnnprmge6  48406  ppivalnn  48412  m1expevenALTV  48440  dfeven2  48442  m2even  48447  gcd2odd1  48461  oexpnegALTV  48470  oexpnegnz  48471  2evenALTV  48485  2noddALTV  48486  nn0o1gt2ALTV  48487  nnpw2evenALTV  48495  perfectALTVlem1  48514  perfectALTVlem2  48515  fppr2odd  48524  341fppr2  48527  9fppr8  48530  nfermltl2rev  48536  sbgoldbalt  48574  mogoldbb  48578  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  gpg5order  48853  gpg5nbgrvtx13starlem2  48865  gpg3nbgrvtx0ALT  48870  gpg3kgrtriexlem5  48880  gpg5gricstgr3  48883  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  gpg5edgnedg  48923  2even  49032  zlmodzxzequa  49304  zlmodzxznm  49305  zlmodzxzequap  49307  zlmodzxzldeplem1  49308  zlmodzxzldeplem3  49310  zlmodzxzldep  49312  ldepsnlinclem1  49313  ldepsnlinc  49316  pw2m1lepw2m1  49328  fldivexpfllog2  49373  nnlog2ge0lt1  49374  logbpw2m1  49375  fllog2  49376  blennnelnn  49384  blenpw2  49386  nnpw2blenfzo  49389  blennnt2  49397  nnolog2flm1  49398  dig2nn0ld  49412  dig2nn1st  49413  0dig2pr01  49418  0dig2nn0o  49421  ackval42  49504  itsclc0xyqsolr  49577  2elfz13  50653  crosspdotsumi  50673