Theorem 2z 12596

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

Syntax hints:   ∈ wcel 2106  2c2 12269  ℤcz 12560

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-neg 11449  df-nn 12215  df-2 12277  df-z 12561

This theorem is referenced by:  nn0lt2  12627  nn0le2is012  12628  zadd2cl  12676  eluz4eluz2  12871  uzuzle23  12875  2eluzge1  12880  eluz2b1  12905  nn01to3  12927  nn0ge2m1nnALT  12928  ige2m1fz  13593  fz0to3un2pr  13605  fz0to4untppr  13606  fzctr  13615  fzo0to2pr  13719  fzo0to42pr  13721  2tnp1ge0ge0  13796  flhalf  13797  m1modge3gt1  13885  2txmodxeq0  13898  f13idfv  13967  sqrecd  14117  znsqcld  14129  sq1  14161  expnass  14174  sqoddm1div8  14208  bcn2m1  14286  bcn2p1  14287  4bc2eq6  14291  hashtpg  14448  ccat2s1p2  14582  pfxtrcfv0  14646  pfxtrcfvl  14649  eqwrds3  14914  iseraltlem2  15631  iseraltlem3  15632  climcndslem1  15797  climcnds  15799  bpolydiflem  16000  efgt0  16048  tanval3  16079  cos01bnd  16131  cos01gt0  16136  odd2np1  16286  even2n  16287  oddm1even  16288  oddp1even  16289  oexpneg  16290  mod2eq1n2dvds  16292  2tp1odd  16297  2teven  16300  evend2  16302  oddp1d2  16303  ltoddhalfle  16306  opoe  16308  omoe  16309  opeo  16310  omeo  16311  z0even  16312  z2even  16315  z4even  16317  4dvdseven  16318  m1expo  16320  m1exp1  16321  nn0o  16328  sumeven  16332  flodddiv4  16358  bits0e  16372  bits0o  16373  bitsp1e  16375  bitsp1o  16376  bitsfzo  16378  bitsmod  16379  bitscmp  16381  bitsinv1lem  16384  bitsinv1  16385  6gcd4e2  16482  3lcm2e6woprm  16554  lcmf2a3a4e12  16586  isprm3  16622  dvdsnprmd  16629  2prm  16631  2mulprm  16632  oddprmge3  16639  ge2nprmge4  16640  isprm7  16647  divgcdodd  16649  oddprm  16745  pythagtriplem4  16754  pythagtriplem11  16760  pythagtriplem13  16762  iserodd  16770  prmgaplem3  16988  prmgaplem7  16992  dec2dvds  16998  prmlem0  17041  4001lem1  17076  psgnunilem4  19367  efgredleme  19613  lt6abl  19765  ablsimpgfindlem1  19979  ablsimpgfindlem2  19980  zringndrg  21044  znidomb  21123  chfacfscmulfsupp  22368  chfacfpmmulfsupp  22372  minveclem2  24950  minveclem3  24953  pjthlem1  24961  dyaddisjlem  25119  mbfi1fseqlem5  25244  dvrecg  25497  dvexp3  25502  aaliou3lem6  25868  tanregt0  26055  efif1olem4  26061  tanarg  26134  cxpsqrtth  26245  2irrexpq  26246  2logb9irr  26307  2logb9irrALT  26310  sqrt2cxp2logb9e3  26311  cubic2  26360  asinlem3  26383  atantayl2  26450  cxp2limlem  26487  lgamgulmlem3  26542  lgamgulmlem4  26543  basellem2  26593  basellem3  26594  basellem4  26595  basellem5  26596  basellem8  26599  basellem9  26600  ppisval  26615  ppiprm  26662  ppinprm  26663  chtprm  26664  chtnprm  26665  chtdif  26669  ppidif  26674  ppi1  26675  cht1  26676  cht3  26684  ppieq0  26687  ppiublem1  26712  chpeq0  26718  chtub  26722  chpval2  26728  chpub  26730  mersenne  26737  perfect1  26738  perfectlem1  26739  perfectlem2  26740  bposlem1  26794  bposlem2  26795  bposlem3  26796  bposlem5  26798  bposlem6  26799  lgslem1  26807  lgsdir2lem2  26836  lgsdir2  26840  lgsqr  26861  gausslemma2dlem0i  26874  gausslemma2dlem1a  26875  gausslemma2dlem5a  26880  gausslemma2dlem5  26881  gausslemma2dlem6  26882  gausslemma2dlem7  26883  gausslemma2d  26884  lgseisenlem1  26885  lgseisenlem2  26886  lgseisenlem3  26887  lgseisenlem4  26888  lgsquadlem1  26890  lgsquadlem2  26891  lgsquad2lem1  26894  lgsquad2lem2  26895  lgsquad2  26896  lgsquad3  26897  m1lgs  26898  2lgslem1a1  26899  2lgslem1a2  26900  2lgslem1b  26902  2lgslem3b1  26911  2lgslem3c1  26912  2lgs2  26915  2lgs  26917  2lgsoddprmlem2  26919  2lgsoddprmlem3  26924  2lgsoddprm  26926  2sqblem  26941  2sqmod  26946  chebbnd1lem1  26979  chebbnd1lem3  26981  chebbnd1  26982  dchrisum0lem1a  26996  dchrvmasumiflem1  27011  dchrisum0flblem1  27018  dchrisum0flblem2  27019  dchrisum0lem1b  27025  dchrisum0lem1  27026  dchrisum0lem2a  27027  dchrisum0lem2  27028  dchrisum0lem3  27029  mulog2sumlem2  27045  pntlemd  27104  pntlema  27106  pntlemb  27107  pntlemh  27109  pntlemr  27112  pntlemf  27115  pntlemo  27117  istrkg2ld  27749  istrkg3ld  27750  axlowdimlem3  28240  axlowdimlem6  28243  axlowdimlem16  28253  axlowdimlem17  28254  axlowdim  28257  usgrexmpldifpr  28553  usgrexmplef  28554  cusgrsizeindb1  28745  pthdlem1  29061  clwlkclwwlklem2a1  29283  clwlkclwwlklem2fv1  29286  clwlkclwwlklem2fv2  29287  clwlkclwwlklem2a4  29288  clwlkclwwlklem2a  29289  clwwisshclwwslem  29305  eupth2lem3lem3  29521  konigsberglem5  29547  2clwwlk2  29639  numclwwlk2lem1  29667  numclwlk2lem2f  29668  frgrreggt1  29684  ex-fl  29738  ex-mod  29740  ex-hash  29744  ex-dvds  29747  ex-ind-dvds  29752  minvecolem3  30167  pjhthlem1  30682  wrdt2ind  32155  archirngz  32376  archiabllem2c  32382  lmat22det  32871  dya2ub  33338  dya2icoseg  33345  oddpwdc  33422  eulerpartlemd  33434  eulerpartlemt  33439  ballotlem2  33556  signslema  33642  prodfzo03  33684  hgt750leme  33739  tgoldbachgtde  33741  nn0prpwlem  35299  knoppndvlem2  35481  knoppndvlem8  35487  irrdifflemf  36298  poimirlem25  36605  poimirlem26  36606  poimirlem27  36607  poimirlem28  36608  logblebd  40933  lcm2un  40971  lcm3un  40972  lcmineqlem18  41003  lcmineqlem19  41004  lcmineqlem21  41006  lcmineqlem22  41007  3lexlogpow5ineq2  41012  3lexlogpow2ineq1  41015  aks4d1p1p3  41026  aks4d1p1p4  41028  aks4d1p1p6  41030  aks4d1p1p7  41031  aks4d1p1p5  41032  aks4d1p1  41033  aks4d1p3  41035  aks4d1p6  41038  aks4d1p7d1  41039  aks4d1p7  41040  aks4d1p8  41044  aks4d1p9  41045  5bc2eq10  41050  2np3bcnp1  41052  2ap1caineq  41053  flt4lem2  41477  flt4lem5  41480  flt4lem7  41489  nna4b4nsq  41490  acongrep  41807  acongeq  41810  jm2.18  41815  jm2.22  41822  jm2.23  41823  jm2.20nn  41824  jm2.26a  41827  jm2.26  41829  jm2.15nn0  41830  jm2.27a  41832  jm2.27c  41834  rmydioph  41841  jm3.1lem1  41844  jm3.1lem3  41846  expdiophlem1  41848  expdiophlem2  41849  hashnzfz2  43168  sumnnodd  44431  coskpi2  44667  cosknegpi  44670  dvdivbd  44724  stoweidlem26  44827  wallispilem4  44869  wallispi2lem1  44872  wallispi2lem2  44873  wallispi2  44874  stirlinglem1  44875  stirlinglem3  44877  stirlinglem7  44881  stirlinglem8  44882  stirlinglem10  44884  stirlinglem11  44885  stirlinglem15  44889  dirkertrigeqlem1  44899  dirkercncflem2  44905  fourierdlem54  44961  fourierdlem56  44963  fourierdlem57  44964  fourierdlem102  45009  fourierdlem114  45021  fourierswlem  45031  fouriersw  45032  smfmullem4  45595  fmtnorec1  46290  goldbachthlem2  46299  odz2prm2pw  46316  fmtnoprmfac1  46318  fmtnoprmfac2lem1  46319  fmtnoprmfac2  46320  fmtno4prmfac  46325  31prm  46350  sfprmdvdsmersenne  46356  lighneallem1  46358  lighneallem4a  46361  lighneallem4b  46362  lighneallem4  46363  proththdlem  46366  proththd  46367  3exp4mod41  46369  41prothprmlem2  46371  m1expevenALTV  46400  dfeven2  46402  m2even  46407  gcd2odd1  46421  oexpnegALTV  46430  oexpnegnz  46431  2evenALTV  46445  2noddALTV  46446  nn0o1gt2ALTV  46447  nnpw2evenALTV  46455  perfectALTVlem1  46474  perfectALTVlem2  46475  fppr2odd  46484  341fppr2  46487  9fppr8  46490  nfermltl2rev  46496  sbgoldbalt  46534  mogoldbb  46538  nnsum4primesodd  46549  nnsum4primesoddALTV  46550  wtgoldbnnsum4prm  46555  bgoldbnnsum3prm  46557  2even  46916  zlmodzxzequa  47261  zlmodzxznm  47262  zlmodzxzequap  47264  zlmodzxzldeplem1  47265  zlmodzxzldeplem3  47267  zlmodzxzldep  47269  ldepsnlinclem1  47270  ldepsnlinc  47273  pw2m1lepw2m1  47285  fldivexpfllog2  47335  nnlog2ge0lt1  47336  logbpw2m1  47337  fllog2  47338  blennnelnn  47346  blenpw2  47348  nnpw2blenfzo  47351  blennnt2  47359  nnolog2flm1  47360  dig2nn0ld  47374  dig2nn1st  47375  0dig2pr01  47380  0dig2nn0o  47383  ackval42  47466  itsclc0xyqsolr  47539