Theorem 2z 12514

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

Syntax hints:   ∈ wcel 2113  2c2 12191  ℤcz 12479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-i2m1 11085  ax-1ne0 11086  ax-rrecex 11089  ax-cnre 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-neg 11358  df-nn 12137  df-2 12199  df-z 12480

This theorem is referenced by:  nn0lt2  12546  nn0le2is012  12547  zadd2cl  12595  2eluzge1  12786  uzuzle23  12788  uzuzle24  12789  eluz2b1  12823  nn01to3  12845  nn0ge2m1nnALT  12846  ige2m1fz  13524  fz0to3un2pr  13536  fz0to4untppr  13537  fz0to5un2tp  13538  fzctr  13547  fzo0to2pr  13657  fzo0to42pr  13660  2tnp1ge0ge0  13740  flhalf  13741  m1modge3gt1  13832  2txmodxeq0  13845  f13idfv  13914  sqrecd  14064  znsqcld  14076  sq1  14109  expnass  14122  sqoddm1div8  14157  bcn2m1  14238  bcn2p1  14239  4bc2eq6  14243  hashtpg  14399  ccat2s1p2  14545  pfxtrcfv0  14608  pfxtrcfvl  14611  eqwrds3  14875  iseraltlem2  15597  iseraltlem3  15598  climcndslem1  15763  climcnds  15765  bpolydiflem  15968  efgt0  16019  tanval3  16050  cos01bnd  16102  cos01gt0  16107  odd2np1  16259  even2n  16260  oddm1even  16261  oddp1even  16262  oexpneg  16263  mod2eq1n2dvds  16265  2tp1odd  16270  2teven  16273  evend2  16275  oddp1d2  16276  ltoddhalfle  16279  opoe  16281  omoe  16282  opeo  16283  omeo  16284  z0even  16285  z2even  16288  z4even  16290  4dvdseven  16291  m1expo  16293  m1exp1  16294  nn0o  16301  sumeven  16305  flodddiv4  16333  bits0e  16347  bits0o  16348  bitsp1e  16350  bitsp1o  16351  bitsfzo  16353  bitsmod  16354  bitscmp  16356  bitsinv1lem  16359  bitsinv1  16360  6gcd4e2  16456  3lcm2e6woprm  16533  lcmf2a3a4e12  16565  isprm3  16601  dvdsnprmd  16608  2prm  16610  2mulprm  16611  oddprmge3  16618  ge2nprmge4  16619  isprm7  16626  divgcdodd  16628  oddprm  16729  pythagtriplem4  16738  pythagtriplem11  16744  pythagtriplem13  16746  iserodd  16754  prmgaplem3  16972  prmgaplem7  16976  dec2dvds  16982  prmlem0  17024  4001lem1  17059  ex-chn1  18551  psgnunilem4  19417  efgredleme  19663  lt6abl  19815  ablsimpgfindlem1  20029  ablsimpgfindlem2  20030  zringndrg  21414  znidomb  21507  chfacfscmulfsupp  22794  chfacfpmmulfsupp  22798  minveclem2  25373  minveclem3  25376  pjthlem1  25384  dyaddisjlem  25543  mbfi1fseqlem5  25667  dvrecg  25924  dvexp3  25929  aaliou3lem6  26303  tanregt0  26495  efif1olem4  26501  tanarg  26575  cxpsqrtth  26686  2irrexpq  26687  2logb9irr  26752  2logb9irrALT  26755  sqrt2cxp2logb9e3  26756  cubic2  26805  asinlem3  26828  atantayl2  26895  cxp2limlem  26933  lgamgulmlem3  26988  lgamgulmlem4  26989  basellem2  27039  basellem3  27040  basellem4  27041  basellem5  27042  basellem8  27045  basellem9  27046  ppisval  27061  ppiprm  27108  ppinprm  27109  chtprm  27110  chtnprm  27111  chtdif  27115  ppidif  27120  ppi1  27121  cht1  27122  cht3  27130  ppieq0  27133  ppiublem1  27160  chpeq0  27166  chtub  27170  chpval2  27176  chpub  27178  mersenne  27185  perfect1  27186  perfectlem1  27187  perfectlem2  27188  bposlem1  27242  bposlem2  27243  bposlem3  27244  bposlem5  27246  bposlem6  27247  lgslem1  27255  lgsdir2lem2  27284  lgsdir2  27288  lgsqr  27309  gausslemma2dlem0i  27322  gausslemma2dlem1a  27323  gausslemma2dlem5a  27328  gausslemma2dlem5  27329  gausslemma2dlem6  27330  gausslemma2dlem7  27331  gausslemma2d  27332  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgseisenlem4  27336  lgsquadlem1  27338  lgsquadlem2  27339  lgsquad2lem1  27342  lgsquad2lem2  27343  lgsquad2  27344  lgsquad3  27345  m1lgs  27346  2lgslem1a1  27347  2lgslem1a2  27348  2lgslem1b  27350  2lgslem3b1  27359  2lgslem3c1  27360  2lgs2  27363  2lgs  27365  2lgsoddprmlem2  27367  2lgsoddprmlem3  27372  2lgsoddprm  27374  2sqblem  27389  2sqmod  27394  chebbnd1lem1  27427  chebbnd1lem3  27429  chebbnd1  27430  dchrisum0lem1a  27444  dchrvmasumiflem1  27459  dchrisum0flblem1  27466  dchrisum0flblem2  27467  dchrisum0lem1b  27473  dchrisum0lem1  27474  dchrisum0lem2a  27475  dchrisum0lem2  27476  dchrisum0lem3  27477  mulog2sumlem2  27493  pntlemd  27552  pntlema  27554  pntlemb  27555  pntlemh  27557  pntlemr  27560  pntlemf  27563  pntlemo  27565  istrkg2ld  28458  istrkg3ld  28459  axlowdimlem3  28943  axlowdimlem6  28946  axlowdimlem16  28956  axlowdimlem17  28957  axlowdim  28960  usgrexmpldifpr  29257  usgrexmplef  29258  cusgrsizeindb1  29450  pthdlem1  29765  clwlkclwwlklem2a1  29993  clwlkclwwlklem2fv1  29996  clwlkclwwlklem2fv2  29997  clwlkclwwlklem2a4  29998  clwlkclwwlklem2a  29999  clwwisshclwwslem  30015  eupth2lem3lem3  30231  konigsberglem5  30257  2clwwlk2  30349  numclwwlk2lem1  30377  numclwlk2lem2f  30378  frgrreggt1  30394  ex-fl  30448  ex-mod  30450  ex-hash  30454  ex-dvds  30457  ex-ind-dvds  30462  minvecolem3  30877  pjhthlem1  31392  wrdt2ind  32963  archirngz  33199  archiabllem2c  33205  evl1deg2  33586  rtelextdg2  33812  constrext2chnlem  33835  constrresqrtcl  33862  2sqr3minply  33865  cos9thpiminplylem2  33868  cos9thpiminplylem5  33871  lmat22det  33907  dya2ub  34355  dya2icoseg  34362  oddpwdc  34439  eulerpartlemd  34451  eulerpartlemt  34456  ballotlem2  34574  signslema  34647  prodfzo03  34688  hgt750leme  34743  tgoldbachgtde  34745  nn0prpwlem  36438  knoppndvlem2  36629  knoppndvlem8  36635  irrdifflemf  37442  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  logblebd  42142  lcm2un  42180  lcm3un  42181  lcmineqlem18  42212  lcmineqlem19  42213  lcmineqlem21  42215  lcmineqlem22  42216  3lexlogpow5ineq2  42221  3lexlogpow2ineq1  42224  aks4d1p1p3  42235  aks4d1p1p4  42237  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  aks4d1p3  42244  aks4d1p6  42247  aks4d1p7d1  42248  aks4d1p7  42249  aks4d1p8  42253  aks4d1p9  42254  posbezout  42266  5bc2eq10  42308  2np3bcnp1  42310  2ap1caineq  42311  aks6d1c6lem4  42339  aks6d1c7lem1  42346  aks6d1c7lem2  42347  flt4lem2  42805  flt4lem5  42808  flt4lem7  42817  nna4b4nsq  42818  acongrep  43137  acongeq  43140  jm2.18  43145  jm2.22  43152  jm2.23  43153  jm2.20nn  43154  jm2.26a  43157  jm2.26  43159  jm2.15nn0  43160  jm2.27a  43162  jm2.27c  43164  rmydioph  43171  jm3.1lem1  43174  jm3.1lem3  43176  expdiophlem1  43178  expdiophlem2  43179  hashnzfz2  44478  sumnnodd  45792  coskpi2  46026  cosknegpi  46029  dvdivbd  46083  stoweidlem26  46186  wallispilem4  46228  wallispi2lem1  46231  wallispi2lem2  46232  wallispi2  46233  stirlinglem1  46234  stirlinglem3  46236  stirlinglem7  46240  stirlinglem8  46241  stirlinglem10  46243  stirlinglem11  46244  stirlinglem15  46248  dirkertrigeqlem1  46258  dirkercncflem2  46264  fourierdlem54  46320  fourierdlem56  46322  fourierdlem57  46323  fourierdlem102  46368  fourierdlem114  46380  fourierswlem  46390  fouriersw  46391  smfmullem4  46954  nthrucw  47046  evenwodadd  47047  ceil5half3  47502  addmodne  47506  m1modnep2mod  47514  minusmodnep2tmod  47515  modmkpkne  47523  modmknepk  47524  modm2nep1  47528  modp2nep1  47529  modm1nep2  47530  modm1nem2  47531  fmtnorec1  47699  goldbachthlem2  47708  odz2prm2pw  47725  fmtnoprmfac1  47727  fmtnoprmfac2lem1  47728  fmtnoprmfac2  47729  fmtno4prmfac  47734  31prm  47759  sfprmdvdsmersenne  47765  lighneallem1  47767  lighneallem4a  47770  lighneallem4b  47771  lighneallem4  47772  proththdlem  47775  proththd  47776  3exp4mod41  47778  41prothprmlem2  47780  m1expevenALTV  47809  dfeven2  47811  m2even  47816  gcd2odd1  47830  oexpnegALTV  47839  oexpnegnz  47840  2evenALTV  47854  2noddALTV  47855  nn0o1gt2ALTV  47856  nnpw2evenALTV  47864  perfectALTVlem1  47883  perfectALTVlem2  47884  fppr2odd  47893  341fppr2  47896  9fppr8  47899  nfermltl2rev  47905  sbgoldbalt  47943  mogoldbb  47947  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  gpg5order  48222  gpg5nbgrvtx13starlem2  48234  gpg3nbgrvtx0ALT  48239  gpg3kgrtriexlem5  48249  gpg5gricstgr3  48252  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  gpg5edgnedg  48292  2even  48401  zlmodzxzequa  48658  zlmodzxznm  48659  zlmodzxzequap  48661  zlmodzxzldeplem1  48662  zlmodzxzldeplem3  48664  zlmodzxzldep  48666  ldepsnlinclem1  48667  ldepsnlinc  48670  pw2m1lepw2m1  48682  fldivexpfllog2  48727  nnlog2ge0lt1  48728  logbpw2m1  48729  fllog2  48730  blennnelnn  48738  blenpw2  48740  nnpw2blenfzo  48743  blennnt2  48751  nnolog2flm1  48752  dig2nn0ld  48766  dig2nn1st  48767  0dig2pr01  48772  0dig2nn0o  48775  ackval42  48858  itsclc0xyqsolr  48931