Theorem 2z 12624

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 12313	. 2 ⊢ 2 ∈ ℕ
2	1	nnzi 12616	1 ⊢ 2 ∈ ℤ

Syntax hints:   ∈ wcel 2108  2c2 12295  ℤcz 12588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rrecex 11201  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-neg 11469  df-nn 12241  df-2 12303  df-z 12589

This theorem is referenced by:  nn0lt2  12656  nn0le2is012  12657  zadd2cl  12705  eluz4eluz2  12899  uzuzle23  12905  2eluzge1  12910  eluz2b1  12935  nn01to3  12957  nn0ge2m1nnALT  12958  ige2m1fz  13634  fz0to3un2pr  13646  fz0to4untppr  13647  fz0to5un2tp  13648  fzctr  13657  fzo0to2pr  13766  fzo0to42pr  13769  2tnp1ge0ge0  13846  flhalf  13847  m1modge3gt1  13936  2txmodxeq0  13949  f13idfv  14018  sqrecd  14168  znsqcld  14180  sq1  14213  expnass  14226  sqoddm1div8  14261  bcn2m1  14342  bcn2p1  14343  4bc2eq6  14347  hashtpg  14503  ccat2s1p2  14648  pfxtrcfv0  14712  pfxtrcfvl  14715  eqwrds3  14980  iseraltlem2  15699  iseraltlem3  15700  climcndslem1  15865  climcnds  15867  bpolydiflem  16070  efgt0  16121  tanval3  16152  cos01bnd  16204  cos01gt0  16209  odd2np1  16360  even2n  16361  oddm1even  16362  oddp1even  16363  oexpneg  16364  mod2eq1n2dvds  16366  2tp1odd  16371  2teven  16374  evend2  16376  oddp1d2  16377  ltoddhalfle  16380  opoe  16382  omoe  16383  opeo  16384  omeo  16385  z0even  16386  z2even  16389  z4even  16391  4dvdseven  16392  m1expo  16394  m1exp1  16395  nn0o  16402  sumeven  16406  flodddiv4  16434  bits0e  16448  bits0o  16449  bitsp1e  16451  bitsp1o  16452  bitsfzo  16454  bitsmod  16455  bitscmp  16457  bitsinv1lem  16460  bitsinv1  16461  6gcd4e2  16557  3lcm2e6woprm  16634  lcmf2a3a4e12  16666  isprm3  16702  dvdsnprmd  16709  2prm  16711  2mulprm  16712  oddprmge3  16719  ge2nprmge4  16720  isprm7  16727  divgcdodd  16729  oddprm  16830  pythagtriplem4  16839  pythagtriplem11  16845  pythagtriplem13  16847  iserodd  16855  prmgaplem3  17073  prmgaplem7  17077  dec2dvds  17083  prmlem0  17125  4001lem1  17160  psgnunilem4  19478  efgredleme  19724  lt6abl  19876  ablsimpgfindlem1  20090  ablsimpgfindlem2  20091  zringndrg  21429  znidomb  21522  chfacfscmulfsupp  22797  chfacfpmmulfsupp  22801  minveclem2  25378  minveclem3  25381  pjthlem1  25389  dyaddisjlem  25548  mbfi1fseqlem5  25672  dvrecg  25929  dvexp3  25934  aaliou3lem6  26308  tanregt0  26500  efif1olem4  26506  tanarg  26580  cxpsqrtth  26691  2irrexpq  26692  2logb9irr  26757  2logb9irrALT  26760  sqrt2cxp2logb9e3  26761  cubic2  26810  asinlem3  26833  atantayl2  26900  cxp2limlem  26938  lgamgulmlem3  26993  lgamgulmlem4  26994  basellem2  27044  basellem3  27045  basellem4  27046  basellem5  27047  basellem8  27050  basellem9  27051  ppisval  27066  ppiprm  27113  ppinprm  27114  chtprm  27115  chtnprm  27116  chtdif  27120  ppidif  27125  ppi1  27126  cht1  27127  cht3  27135  ppieq0  27138  ppiublem1  27165  chpeq0  27171  chtub  27175  chpval2  27181  chpub  27183  mersenne  27190  perfect1  27191  perfectlem1  27192  perfectlem2  27193  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgslem1  27260  lgsdir2lem2  27289  lgsdir2  27293  lgsqr  27314  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  gausslemma2dlem5a  27333  gausslemma2dlem5  27334  gausslemma2dlem6  27335  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem1  27347  lgsquad2lem2  27348  lgsquad2  27349  lgsquad3  27350  m1lgs  27351  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1b  27355  2lgslem3b1  27364  2lgslem3c1  27365  2lgs2  27368  2lgs  27370  2lgsoddprmlem2  27372  2lgsoddprmlem3  27377  2lgsoddprm  27379  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  dchrisum0lem1a  27449  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  mulog2sumlem2  27498  pntlemd  27557  pntlema  27559  pntlemb  27560  pntlemh  27562  pntlemr  27565  pntlemf  27568  pntlemo  27570  istrkg2ld  28439  istrkg3ld  28440  axlowdimlem3  28923  axlowdimlem6  28926  axlowdimlem16  28936  axlowdimlem17  28937  axlowdim  28940  usgrexmpldifpr  29237  usgrexmplef  29238  cusgrsizeindb1  29430  pthdlem1  29748  clwlkclwwlklem2a1  29973  clwlkclwwlklem2fv1  29976  clwlkclwwlklem2fv2  29977  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwwisshclwwslem  29995  eupth2lem3lem3  30211  konigsberglem5  30237  2clwwlk2  30329  numclwwlk2lem1  30357  numclwlk2lem2f  30358  frgrreggt1  30374  ex-fl  30428  ex-mod  30430  ex-hash  30434  ex-dvds  30437  ex-ind-dvds  30442  minvecolem3  30857  pjhthlem1  31372  wrdt2ind  32929  archirngz  33187  archiabllem2c  33193  evl1deg2  33590  rtelextdg2  33761  constrext2chnlem  33784  constrresqrtcl  33811  2sqr3minply  33814  cos9thpiminplylem2  33817  cos9thpiminplylem5  33820  lmat22det  33853  dya2ub  34302  dya2icoseg  34309  oddpwdc  34386  eulerpartlemd  34398  eulerpartlemt  34403  ballotlem2  34521  signslema  34594  prodfzo03  34635  hgt750leme  34690  tgoldbachgtde  34692  nn0prpwlem  36340  knoppndvlem2  36531  knoppndvlem8  36537  irrdifflemf  37343  poimirlem25  37669  poimirlem26  37670  poimirlem27  37671  poimirlem28  37672  logblebd  41989  lcm2un  42027  lcm3un  42028  lcmineqlem18  42059  lcmineqlem19  42060  lcmineqlem21  42062  lcmineqlem22  42063  3lexlogpow5ineq2  42068  3lexlogpow2ineq1  42071  aks4d1p1p3  42082  aks4d1p1p4  42084  aks4d1p1p6  42086  aks4d1p1p7  42087  aks4d1p1p5  42088  aks4d1p1  42089  aks4d1p3  42091  aks4d1p6  42094  aks4d1p7d1  42095  aks4d1p7  42096  aks4d1p8  42100  aks4d1p9  42101  posbezout  42113  5bc2eq10  42155  2np3bcnp1  42157  2ap1caineq  42158  aks6d1c6lem4  42186  aks6d1c7lem1  42193  aks6d1c7lem2  42194  flt4lem2  42670  flt4lem5  42673  flt4lem7  42682  nna4b4nsq  42683  acongrep  43004  acongeq  43007  jm2.18  43012  jm2.22  43019  jm2.23  43020  jm2.20nn  43021  jm2.26a  43024  jm2.26  43026  jm2.15nn0  43027  jm2.27a  43029  jm2.27c  43031  rmydioph  43038  jm3.1lem1  43041  jm3.1lem3  43043  expdiophlem1  43045  expdiophlem2  43046  hashnzfz2  44345  sumnnodd  45659  coskpi2  45895  cosknegpi  45898  dvdivbd  45952  stoweidlem26  46055  wallispilem4  46097  wallispi2lem1  46100  wallispi2lem2  46101  wallispi2  46102  stirlinglem1  46103  stirlinglem3  46105  stirlinglem7  46109  stirlinglem8  46110  stirlinglem10  46112  stirlinglem11  46113  stirlinglem15  46117  dirkertrigeqlem1  46127  dirkercncflem2  46133  fourierdlem54  46189  fourierdlem56  46191  fourierdlem57  46192  fourierdlem102  46237  fourierdlem114  46249  fourierswlem  46259  fouriersw  46260  smfmullem4  46823  evenwodadd  46917  ceil5half3  47369  addmodne  47373  m1modnep2mod  47381  minusmodnep2tmod  47382  fmtnorec1  47551  goldbachthlem2  47560  odz2prm2pw  47577  fmtnoprmfac1  47579  fmtnoprmfac2lem1  47580  fmtnoprmfac2  47581  fmtno4prmfac  47586  31prm  47611  sfprmdvdsmersenne  47617  lighneallem1  47619  lighneallem4a  47622  lighneallem4b  47623  lighneallem4  47624  proththdlem  47627  proththd  47628  3exp4mod41  47630  41prothprmlem2  47632  m1expevenALTV  47661  dfeven2  47663  m2even  47668  gcd2odd1  47682  oexpnegALTV  47691  oexpnegnz  47692  2evenALTV  47706  2noddALTV  47707  nn0o1gt2ALTV  47708  nnpw2evenALTV  47716  perfectALTVlem1  47735  perfectALTVlem2  47736  fppr2odd  47745  341fppr2  47748  9fppr8  47751  nfermltl2rev  47757  sbgoldbalt  47795  mogoldbb  47799  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  gpg5order  48064  gpg3nbgrvtxlem  48069  gpg5nbgrvtx13starlem2  48074  gpg3nbgrvtx0ALT  48079  gpg3kgrtriexlem5  48089  gpg5gricstgr3  48092  2even  48214  zlmodzxzequa  48472  zlmodzxznm  48473  zlmodzxzequap  48475  zlmodzxzldeplem1  48476  zlmodzxzldeplem3  48478  zlmodzxzldep  48480  ldepsnlinclem1  48481  ldepsnlinc  48484  pw2m1lepw2m1  48496  fldivexpfllog2  48545  nnlog2ge0lt1  48546  logbpw2m1  48547  fllog2  48548  blennnelnn  48556  blenpw2  48558  nnpw2blenfzo  48561  blennnt2  48569  nnolog2flm1  48570  dig2nn0ld  48584  dig2nn1st  48585  0dig2pr01  48590  0dig2nn0o  48593  ackval42  48676  itsclc0xyqsolr  48749