Theorem 2z 12565

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

Syntax hints:   ∈ wcel 2109  2c2 12241  ℤcz 12529

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-2 12249  df-z 12530

This theorem is referenced by:  nn0lt2  12597  nn0le2is012  12598  zadd2cl  12646  2eluzge1  12841  uzuzle23  12843  uzuzle24  12844  eluz2b1  12878  nn01to3  12900  nn0ge2m1nnALT  12901  ige2m1fz  13578  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  fzctr  13601  fzo0to2pr  13711  fzo0to42pr  13714  2tnp1ge0ge0  13791  flhalf  13792  m1modge3gt1  13883  2txmodxeq0  13896  f13idfv  13965  sqrecd  14115  znsqcld  14127  sq1  14160  expnass  14173  sqoddm1div8  14208  bcn2m1  14289  bcn2p1  14290  4bc2eq6  14294  hashtpg  14450  ccat2s1p2  14595  pfxtrcfv0  14659  pfxtrcfvl  14662  eqwrds3  14927  iseraltlem2  15649  iseraltlem3  15650  climcndslem1  15815  climcnds  15817  bpolydiflem  16020  efgt0  16071  tanval3  16102  cos01bnd  16154  cos01gt0  16159  odd2np1  16311  even2n  16312  oddm1even  16313  oddp1even  16314  oexpneg  16315  mod2eq1n2dvds  16317  2tp1odd  16322  2teven  16325  evend2  16327  oddp1d2  16328  ltoddhalfle  16331  opoe  16333  omoe  16334  opeo  16335  omeo  16336  z0even  16337  z2even  16340  z4even  16342  4dvdseven  16343  m1expo  16345  m1exp1  16346  nn0o  16353  sumeven  16357  flodddiv4  16385  bits0e  16399  bits0o  16400  bitsp1e  16402  bitsp1o  16403  bitsfzo  16405  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  bitsinv1  16412  6gcd4e2  16508  3lcm2e6woprm  16585  lcmf2a3a4e12  16617  isprm3  16653  dvdsnprmd  16660  2prm  16662  2mulprm  16663  oddprmge3  16670  ge2nprmge4  16671  isprm7  16678  divgcdodd  16680  oddprm  16781  pythagtriplem4  16790  pythagtriplem11  16796  pythagtriplem13  16798  iserodd  16806  prmgaplem3  17024  prmgaplem7  17028  dec2dvds  17034  prmlem0  17076  4001lem1  17111  psgnunilem4  19427  efgredleme  19673  lt6abl  19825  ablsimpgfindlem1  20039  ablsimpgfindlem2  20040  zringndrg  21378  znidomb  21471  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  minveclem2  25326  minveclem3  25329  pjthlem1  25337  dyaddisjlem  25496  mbfi1fseqlem5  25620  dvrecg  25877  dvexp3  25882  aaliou3lem6  26256  tanregt0  26448  efif1olem4  26454  tanarg  26528  cxpsqrtth  26639  2irrexpq  26640  2logb9irr  26705  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  cubic2  26758  asinlem3  26781  atantayl2  26848  cxp2limlem  26886  lgamgulmlem3  26941  lgamgulmlem4  26942  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  basellem8  26998  basellem9  26999  ppisval  27014  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  chtdif  27068  ppidif  27073  ppi1  27074  cht1  27075  cht3  27083  ppieq0  27086  ppiublem1  27113  chpeq0  27119  chtub  27123  chpval2  27129  chpub  27131  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgslem1  27208  lgsdir2lem2  27237  lgsdir2  27241  lgsqr  27262  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  gausslemma2dlem5a  27281  gausslemma2dlem5  27282  gausslemma2dlem6  27283  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem1  27295  lgsquad2lem2  27296  lgsquad2  27297  lgsquad3  27298  m1lgs  27299  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1b  27303  2lgslem3b1  27312  2lgslem3c1  27313  2lgs2  27316  2lgs  27318  2lgsoddprmlem2  27320  2lgsoddprmlem3  27325  2lgsoddprm  27327  2sqblem  27342  2sqmod  27347  chebbnd1lem1  27380  chebbnd1lem3  27382  chebbnd1  27383  dchrisum0lem1a  27397  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  mulog2sumlem2  27446  pntlemd  27505  pntlema  27507  pntlemb  27508  pntlemh  27510  pntlemr  27513  pntlemf  27516  pntlemo  27518  istrkg2ld  28387  istrkg3ld  28388  axlowdimlem3  28871  axlowdimlem6  28874  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  usgrexmpldifpr  29185  usgrexmplef  29186  cusgrsizeindb1  29378  pthdlem1  29696  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwwisshclwwslem  29943  eupth2lem3lem3  30159  konigsberglem5  30185  2clwwlk2  30277  numclwwlk2lem1  30305  numclwlk2lem2f  30306  frgrreggt1  30322  ex-fl  30376  ex-mod  30378  ex-hash  30382  ex-dvds  30385  ex-ind-dvds  30390  minvecolem3  30805  pjhthlem1  31320  wrdt2ind  32875  archirngz  33143  archiabllem2c  33149  evl1deg2  33546  rtelextdg2  33717  constrext2chnlem  33740  constrresqrtcl  33767  2sqr3minply  33770  cos9thpiminplylem2  33773  cos9thpiminplylem5  33776  lmat22det  33812  dya2ub  34261  dya2icoseg  34268  oddpwdc  34345  eulerpartlemd  34357  eulerpartlemt  34362  ballotlem2  34480  signslema  34553  prodfzo03  34594  hgt750leme  34649  tgoldbachgtde  34651  nn0prpwlem  36310  knoppndvlem2  36501  knoppndvlem8  36507  irrdifflemf  37313  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  logblebd  41964  lcm2un  42002  lcm3un  42003  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem21  42037  lcmineqlem22  42038  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  aks4d1p1p3  42057  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  5bc2eq10  42130  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7lem2  42169  flt4lem2  42635  flt4lem5  42638  flt4lem7  42647  nna4b4nsq  42648  acongrep  42969  acongeq  42972  jm2.18  42977  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.26a  42989  jm2.26  42991  jm2.15nn0  42992  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  jm3.1lem1  43006  jm3.1lem3  43008  expdiophlem1  43010  expdiophlem2  43011  hashnzfz2  44310  sumnnodd  45628  coskpi2  45864  cosknegpi  45867  dvdivbd  45921  stoweidlem26  46024  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem15  46086  dirkertrigeqlem1  46096  dirkercncflem2  46102  fourierdlem54  46158  fourierdlem56  46160  fourierdlem57  46161  fourierdlem102  46206  fourierdlem114  46218  fourierswlem  46228  fouriersw  46229  smfmullem4  46792  evenwodadd  46886  ceil5half3  47341  addmodne  47345  m1modnep2mod  47353  minusmodnep2tmod  47354  modmkpkne  47362  modmknepk  47363  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  fmtnorec1  47538  goldbachthlem2  47547  odz2prm2pw  47564  fmtnoprmfac1  47566  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  fmtno4prmfac  47573  31prm  47598  sfprmdvdsmersenne  47604  lighneallem1  47606  lighneallem4a  47609  lighneallem4b  47610  lighneallem4  47611  proththdlem  47614  proththd  47615  3exp4mod41  47617  41prothprmlem2  47619  m1expevenALTV  47648  dfeven2  47650  m2even  47655  gcd2odd1  47669  oexpnegALTV  47678  oexpnegnz  47679  2evenALTV  47693  2noddALTV  47694  nn0o1gt2ALTV  47695  nnpw2evenALTV  47703  perfectALTVlem1  47722  perfectALTVlem2  47723  fppr2odd  47732  341fppr2  47735  9fppr8  47738  nfermltl2rev  47744  sbgoldbalt  47782  mogoldbb  47786  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  gpg5order  48051  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0ALT  48068  gpg3kgrtriexlem5  48078  gpg5gricstgr3  48081  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  2even  48227  zlmodzxzequa  48485  zlmodzxznm  48486  zlmodzxzequap  48488  zlmodzxzldeplem1  48489  zlmodzxzldeplem3  48491  zlmodzxzldep  48493  ldepsnlinclem1  48494  ldepsnlinc  48497  pw2m1lepw2m1  48509  fldivexpfllog2  48554  nnlog2ge0lt1  48555  logbpw2m1  48556  fllog2  48557  blennnelnn  48565  blenpw2  48567  nnpw2blenfzo  48570  blennnt2  48578  nnolog2flm1  48579  dig2nn0ld  48593  dig2nn1st  48594  0dig2pr01  48599  0dig2nn0o  48602  ackval42  48685  itsclc0xyqsolr  48758