Theorem 2z 12550

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

Syntax hints:   ∈ wcel 2114  2c2 12227  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-nn 12166  df-2 12235  df-z 12516

This theorem is referenced by:  nn0lt2  12583  nn0le2is012  12584  zadd2cl  12632  2eluzge1  12823  uzuzle23  12825  uzuzle24  12826  eluz2b1  12860  nn01to3  12882  nn0ge2m1nnALT  12883  ige2m1fz  13562  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  fzctr  13585  fzo0to2pr  13696  fzo0to42pr  13699  2tnp1ge0ge0  13779  flhalf  13780  m1modge3gt1  13871  2txmodxeq0  13884  f13idfv  13953  sqrecd  14103  znsqcld  14115  sq1  14148  expnass  14161  sqoddm1div8  14196  bcn2m1  14277  bcn2p1  14278  4bc2eq6  14282  hashtpg  14438  ccat2s1p2  14584  pfxtrcfv0  14647  pfxtrcfvl  14650  eqwrds3  14914  iseraltlem2  15636  iseraltlem3  15637  climcndslem1  15805  climcnds  15807  bpolydiflem  16010  efgt0  16061  tanval3  16092  cos01bnd  16144  cos01gt0  16149  odd2np1  16301  even2n  16302  oddm1even  16303  oddp1even  16304  oexpneg  16305  mod2eq1n2dvds  16307  2tp1odd  16312  2teven  16315  evend2  16317  oddp1d2  16318  ltoddhalfle  16321  opoe  16323  omoe  16324  opeo  16325  omeo  16326  z0even  16327  z2even  16330  z4even  16332  4dvdseven  16333  m1expo  16335  m1exp1  16336  nn0o  16343  sumeven  16347  flodddiv4  16375  bits0e  16389  bits0o  16390  bitsp1e  16392  bitsp1o  16393  bitsfzo  16395  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  bitsinv1  16402  6gcd4e2  16498  3lcm2e6woprm  16575  lcmf2a3a4e12  16607  isprm3  16643  dvdsnprmd  16650  2prm  16652  2mulprm  16653  oddprmge3  16661  ge2nprmge4  16662  isprm7  16669  divgcdodd  16671  oddprm  16772  pythagtriplem4  16781  pythagtriplem11  16787  pythagtriplem13  16789  iserodd  16797  prmgaplem3  17015  prmgaplem7  17019  dec2dvds  17025  prmlem0  17067  4001lem1  17102  ex-chn1  18594  psgnunilem4  19463  efgredleme  19709  lt6abl  19861  ablsimpgfindlem1  20075  ablsimpgfindlem2  20076  zringndrg  21458  znidomb  21551  chfacfscmulfsupp  22834  chfacfpmmulfsupp  22838  minveclem2  25403  minveclem3  25406  pjthlem1  25414  dyaddisjlem  25572  mbfi1fseqlem5  25696  dvrecg  25950  dvexp3  25955  aaliou3lem6  26325  tanregt0  26516  efif1olem4  26522  tanarg  26596  cxpsqrtth  26707  2irrexpq  26708  2logb9irr  26772  2logb9irrALT  26775  sqrt2cxp2logb9e3  26776  cubic2  26825  asinlem3  26848  atantayl2  26915  cxp2limlem  26953  lgamgulmlem3  27008  lgamgulmlem4  27009  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  basellem8  27065  basellem9  27066  ppisval  27081  ppiprm  27128  ppinprm  27129  chtprm  27130  chtnprm  27131  chtdif  27135  ppidif  27140  ppi1  27141  cht1  27142  cht3  27150  ppieq0  27153  ppiublem1  27179  chpeq0  27185  chtub  27189  chpval2  27195  chpub  27197  mersenne  27204  perfect1  27205  perfectlem1  27206  perfectlem2  27207  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem5  27265  bposlem6  27266  lgslem1  27274  lgsdir2lem2  27303  lgsdir2  27307  lgsqr  27328  gausslemma2dlem0i  27341  gausslemma2dlem1a  27342  gausslemma2dlem5a  27347  gausslemma2dlem5  27348  gausslemma2dlem6  27349  gausslemma2dlem7  27350  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  lgsquadlem2  27358  lgsquad2lem1  27361  lgsquad2lem2  27362  lgsquad2  27363  lgsquad3  27364  m1lgs  27365  2lgslem1a1  27366  2lgslem1a2  27367  2lgslem1b  27369  2lgslem3b1  27378  2lgslem3c1  27379  2lgs2  27382  2lgs  27384  2lgsoddprmlem2  27386  2lgsoddprmlem3  27391  2lgsoddprm  27393  2sqblem  27408  2sqmod  27413  chebbnd1lem1  27446  chebbnd1lem3  27448  chebbnd1  27449  dchrisum0lem1a  27463  dchrvmasumiflem1  27478  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  mulog2sumlem2  27512  pntlemd  27571  pntlema  27573  pntlemb  27574  pntlemh  27576  pntlemr  27579  pntlemf  27582  pntlemo  27584  istrkg2ld  28542  istrkg3ld  28543  axlowdimlem3  29027  axlowdimlem6  29030  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  usgrexmpldifpr  29341  usgrexmplef  29342  cusgrsizeindb1  29534  pthdlem1  29849  clwlkclwwlklem2a1  30077  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwwisshclwwslem  30099  eupth2lem3lem3  30315  konigsberglem5  30341  2clwwlk2  30433  numclwwlk2lem1  30461  numclwlk2lem2f  30462  frgrreggt1  30478  ex-fl  30532  ex-mod  30534  ex-hash  30538  ex-dvds  30541  ex-ind-dvds  30546  minvecolem3  30962  pjhthlem1  31477  wrdt2ind  33028  archirngz  33265  archiabllem2c  33271  evl1deg2  33652  rtelextdg2  33887  constrext2chnlem  33910  constrresqrtcl  33937  2sqr3minply  33940  cos9thpiminplylem2  33943  cos9thpiminplylem5  33946  lmat22det  33982  dya2ub  34430  dya2icoseg  34437  oddpwdc  34514  eulerpartlemd  34526  eulerpartlemt  34531  ballotlem2  34649  signslema  34722  prodfzo03  34763  hgt750leme  34818  tgoldbachgtde  34820  nn0prpwlem  36520  knoppndvlem2  36789  knoppndvlem8  36795  irrdifflemf  37655  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  logblebd  42430  lcm2un  42467  lcm3un  42468  lcmineqlem18  42499  lcmineqlem19  42500  lcmineqlem21  42502  lcmineqlem22  42503  3lexlogpow5ineq2  42508  3lexlogpow2ineq1  42511  aks4d1p1p3  42522  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p3  42531  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  5bc2eq10  42595  2np3bcnp1  42597  2ap1caineq  42598  aks6d1c6lem4  42626  aks6d1c7lem1  42633  aks6d1c7lem2  42634  flt4lem2  43094  flt4lem5  43097  flt4lem7  43106  nna4b4nsq  43107  acongrep  43426  acongeq  43429  jm2.18  43434  jm2.22  43441  jm2.23  43442  jm2.20nn  43443  jm2.26a  43446  jm2.26  43448  jm2.15nn0  43449  jm2.27a  43451  jm2.27c  43453  rmydioph  43460  jm3.1lem1  43463  jm3.1lem3  43465  expdiophlem1  43467  expdiophlem2  43468  hashnzfz2  44766  sumnnodd  46078  coskpi2  46312  cosknegpi  46315  dvdivbd  46369  stoweidlem26  46472  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem11  46530  stirlinglem15  46534  dirkertrigeqlem1  46544  dirkercncflem2  46550  fourierdlem54  46606  fourierdlem56  46608  fourierdlem57  46609  fourierdlem102  46654  fourierdlem114  46666  fourierswlem  46676  fouriersw  46677  smfmullem4  47240  nthrucw  47332  evenwodadd  47333  nnmul2  47790  ceil5half3  47806  addmodne  47810  m1modnep2mod  47818  minusmodnep2tmod  47819  modmkpkne  47827  modmknepk  47828  modm2nep1  47832  modp2nep1  47833  modm1nep2  47834  modm1nem2  47835  2timesltsq  47838  2timesltsqm1  47839  fmtnorec1  48012  goldbachthlem2  48021  odz2prm2pw  48038  fmtnoprmfac1  48040  fmtnoprmfac2lem1  48041  fmtnoprmfac2  48042  fmtno4prmfac  48047  31prm  48072  sfprmdvdsmersenne  48078  lighneallem1  48080  lighneallem4a  48083  lighneallem4b  48084  lighneallem4  48085  proththdlem  48088  proththd  48089  3exp4mod41  48091  41prothprmlem2  48093  nprmdvdsfacm1lem1  48095  nprmdvdsfacm1lem2  48096  nprmdvdsfacm1lem4  48098  ppivalnnnprmge6  48101  ppivalnn  48107  m1expevenALTV  48135  dfeven2  48137  m2even  48142  gcd2odd1  48156  oexpnegALTV  48165  oexpnegnz  48166  2evenALTV  48180  2noddALTV  48181  nn0o1gt2ALTV  48182  nnpw2evenALTV  48190  perfectALTVlem1  48209  perfectALTVlem2  48210  fppr2odd  48219  341fppr2  48222  9fppr8  48225  nfermltl2rev  48231  sbgoldbalt  48269  mogoldbb  48273  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  gpg5order  48548  gpg5nbgrvtx13starlem2  48560  gpg3nbgrvtx0ALT  48565  gpg3kgrtriexlem5  48575  gpg5gricstgr3  48578  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  gpg5edgnedg  48618  2even  48727  zlmodzxzequa  48984  zlmodzxznm  48985  zlmodzxzequap  48987  zlmodzxzldeplem1  48988  zlmodzxzldeplem3  48990  zlmodzxzldep  48992  ldepsnlinclem1  48993  ldepsnlinc  48996  pw2m1lepw2m1  49008  fldivexpfllog2  49053  nnlog2ge0lt1  49054  logbpw2m1  49055  fllog2  49056  blennnelnn  49064  blenpw2  49066  nnpw2blenfzo  49069  blennnt2  49077  nnolog2flm1  49078  dig2nn0ld  49092  dig2nn1st  49093  0dig2pr01  49098  0dig2nn0o  49101  ackval42  49184  itsclc0xyqsolr  49257