Theorem 2z 12646

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

Syntax hints:   ∈ wcel 2105  2c2 12318  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-2 12326  df-z 12611

This theorem is referenced by:  nn0lt2  12678  nn0le2is012  12679  zadd2cl  12727  eluz4eluz2  12922  uzuzle23  12928  2eluzge1  12933  eluz2b1  12958  nn01to3  12980  nn0ge2m1nnALT  12981  ige2m1fz  13653  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  fzctr  13676  fzo0to2pr  13785  fzo0to42pr  13788  2tnp1ge0ge0  13865  flhalf  13866  m1modge3gt1  13955  2txmodxeq0  13968  f13idfv  14037  sqrecd  14186  znsqcld  14198  sq1  14230  expnass  14243  sqoddm1div8  14278  bcn2m1  14359  bcn2p1  14360  4bc2eq6  14364  hashtpg  14520  ccat2s1p2  14664  pfxtrcfv0  14728  pfxtrcfvl  14731  eqwrds3  14996  iseraltlem2  15715  iseraltlem3  15716  climcndslem1  15881  climcnds  15883  bpolydiflem  16086  efgt0  16135  tanval3  16166  cos01bnd  16218  cos01gt0  16223  odd2np1  16374  even2n  16375  oddm1even  16376  oddp1even  16377  oexpneg  16378  mod2eq1n2dvds  16380  2tp1odd  16385  2teven  16388  evend2  16390  oddp1d2  16391  ltoddhalfle  16394  opoe  16396  omoe  16397  opeo  16398  omeo  16399  z0even  16400  z2even  16403  z4even  16405  4dvdseven  16406  m1expo  16408  m1exp1  16409  nn0o  16416  sumeven  16420  flodddiv4  16448  bits0e  16462  bits0o  16463  bitsp1e  16465  bitsp1o  16466  bitsfzo  16468  bitsmod  16469  bitscmp  16471  bitsinv1lem  16474  bitsinv1  16475  6gcd4e2  16571  3lcm2e6woprm  16648  lcmf2a3a4e12  16680  isprm3  16716  dvdsnprmd  16723  2prm  16725  2mulprm  16726  oddprmge3  16733  ge2nprmge4  16734  isprm7  16741  divgcdodd  16743  oddprm  16843  pythagtriplem4  16852  pythagtriplem11  16858  pythagtriplem13  16860  iserodd  16868  prmgaplem3  17086  prmgaplem7  17090  dec2dvds  17096  prmlem0  17139  4001lem1  17174  psgnunilem4  19529  efgredleme  19775  lt6abl  19927  ablsimpgfindlem1  20141  ablsimpgfindlem2  20142  zringndrg  21496  znidomb  21597  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  minveclem2  25473  minveclem3  25476  pjthlem1  25484  dyaddisjlem  25643  mbfi1fseqlem5  25768  dvrecg  26025  dvexp3  26030  aaliou3lem6  26404  tanregt0  26595  efif1olem4  26601  tanarg  26675  cxpsqrtth  26786  2irrexpq  26787  2logb9irr  26852  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  cubic2  26905  asinlem3  26928  atantayl2  26995  cxp2limlem  27033  lgamgulmlem3  27088  lgamgulmlem4  27089  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  basellem8  27145  basellem9  27146  ppisval  27161  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  chtdif  27215  ppidif  27220  ppi1  27221  cht1  27222  cht3  27230  ppieq0  27233  ppiublem1  27260  chpeq0  27266  chtub  27270  chpval2  27276  chpub  27278  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgslem1  27355  lgsdir2lem2  27384  lgsdir2  27388  lgsqr  27409  gausslemma2dlem0i  27422  gausslemma2dlem1a  27423  gausslemma2dlem5a  27428  gausslemma2dlem5  27429  gausslemma2dlem6  27430  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem1  27442  lgsquad2lem2  27443  lgsquad2  27444  lgsquad3  27445  m1lgs  27446  2lgslem1a1  27447  2lgslem1a2  27448  2lgslem1b  27450  2lgslem3b1  27459  2lgslem3c1  27460  2lgs2  27463  2lgs  27465  2lgsoddprmlem2  27467  2lgsoddprmlem3  27472  2lgsoddprm  27474  2sqblem  27489  2sqmod  27494  chebbnd1lem1  27527  chebbnd1lem3  27529  chebbnd1  27530  dchrisum0lem1a  27544  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  mulog2sumlem2  27593  pntlemd  27652  pntlema  27654  pntlemb  27655  pntlemh  27657  pntlemr  27660  pntlemf  27663  pntlemo  27665  istrkg2ld  28482  istrkg3ld  28483  axlowdimlem3  28973  axlowdimlem6  28976  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  usgrexmpldifpr  29289  usgrexmplef  29290  cusgrsizeindb1  29482  pthdlem1  29798  clwlkclwwlklem2a1  30020  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwwisshclwwslem  30042  eupth2lem3lem3  30258  konigsberglem5  30284  2clwwlk2  30376  numclwwlk2lem1  30404  numclwlk2lem2f  30405  frgrreggt1  30421  ex-fl  30475  ex-mod  30477  ex-hash  30481  ex-dvds  30484  ex-ind-dvds  30489  minvecolem3  30904  pjhthlem1  31419  wrdt2ind  32922  archirngz  33178  archiabllem2c  33184  evl1deg2  33581  rtelextdg2  33732  2sqr3minply  33752  lmat22det  33782  dya2ub  34251  dya2icoseg  34258  oddpwdc  34335  eulerpartlemd  34347  eulerpartlemt  34352  ballotlem2  34469  signslema  34555  prodfzo03  34596  hgt750leme  34651  tgoldbachgtde  34653  nn0prpwlem  36304  knoppndvlem2  36495  knoppndvlem8  36501  irrdifflemf  37307  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  logblebd  41957  lcm2un  41995  lcm3un  41996  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  aks4d1p1p3  42050  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p3  42059  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  5bc2eq10  42123  2np3bcnp1  42125  2ap1caineq  42126  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7lem2  42162  flt4lem2  42633  flt4lem5  42636  flt4lem7  42645  nna4b4nsq  42646  acongrep  42968  acongeq  42971  jm2.18  42976  jm2.22  42983  jm2.23  42984  jm2.20nn  42985  jm2.26a  42988  jm2.26  42990  jm2.15nn0  42991  jm2.27a  42993  jm2.27c  42995  rmydioph  43002  jm3.1lem1  43005  jm3.1lem3  43007  expdiophlem1  43009  expdiophlem2  43010  hashnzfz2  44316  sumnnodd  45585  coskpi2  45821  cosknegpi  45824  dvdivbd  45878  stoweidlem26  45981  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem15  46043  dirkertrigeqlem1  46053  dirkercncflem2  46059  fourierdlem54  46115  fourierdlem56  46117  fourierdlem57  46118  fourierdlem102  46163  fourierdlem114  46175  fourierswlem  46185  fouriersw  46186  smfmullem4  46749  ceil5half3  47279  addmodne  47283  m1modnep2mod  47291  minusmodnep2tmod  47292  fmtnorec1  47461  goldbachthlem2  47470  odz2prm2pw  47487  fmtnoprmfac1  47489  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  fmtno4prmfac  47496  31prm  47521  sfprmdvdsmersenne  47527  lighneallem1  47529  lighneallem4a  47532  lighneallem4b  47533  lighneallem4  47534  proththdlem  47537  proththd  47538  3exp4mod41  47540  41prothprmlem2  47542  m1expevenALTV  47571  dfeven2  47573  m2even  47578  gcd2odd1  47592  oexpnegALTV  47601  oexpnegnz  47602  2evenALTV  47616  2noddALTV  47617  nn0o1gt2ALTV  47618  nnpw2evenALTV  47626  perfectALTVlem1  47645  perfectALTVlem2  47646  fppr2odd  47655  341fppr2  47658  9fppr8  47661  nfermltl2rev  47667  sbgoldbalt  47705  mogoldbb  47709  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  gpg5order  47948  gpg3nbgrvtxlem  47957  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0ALT  47967  gpg5gricstgr3  47973  2even  48082  zlmodzxzequa  48341  zlmodzxznm  48342  zlmodzxzequap  48344  zlmodzxzldeplem1  48345  zlmodzxzldeplem3  48347  zlmodzxzldep  48349  ldepsnlinclem1  48350  ldepsnlinc  48353  pw2m1lepw2m1  48365  fldivexpfllog2  48414  nnlog2ge0lt1  48415  logbpw2m1  48416  fllog2  48417  blennnelnn  48425  blenpw2  48427  nnpw2blenfzo  48430  blennnt2  48438  nnolog2flm1  48439  dig2nn0ld  48453  dig2nn1st  48454  0dig2pr01  48459  0dig2nn0o  48462  ackval42  48545  itsclc0xyqsolr  48618