Theorem 2z 12526

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

Syntax hints:   ∈ wcel 2109  2c2 12202  ℤcz 12490

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11369  df-nn 12148  df-2 12210  df-z 12491

This theorem is referenced by:  nn0lt2  12558  nn0le2is012  12559  zadd2cl  12607  2eluzge1  12802  uzuzle23  12804  uzuzle24  12805  eluz2b1  12839  nn01to3  12861  nn0ge2m1nnALT  12862  ige2m1fz  13539  fz0to3un2pr  13551  fz0to4untppr  13552  fz0to5un2tp  13553  fzctr  13562  fzo0to2pr  13672  fzo0to42pr  13675  2tnp1ge0ge0  13752  flhalf  13753  m1modge3gt1  13844  2txmodxeq0  13857  f13idfv  13926  sqrecd  14076  znsqcld  14088  sq1  14121  expnass  14134  sqoddm1div8  14169  bcn2m1  14250  bcn2p1  14251  4bc2eq6  14255  hashtpg  14411  ccat2s1p2  14556  pfxtrcfv0  14619  pfxtrcfvl  14622  eqwrds3  14887  iseraltlem2  15609  iseraltlem3  15610  climcndslem1  15775  climcnds  15777  bpolydiflem  15980  efgt0  16031  tanval3  16062  cos01bnd  16114  cos01gt0  16119  odd2np1  16271  even2n  16272  oddm1even  16273  oddp1even  16274  oexpneg  16275  mod2eq1n2dvds  16277  2tp1odd  16282  2teven  16285  evend2  16287  oddp1d2  16288  ltoddhalfle  16291  opoe  16293  omoe  16294  opeo  16295  omeo  16296  z0even  16297  z2even  16300  z4even  16302  4dvdseven  16303  m1expo  16305  m1exp1  16306  nn0o  16313  sumeven  16317  flodddiv4  16345  bits0e  16359  bits0o  16360  bitsp1e  16362  bitsp1o  16363  bitsfzo  16365  bitsmod  16366  bitscmp  16368  bitsinv1lem  16371  bitsinv1  16372  6gcd4e2  16468  3lcm2e6woprm  16545  lcmf2a3a4e12  16577  isprm3  16613  dvdsnprmd  16620  2prm  16622  2mulprm  16623  oddprmge3  16630  ge2nprmge4  16631  isprm7  16638  divgcdodd  16640  oddprm  16741  pythagtriplem4  16750  pythagtriplem11  16756  pythagtriplem13  16758  iserodd  16766  prmgaplem3  16984  prmgaplem7  16988  dec2dvds  16994  prmlem0  17036  4001lem1  17071  psgnunilem4  19395  efgredleme  19641  lt6abl  19793  ablsimpgfindlem1  20007  ablsimpgfindlem2  20008  zringndrg  21394  znidomb  21487  chfacfscmulfsupp  22763  chfacfpmmulfsupp  22767  minveclem2  25343  minveclem3  25346  pjthlem1  25354  dyaddisjlem  25513  mbfi1fseqlem5  25637  dvrecg  25894  dvexp3  25899  aaliou3lem6  26273  tanregt0  26465  efif1olem4  26471  tanarg  26545  cxpsqrtth  26656  2irrexpq  26657  2logb9irr  26722  2logb9irrALT  26725  sqrt2cxp2logb9e3  26726  cubic2  26775  asinlem3  26798  atantayl2  26865  cxp2limlem  26903  lgamgulmlem3  26958  lgamgulmlem4  26959  basellem2  27009  basellem3  27010  basellem4  27011  basellem5  27012  basellem8  27015  basellem9  27016  ppisval  27031  ppiprm  27078  ppinprm  27079  chtprm  27080  chtnprm  27081  chtdif  27085  ppidif  27090  ppi1  27091  cht1  27092  cht3  27100  ppieq0  27103  ppiublem1  27130  chpeq0  27136  chtub  27140  chpval2  27146  chpub  27148  mersenne  27155  perfect1  27156  perfectlem1  27157  perfectlem2  27158  bposlem1  27212  bposlem2  27213  bposlem3  27214  bposlem5  27216  bposlem6  27217  lgslem1  27225  lgsdir2lem2  27254  lgsdir2  27258  lgsqr  27279  gausslemma2dlem0i  27292  gausslemma2dlem1a  27293  gausslemma2dlem5a  27298  gausslemma2dlem5  27299  gausslemma2dlem6  27300  gausslemma2dlem7  27301  gausslemma2d  27302  lgseisenlem1  27303  lgseisenlem2  27304  lgseisenlem3  27305  lgseisenlem4  27306  lgsquadlem1  27308  lgsquadlem2  27309  lgsquad2lem1  27312  lgsquad2lem2  27313  lgsquad2  27314  lgsquad3  27315  m1lgs  27316  2lgslem1a1  27317  2lgslem1a2  27318  2lgslem1b  27320  2lgslem3b1  27329  2lgslem3c1  27330  2lgs2  27333  2lgs  27335  2lgsoddprmlem2  27337  2lgsoddprmlem3  27342  2lgsoddprm  27344  2sqblem  27359  2sqmod  27364  chebbnd1lem1  27397  chebbnd1lem3  27399  chebbnd1  27400  dchrisum0lem1a  27414  dchrvmasumiflem1  27429  dchrisum0flblem1  27436  dchrisum0flblem2  27437  dchrisum0lem1b  27443  dchrisum0lem1  27444  dchrisum0lem2a  27445  dchrisum0lem2  27446  dchrisum0lem3  27447  mulog2sumlem2  27463  pntlemd  27522  pntlema  27524  pntlemb  27525  pntlemh  27527  pntlemr  27530  pntlemf  27533  pntlemo  27535  istrkg2ld  28424  istrkg3ld  28425  axlowdimlem3  28908  axlowdimlem6  28911  axlowdimlem16  28921  axlowdimlem17  28922  axlowdim  28925  usgrexmpldifpr  29222  usgrexmplef  29223  cusgrsizeindb1  29415  pthdlem1  29730  clwlkclwwlklem2a1  29955  clwlkclwwlklem2fv1  29958  clwlkclwwlklem2fv2  29959  clwlkclwwlklem2a4  29960  clwlkclwwlklem2a  29961  clwwisshclwwslem  29977  eupth2lem3lem3  30193  konigsberglem5  30219  2clwwlk2  30311  numclwwlk2lem1  30339  numclwlk2lem2f  30340  frgrreggt1  30356  ex-fl  30410  ex-mod  30412  ex-hash  30416  ex-dvds  30419  ex-ind-dvds  30424  minvecolem3  30839  pjhthlem1  31354  wrdt2ind  32914  archirngz  33150  archiabllem2c  33156  evl1deg2  33531  rtelextdg2  33713  constrext2chnlem  33736  constrresqrtcl  33763  2sqr3minply  33766  cos9thpiminplylem2  33769  cos9thpiminplylem5  33772  lmat22det  33808  dya2ub  34257  dya2icoseg  34264  oddpwdc  34341  eulerpartlemd  34353  eulerpartlemt  34358  ballotlem2  34476  signslema  34549  prodfzo03  34590  hgt750leme  34645  tgoldbachgtde  34647  nn0prpwlem  36315  knoppndvlem2  36506  knoppndvlem8  36512  irrdifflemf  37318  poimirlem25  37644  poimirlem26  37645  poimirlem27  37646  poimirlem28  37647  logblebd  41969  lcm2un  42007  lcm3un  42008  lcmineqlem18  42039  lcmineqlem19  42040  lcmineqlem21  42042  lcmineqlem22  42043  3lexlogpow5ineq2  42048  3lexlogpow2ineq1  42051  aks4d1p1p3  42062  aks4d1p1p4  42064  aks4d1p1p6  42066  aks4d1p1p7  42067  aks4d1p1p5  42068  aks4d1p1  42069  aks4d1p3  42071  aks4d1p6  42074  aks4d1p7d1  42075  aks4d1p7  42076  aks4d1p8  42080  aks4d1p9  42081  posbezout  42093  5bc2eq10  42135  2np3bcnp1  42137  2ap1caineq  42138  aks6d1c6lem4  42166  aks6d1c7lem1  42173  aks6d1c7lem2  42174  flt4lem2  42640  flt4lem5  42643  flt4lem7  42652  nna4b4nsq  42653  acongrep  42973  acongeq  42976  jm2.18  42981  jm2.22  42988  jm2.23  42989  jm2.20nn  42990  jm2.26a  42993  jm2.26  42995  jm2.15nn0  42996  jm2.27a  42998  jm2.27c  43000  rmydioph  43007  jm3.1lem1  43010  jm3.1lem3  43012  expdiophlem1  43014  expdiophlem2  43015  hashnzfz2  44314  sumnnodd  45631  coskpi2  45867  cosknegpi  45870  dvdivbd  45924  stoweidlem26  46027  wallispilem4  46069  wallispi2lem1  46072  wallispi2lem2  46073  wallispi2  46074  stirlinglem1  46075  stirlinglem3  46077  stirlinglem7  46081  stirlinglem8  46082  stirlinglem10  46084  stirlinglem11  46085  stirlinglem15  46089  dirkertrigeqlem1  46099  dirkercncflem2  46105  fourierdlem54  46161  fourierdlem56  46163  fourierdlem57  46164  fourierdlem102  46209  fourierdlem114  46221  fourierswlem  46231  fouriersw  46232  smfmullem4  46795  evenwodadd  46889  ceil5half3  47344  addmodne  47348  m1modnep2mod  47356  minusmodnep2tmod  47357  modmkpkne  47365  modmknepk  47366  modm2nep1  47370  modp2nep1  47371  modm1nep2  47372  modm1nem2  47373  fmtnorec1  47541  goldbachthlem2  47550  odz2prm2pw  47567  fmtnoprmfac1  47569  fmtnoprmfac2lem1  47570  fmtnoprmfac2  47571  fmtno4prmfac  47576  31prm  47601  sfprmdvdsmersenne  47607  lighneallem1  47609  lighneallem4a  47612  lighneallem4b  47613  lighneallem4  47614  proththdlem  47617  proththd  47618  3exp4mod41  47620  41prothprmlem2  47622  m1expevenALTV  47651  dfeven2  47653  m2even  47658  gcd2odd1  47672  oexpnegALTV  47681  oexpnegnz  47682  2evenALTV  47696  2noddALTV  47697  nn0o1gt2ALTV  47698  nnpw2evenALTV  47706  perfectALTVlem1  47725  perfectALTVlem2  47726  fppr2odd  47735  341fppr2  47738  9fppr8  47741  nfermltl2rev  47747  sbgoldbalt  47785  mogoldbb  47789  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  gpg5order  48064  gpg5nbgrvtx13starlem2  48076  gpg3nbgrvtx0ALT  48081  gpg3kgrtriexlem5  48091  gpg5gricstgr3  48094  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  gpg5edgnedg  48134  2even  48243  zlmodzxzequa  48501  zlmodzxznm  48502  zlmodzxzequap  48504  zlmodzxzldeplem1  48505  zlmodzxzldeplem3  48507  zlmodzxzldep  48509  ldepsnlinclem1  48510  ldepsnlinc  48513  pw2m1lepw2m1  48525  fldivexpfllog2  48570  nnlog2ge0lt1  48571  logbpw2m1  48572  fllog2  48573  blennnelnn  48581  blenpw2  48583  nnpw2blenfzo  48586  blennnt2  48594  nnolog2flm1  48595  dig2nn0ld  48609  dig2nn1st  48610  0dig2pr01  48615  0dig2nn0o  48618  ackval42  48701  itsclc0xyqsolr  48774