Theorem 2z 12535

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

Syntax hints:   ∈ wcel 2114  2c2 12212  ℤcz 12500

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-2 12220  df-z 12501

This theorem is referenced by:  nn0lt2  12567  nn0le2is012  12568  zadd2cl  12616  2eluzge1  12807  uzuzle23  12809  uzuzle24  12810  eluz2b1  12844  nn01to3  12866  nn0ge2m1nnALT  12867  ige2m1fz  13545  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  fzctr  13568  fzo0to2pr  13678  fzo0to42pr  13681  2tnp1ge0ge0  13761  flhalf  13762  m1modge3gt1  13853  2txmodxeq0  13866  f13idfv  13935  sqrecd  14085  znsqcld  14097  sq1  14130  expnass  14143  sqoddm1div8  14178  bcn2m1  14259  bcn2p1  14260  4bc2eq6  14264  hashtpg  14420  ccat2s1p2  14566  pfxtrcfv0  14629  pfxtrcfvl  14632  eqwrds3  14896  iseraltlem2  15618  iseraltlem3  15619  climcndslem1  15784  climcnds  15786  bpolydiflem  15989  efgt0  16040  tanval3  16071  cos01bnd  16123  cos01gt0  16128  odd2np1  16280  even2n  16281  oddm1even  16282  oddp1even  16283  oexpneg  16284  mod2eq1n2dvds  16286  2tp1odd  16291  2teven  16294  evend2  16296  oddp1d2  16297  ltoddhalfle  16300  opoe  16302  omoe  16303  opeo  16304  omeo  16305  z0even  16306  z2even  16309  z4even  16311  4dvdseven  16312  m1expo  16314  m1exp1  16315  nn0o  16322  sumeven  16326  flodddiv4  16354  bits0e  16368  bits0o  16369  bitsp1e  16371  bitsp1o  16372  bitsfzo  16374  bitsmod  16375  bitscmp  16377  bitsinv1lem  16380  bitsinv1  16381  6gcd4e2  16477  3lcm2e6woprm  16554  lcmf2a3a4e12  16586  isprm3  16622  dvdsnprmd  16629  2prm  16631  2mulprm  16632  oddprmge3  16639  ge2nprmge4  16640  isprm7  16647  divgcdodd  16649  oddprm  16750  pythagtriplem4  16759  pythagtriplem11  16765  pythagtriplem13  16767  iserodd  16775  prmgaplem3  16993  prmgaplem7  16997  dec2dvds  17003  prmlem0  17045  4001lem1  17080  ex-chn1  18572  psgnunilem4  19438  efgredleme  19684  lt6abl  19836  ablsimpgfindlem1  20050  ablsimpgfindlem2  20051  zringndrg  21435  znidomb  21528  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  minveclem2  25394  minveclem3  25397  pjthlem1  25405  dyaddisjlem  25564  mbfi1fseqlem5  25688  dvrecg  25945  dvexp3  25950  aaliou3lem6  26324  tanregt0  26516  efif1olem4  26522  tanarg  26596  cxpsqrtth  26707  2irrexpq  26708  2logb9irr  26773  2logb9irrALT  26776  sqrt2cxp2logb9e3  26777  cubic2  26826  asinlem3  26849  atantayl2  26916  cxp2limlem  26954  lgamgulmlem3  27009  lgamgulmlem4  27010  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  basellem8  27066  basellem9  27067  ppisval  27082  ppiprm  27129  ppinprm  27130  chtprm  27131  chtnprm  27132  chtdif  27136  ppidif  27141  ppi1  27142  cht1  27143  cht3  27151  ppieq0  27154  ppiublem1  27181  chpeq0  27187  chtub  27191  chpval2  27197  chpub  27199  mersenne  27206  perfect1  27207  perfectlem1  27208  perfectlem2  27209  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgslem1  27276  lgsdir2lem2  27305  lgsdir2  27309  lgsqr  27330  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  gausslemma2dlem5a  27349  gausslemma2dlem5  27350  gausslemma2dlem6  27351  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem1  27363  lgsquad2lem2  27364  lgsquad2  27365  lgsquad3  27366  m1lgs  27367  2lgslem1a1  27368  2lgslem1a2  27369  2lgslem1b  27371  2lgslem3b1  27380  2lgslem3c1  27381  2lgs2  27384  2lgs  27386  2lgsoddprmlem2  27388  2lgsoddprmlem3  27393  2lgsoddprm  27395  2sqblem  27410  2sqmod  27415  chebbnd1lem1  27448  chebbnd1lem3  27450  chebbnd1  27451  dchrisum0lem1a  27465  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  mulog2sumlem2  27514  pntlemd  27573  pntlema  27575  pntlemb  27576  pntlemh  27578  pntlemr  27581  pntlemf  27584  pntlemo  27586  istrkg2ld  28544  istrkg3ld  28545  axlowdimlem3  29029  axlowdimlem6  29032  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  usgrexmpldifpr  29343  usgrexmplef  29344  cusgrsizeindb1  29536  pthdlem1  29851  clwlkclwwlklem2a1  30079  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwwisshclwwslem  30101  eupth2lem3lem3  30317  konigsberglem5  30343  2clwwlk2  30435  numclwwlk2lem1  30463  numclwlk2lem2f  30464  frgrreggt1  30480  ex-fl  30534  ex-mod  30536  ex-hash  30540  ex-dvds  30543  ex-ind-dvds  30548  minvecolem3  30963  pjhthlem1  31478  wrdt2ind  33045  archirngz  33282  archiabllem2c  33288  evl1deg2  33669  rtelextdg2  33904  constrext2chnlem  33927  constrresqrtcl  33954  2sqr3minply  33957  cos9thpiminplylem2  33960  cos9thpiminplylem5  33963  lmat22det  33999  dya2ub  34447  dya2icoseg  34454  oddpwdc  34531  eulerpartlemd  34543  eulerpartlemt  34548  ballotlem2  34666  signslema  34739  prodfzo03  34780  hgt750leme  34835  tgoldbachgtde  34837  nn0prpwlem  36535  knoppndvlem2  36732  knoppndvlem8  36738  irrdifflemf  37577  poimirlem25  37893  poimirlem26  37894  poimirlem27  37895  poimirlem28  37896  logblebd  42343  lcm2un  42381  lcm3un  42382  lcmineqlem18  42413  lcmineqlem19  42414  lcmineqlem21  42416  lcmineqlem22  42417  3lexlogpow5ineq2  42422  3lexlogpow2ineq1  42425  aks4d1p1p3  42436  aks4d1p1p4  42438  aks4d1p1p6  42440  aks4d1p1p7  42441  aks4d1p1p5  42442  aks4d1p1  42443  aks4d1p3  42445  aks4d1p6  42448  aks4d1p7d1  42449  aks4d1p7  42450  aks4d1p8  42454  aks4d1p9  42455  posbezout  42467  5bc2eq10  42509  2np3bcnp1  42511  2ap1caineq  42512  aks6d1c6lem4  42540  aks6d1c7lem1  42547  aks6d1c7lem2  42548  flt4lem2  43002  flt4lem5  43005  flt4lem7  43014  nna4b4nsq  43015  acongrep  43334  acongeq  43337  jm2.18  43342  jm2.22  43349  jm2.23  43350  jm2.20nn  43351  jm2.26a  43354  jm2.26  43356  jm2.15nn0  43357  jm2.27a  43359  jm2.27c  43361  rmydioph  43368  jm3.1lem1  43371  jm3.1lem3  43373  expdiophlem1  43375  expdiophlem2  43376  hashnzfz2  44674  sumnnodd  45987  coskpi2  46221  cosknegpi  46224  dvdivbd  46278  stoweidlem26  46381  wallispilem4  46423  wallispi2lem1  46426  wallispi2lem2  46427  wallispi2  46428  stirlinglem1  46429  stirlinglem3  46431  stirlinglem7  46435  stirlinglem8  46436  stirlinglem10  46438  stirlinglem11  46439  stirlinglem15  46443  dirkertrigeqlem1  46453  dirkercncflem2  46459  fourierdlem54  46515  fourierdlem56  46517  fourierdlem57  46518  fourierdlem102  46563  fourierdlem114  46575  fourierswlem  46585  fouriersw  46586  smfmullem4  47149  nthrucw  47241  evenwodadd  47242  ceil5half3  47697  addmodne  47701  m1modnep2mod  47709  minusmodnep2tmod  47710  modmkpkne  47718  modmknepk  47719  modm2nep1  47723  modp2nep1  47724  modm1nep2  47725  modm1nem2  47726  fmtnorec1  47894  goldbachthlem2  47903  odz2prm2pw  47920  fmtnoprmfac1  47922  fmtnoprmfac2lem1  47923  fmtnoprmfac2  47924  fmtno4prmfac  47929  31prm  47954  sfprmdvdsmersenne  47960  lighneallem1  47962  lighneallem4a  47965  lighneallem4b  47966  lighneallem4  47967  proththdlem  47970  proththd  47971  3exp4mod41  47973  41prothprmlem2  47975  m1expevenALTV  48004  dfeven2  48006  m2even  48011  gcd2odd1  48025  oexpnegALTV  48034  oexpnegnz  48035  2evenALTV  48049  2noddALTV  48050  nn0o1gt2ALTV  48051  nnpw2evenALTV  48059  perfectALTVlem1  48078  perfectALTVlem2  48079  fppr2odd  48088  341fppr2  48091  9fppr8  48094  nfermltl2rev  48100  sbgoldbalt  48138  mogoldbb  48142  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  wtgoldbnnsum4prm  48159  bgoldbnnsum3prm  48161  gpg5order  48417  gpg5nbgrvtx13starlem2  48429  gpg3nbgrvtx0ALT  48434  gpg3kgrtriexlem5  48444  gpg5gricstgr3  48447  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  gpg5edgnedg  48487  2even  48596  zlmodzxzequa  48853  zlmodzxznm  48854  zlmodzxzequap  48856  zlmodzxzldeplem1  48857  zlmodzxzldeplem3  48859  zlmodzxzldep  48861  ldepsnlinclem1  48862  ldepsnlinc  48865  pw2m1lepw2m1  48877  fldivexpfllog2  48922  nnlog2ge0lt1  48923  logbpw2m1  48924  fllog2  48925  blennnelnn  48933  blenpw2  48935  nnpw2blenfzo  48938  blennnt2  48946  nnolog2flm1  48947  dig2nn0ld  48961  dig2nn1st  48962  0dig2pr01  48967  0dig2nn0o  48970  ackval42  49053  itsclc0xyqsolr  49126