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 2119  2c2 12227  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  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  21443  znidomb  21536  chfacfscmulfsupp  22842  chfacfpmmulfsupp  22846  minveclem2  25411  minveclem3  25414  pjthlem1  25422  dyaddisjlem  25580  mbfi1fseqlem5  25704  dvrecg  25958  dvexp3  25963  aaliou3lem6  26332  tanregt0  26521  efif1olem4  26527  tanarg  26601  cxpsqrtth  26712  2irrexpq  26713  2logb9irr  26777  2logb9irrALT  26780  sqrt2cxp2logb9e3  26781  cubic2  26830  asinlem3  26853  atantayl2  26920  cxp2limlem  26957  lgamgulmlem3  27012  lgamgulmlem4  27013  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  basellem8  27069  basellem9  27070  ppisval  27085  ppiprm  27132  ppinprm  27133  chtprm  27134  chtnprm  27135  chtdif  27139  ppidif  27144  ppi1  27145  cht1  27146  cht3  27154  ppieq0  27157  ppiublem1  27183  chpeq0  27189  chtub  27193  chpval2  27199  chpub  27201  mersenne  27208  perfect1  27209  perfectlem1  27210  perfectlem2  27211  bposlem1  27265  bposlem2  27266  bposlem3  27267  bposlem5  27269  bposlem6  27270  lgslem1  27278  lgsdir2lem2  27307  lgsdir2  27311  lgsqr  27332  gausslemma2dlem0i  27345  gausslemma2dlem1a  27346  gausslemma2dlem5a  27351  gausslemma2dlem5  27352  gausslemma2dlem6  27353  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquadlem2  27362  lgsquad2lem1  27365  lgsquad2lem2  27366  lgsquad2  27367  lgsquad3  27368  m1lgs  27369  2lgslem1a1  27370  2lgslem1a2  27371  2lgslem1b  27373  2lgslem3b1  27382  2lgslem3c1  27383  2lgs2  27386  2lgs  27388  2lgsoddprmlem2  27390  2lgsoddprmlem3  27395  2lgsoddprm  27397  2sqblem  27412  2sqmod  27417  chebbnd1lem1  27450  chebbnd1lem3  27452  chebbnd1  27453  dchrisum0lem1a  27467  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  mulog2sumlem2  27516  pntlemd  27575  pntlema  27577  pntlemb  27578  pntlemh  27580  pntlemr  27583  pntlemf  27586  pntlemo  27588  istrkg2ld  28546  istrkg3ld  28547  axlowdimlem3  29031  axlowdimlem6  29034  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  usgrexmpldifpr  29345  usgrexmplef  29346  cusgrsizeindb1  29537  pthdlem1  29852  clwlkclwwlklem2a1  30080  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwwisshclwwslem  30102  eupth2lem3lem3  30318  konigsberglem5  30344  2clwwlk2  30436  numclwwlk2lem1  30464  numclwlk2lem2f  30465  frgrreggt1  30481  ex-fl  30535  ex-mod  30537  ex-hash  30541  ex-dvds  30544  ex-ind-dvds  30549  minvecolem3  30965  pjhthlem1  31480  wrdt2ind  33032  archirngz  33270  archiabllem2c  33276  evl1deg2  33660  rtelextdg2  33911  constrext2chnlem  33934  constrresqrtcl  33961  2sqr3minply  33964  cos9thpiminplylem2  33967  cos9thpiminplylem5  33970  lmat22det  34006  dya2ub  34454  dya2icoseg  34461  oddpwdc  34538  eulerpartlemd  34550  eulerpartlemt  34555  ballotlem2  34673  signslema  34746  prodfzo03  34787  hgt750leme  34842  tgoldbachgtde  34844  nn0prpwlem  36550  knoppndvlem2  36819  knoppndvlem8  36825  irrdifflemf  37685  qdiff  37687  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  logblebd  42462  lcm2un  42499  lcm3un  42500  lcmineqlem18  42531  lcmineqlem19  42532  lcmineqlem21  42534  lcmineqlem22  42535  3lexlogpow5ineq2  42540  3lexlogpow2ineq1  42543  aks4d1p1p3  42554  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p3  42563  aks4d1p6  42566  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  posbezout  42585  5bc2eq10  42627  2np3bcnp1  42629  2ap1caineq  42630  aks6d1c6lem4  42658  aks6d1c7lem1  42665  aks6d1c7lem2  42666  flt4lem2  43097  flt4lem5  43100  flt4lem7  43109  nna4b4nsq  43110  acongrep  43425  acongeq  43428  jm2.18  43433  jm2.22  43440  jm2.23  43441  jm2.20nn  43442  jm2.26a  43445  jm2.26  43447  jm2.15nn0  43448  jm2.27a  43450  jm2.27c  43452  rmydioph  43459  jm3.1lem1  43462  jm3.1lem3  43464  expdiophlem1  43466  expdiophlem2  43467  hashnzfz2  44765  sumnnodd  46075  coskpi2  46309  cosknegpi  46312  dvdivbd  46366  stoweidlem26  46469  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem3  46519  stirlinglem7  46523  stirlinglem8  46524  stirlinglem10  46526  stirlinglem11  46527  stirlinglem15  46531  dirkertrigeqlem1  46541  dirkercncflem2  46547  fourierdlem54  46603  fourierdlem56  46605  fourierdlem57  46606  fourierdlem102  46651  fourierdlem114  46663  fourierswlem  46673  fouriersw  46674  smfmullem4  47237  nthrucw  47331  evenwodadd  47332  nnmul2  47793  ceil5half3  47809  addmodne  47813  m1modnep2mod  47821  minusmodnep2tmod  47822  modmkpkne  47830  modmknepk  47831  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  2timesltsq  47841  2timesltsqm1  47842  fmtnorec1  48015  goldbachthlem2  48024  odz2prm2pw  48041  fmtnoprmfac1  48043  fmtnoprmfac2lem1  48044  fmtnoprmfac2  48045  fmtno4prmfac  48050  31prm  48075  sfprmdvdsmersenne  48081  lighneallem1  48083  lighneallem4a  48086  lighneallem4b  48087  lighneallem4  48088  proththdlem  48091  proththd  48092  3exp4mod41  48094  41prothprmlem2  48096  nprmdvdsfacm1lem1  48098  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  ppivalnnnprmge6  48104  ppivalnn  48110  m1expevenALTV  48138  dfeven2  48140  m2even  48145  gcd2odd1  48159  oexpnegALTV  48168  oexpnegnz  48169  2evenALTV  48183  2noddALTV  48184  nn0o1gt2ALTV  48185  nnpw2evenALTV  48193  perfectALTVlem1  48212  perfectALTVlem2  48213  fppr2odd  48222  341fppr2  48225  9fppr8  48228  nfermltl2rev  48234  sbgoldbalt  48272  mogoldbb  48276  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  gpg5order  48551  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0ALT  48568  gpg3kgrtriexlem5  48578  gpg5gricstgr3  48581  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  gpg5edgnedg  48621  2even  48730  zlmodzxzequa  48987  zlmodzxznm  48988  zlmodzxzequap  48990  zlmodzxzldeplem1  48991  zlmodzxzldeplem3  48993  zlmodzxzldep  48995  ldepsnlinclem1  48996  ldepsnlinc  48999  pw2m1lepw2m1  49011  fldivexpfllog2  49056  nnlog2ge0lt1  49057  logbpw2m1  49058  fllog2  49059  blennnelnn  49067  blenpw2  49069  nnpw2blenfzo  49072  blennnt2  49080  nnolog2flm1  49081  dig2nn0ld  49095  dig2nn1st  49096  0dig2pr01  49101  0dig2nn0o  49104  ackval42  49187  itsclc0xyqsolr  49260