Theorem 2z 12622

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

Syntax hints:   ∈ wcel 2149  2c2 12291  ℤcz 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rrecex 11168  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-neg 11440  df-nn 12230  df-2 12299  df-z 12588

This theorem is referenced by:  nn0lt2  12655  nn0le2is012  12656  zadd2cl  12704  2eluzge1  12902  uzuzle23  12904  uzuzle24  12905  eluz2b1  12939  nn01to3  12961  nn0ge2m1nnALT  12962  ige2m1fz  13641  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzctr  13664  fzo0to2pr  13775  fzo0to42pr  13778  2tnp1ge0ge0  13858  flhalf  13859  m1modge3gt1  13950  2txmodxeq0  13963  f13idfv  14032  sqrecd  14182  znsqcld  14194  sq1  14227  expnass  14240  sqoddm1div8  14275  bcn2m1  14356  bcn2p1  14357  4bc2eq6  14361  hashtpg  14518  ccat2s1p2  14664  pfxtrcfv0  14727  pfxtrcfvl  14730  eqwrds3  14994  iseraltlem2  15730  iseraltlem3  15731  climcndslem1  15899  climcnds  15901  bpolydiflem  16104  efgt0  16155  tanval3  16186  cos01bnd  16238  cos01gt0  16243  odd2np1  16395  even2n  16396  oddm1even  16397  oddp1even  16398  oexpneg  16399  mod2eq1n2dvds  16401  2tp1odd  16406  2teven  16409  evend2  16411  oddp1d2  16412  ltoddhalfle  16415  opoe  16417  omoe  16418  opeo  16419  omeo  16420  z0even  16421  z2even  16424  z4even  16426  4dvdseven  16427  m1expo  16429  m1exp1  16430  nn0o  16437  sumeven  16441  flodddiv4  16469  bits0e  16483  bits0o  16484  bitsp1e  16486  bitsp1o  16487  bitsfzo  16489  bitsmod  16490  bitscmp  16492  bitsinv1lem  16495  bitsinv1  16496  6gcd4e2  16592  3lcm2e6woprm  16669  lcmf2a3a4e12  16701  isprm3  16737  dvdsnprmd  16744  2prm  16746  2mulprm  16747  oddprmge3  16755  ge2nprmge4  16756  isprm7  16763  divgcdodd  16765  oddprm  16866  pythagtriplem4  16875  pythagtriplem11  16881  pythagtriplem13  16883  iserodd  16891  prmgaplem3  17109  prmgaplem7  17113  dec2dvds  17119  prmlem0  17161  4001lem1  17197  ex-chn1  18689  psgnunilem4  19563  efgredleme  19809  lt6abl  19961  ablsimpgfindlem1  20175  ablsimpgfindlem2  20176  zringndrg  21583  znidomb  21676  chfacfscmulfsupp  22981  chfacfpmmulfsupp  22985  minveclem2  25550  minveclem3  25553  pjthlem1  25561  dyaddisjlem  25719  mbfi1fseqlem5  25843  dvrecg  26097  dvexp3  26102  aaliou3lem6  26474  tanregt0  26666  efif1olem4  26672  tanarg  26746  cxpsqrtth  26857  2irrexpq  26858  2logb9irr  26922  2logb9irrALT  26925  sqrt2cxp2logb9e3  26926  cubic2  26975  asinlem3  26998  atantayl2  27065  cxp2limlem  27102  lgamgulmlem3  27157  lgamgulmlem4  27158  basellem2  27208  basellem3  27209  basellem4  27210  basellem5  27211  basellem8  27214  basellem9  27215  ppisval  27230  ppiprm  27277  ppinprm  27278  chtprm  27279  chtnprm  27280  chtdif  27284  ppidif  27289  ppi1  27290  cht1  27291  cht3  27299  ppieq0  27302  ppiublem1  27328  chpeq0  27334  chtub  27338  chpval2  27344  chpub  27346  mersenne  27353  perfect1  27354  perfectlem1  27355  perfectlem2  27356  bposlem1  27410  bposlem2  27411  bposlem3  27412  bposlem5  27414  bposlem6  27415  lgslem1  27423  lgsdir2lem2  27452  lgsdir2  27456  lgsqr  27477  gausslemma2dlem0i  27490  gausslemma2dlem1a  27491  gausslemma2dlem5a  27496  gausslemma2dlem5  27497  gausslemma2dlem6  27498  gausslemma2dlem7  27499  gausslemma2d  27500  lgseisenlem1  27501  lgseisenlem2  27502  lgseisenlem3  27503  lgseisenlem4  27504  lgsquadlem1  27506  lgsquadlem2  27507  lgsquad2lem1  27510  lgsquad2lem2  27511  lgsquad2  27512  lgsquad3  27513  m1lgs  27514  2lgslem1a1  27515  2lgslem1a2  27516  2lgslem1b  27518  2lgslem3b1  27527  2lgslem3c1  27528  2lgs2  27531  2lgs  27533  2lgsoddprmlem2  27535  2lgsoddprmlem3  27540  2lgsoddprm  27542  2sqblem  27557  2sqmod  27562  chebbnd1lem1  27595  chebbnd1lem3  27597  chebbnd1  27598  dchrisum0lem1a  27612  dchrvmasumiflem1  27627  dchrisum0flblem1  27634  dchrisum0flblem2  27635  dchrisum0lem1b  27641  dchrisum0lem1  27642  dchrisum0lem2a  27643  dchrisum0lem2  27644  dchrisum0lem3  27645  mulog2sumlem2  27661  pntlemd  27720  pntlema  27722  pntlemb  27723  pntlemh  27725  pntlemr  27728  pntlemf  27731  pntlemo  27733  istrkg2ld  28691  istrkg3ld  28692  axlowdimlem3  29231  axlowdimlem6  29234  axlowdimlem16  29244  axlowdimlem17  29245  axlowdim  29248  usgrexmpldifpr  29545  usgrexmplef  29546  cusgrsizeindb1  29737  pthdlem1  30052  clwlkclwwlklem2a1  30280  clwlkclwwlklem2fv1  30283  clwlkclwwlklem2fv2  30284  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwwisshclwwslem  30302  eupth2lem3lem3  30518  konigsberglem5  30544  2clwwlk2  30636  numclwwlk2lem1  30664  numclwlk2lem2f  30665  frgrreggt1  30681  ex-fl  30735  ex-mod  30737  ex-hash  30741  ex-dvds  30744  ex-ind-dvds  30749  minvecolem3  31165  pjhthlem1  31680  wrdt2ind  33210  archirngz  33446  archiabllem2c  33452  evl1deg2  33808  rtelextdg2  34058  constrext2chnlem  34081  constrresqrtcl  34108  2sqr3minply  34111  cos9thpiminplylem2  34114  cos9thpiminplylem5  34117  lmat22det  34153  dya2ub  34601  dya2icoseg  34608  oddpwdc  34685  eulerpartlemd  34697  eulerpartlemt  34702  ballotlem2  34820  signslema  34890  prodfzo03  34931  hgt750leme  34986  tgoldbachgtde  34988  nn0prpwlem  36718  knoppndvlem2  36987  knoppndvlem8  36993  irrdifflemf  37852  qdiff  37854  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  poimirlem28  38182  logblebd  42629  lcm2un  42666  lcm3un  42667  lcmineqlem18  42698  lcmineqlem19  42699  lcmineqlem21  42701  lcmineqlem22  42702  3lexlogpow5ineq2  42707  3lexlogpow2ineq1  42710  aks4d1p1p3  42721  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p3  42730  aks4d1p6  42733  aks4d1p7d1  42734  aks4d1p7  42735  aks4d1p8  42739  aks4d1p9  42740  posbezout  42752  5bc2eq10  42794  2np3bcnp1  42796  2ap1caineq  42797  aks6d1c6lem4  42825  aks6d1c7lem1  42832  aks6d1c7lem2  42833  flt4lem2  43264  flt4lem5  43267  flt4lem7  43276  nna4b4nsq  43277  acongrep  43592  acongeq  43595  jm2.18  43600  jm2.22  43607  jm2.23  43608  jm2.20nn  43609  jm2.26a  43612  jm2.26  43614  jm2.15nn0  43615  jm2.27a  43617  jm2.27c  43619  rmydioph  43626  jm3.1lem1  43629  jm3.1lem3  43631  expdiophlem1  43633  expdiophlem2  43634  hashnzfz2  44916  sumnnodd  46231  coskpi2  46465  cosknegpi  46468  dvdivbd  46522  stoweidlem26  46625  wallispilem4  46667  wallispi2lem1  46670  wallispi2lem2  46671  wallispi2  46672  stirlinglem1  46673  stirlinglem3  46675  stirlinglem7  46679  stirlinglem8  46680  stirlinglem10  46682  stirlinglem11  46683  stirlinglem15  46687  dirkertrigeqlem1  46697  dirkercncflem2  46703  fourierdlem54  46759  fourierdlem56  46761  fourierdlem57  46762  fourierdlem102  46807  fourierdlem114  46819  fourierswlem  46829  fouriersw  46830  smfmullem4  47393  nthrucw  47487  evenwodadd  47488  nnmul2  47949  ceil5half3  47965  addmodne  47969  m1modnep2mod  47977  minusmodnep2tmod  47978  modmkpkne  47986  modmknepk  47987  modm2nep1  47991  modp2nep1  47992  modm1nep2  47993  modm1nem2  47994  2timesltsq  47997  2timesltsqm1  47998  fmtnorec1  48171  goldbachthlem2  48180  odz2prm2pw  48197  fmtnoprmfac1  48199  fmtnoprmfac2lem1  48200  fmtnoprmfac2  48201  fmtno4prmfac  48206  31prm  48231  sfprmdvdsmersenne  48237  lighneallem1  48239  lighneallem4a  48242  lighneallem4b  48243  lighneallem4  48244  proththdlem  48247  proththd  48248  3exp4mod41  48250  41prothprmlem2  48252  nprmdvdsfacm1lem1  48254  nprmdvdsfacm1lem2  48255  nprmdvdsfacm1lem4  48257  ppivalnnnprmge6  48260  ppivalnn  48266  m1expevenALTV  48294  dfeven2  48296  m2even  48301  gcd2odd1  48315  oexpnegALTV  48324  oexpnegnz  48325  2evenALTV  48339  2noddALTV  48340  nn0o1gt2ALTV  48341  nnpw2evenALTV  48349  perfectALTVlem1  48368  perfectALTVlem2  48369  fppr2odd  48378  341fppr2  48381  9fppr8  48384  nfermltl2rev  48390  sbgoldbalt  48428  mogoldbb  48432  nnsum4primesodd  48443  nnsum4primesoddALTV  48444  wtgoldbnnsum4prm  48449  bgoldbnnsum3prm  48451  gpg5order  48707  gpg5nbgrvtx13starlem2  48719  gpg3nbgrvtx0ALT  48724  gpg3kgrtriexlem5  48734  gpg5gricstgr3  48737  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  gpg5edgnedg  48777  2even  48886  zlmodzxzequa  49154  zlmodzxznm  49155  zlmodzxzequap  49157  zlmodzxzldeplem1  49158  zlmodzxzldeplem3  49160  zlmodzxzldep  49162  ldepsnlinclem1  49163  ldepsnlinc  49166  pw2m1lepw2m1  49178  fldivexpfllog2  49223  nnlog2ge0lt1  49224  logbpw2m1  49225  fllog2  49226  blennnelnn  49234  blenpw2  49236  nnpw2blenfzo  49239  blennnt2  49247  nnolog2flm1  49248  dig2nn0ld  49262  dig2nn1st  49263  0dig2pr01  49268  0dig2nn0o  49271  ackval42  49354  itsclc0xyqsolr  49427