Theorem 2z 12675

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

Syntax hints:   ∈ wcel 2108  2c2 12348  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-2 12356  df-z 12640

This theorem is referenced by:  nn0lt2  12706  nn0le2is012  12707  zadd2cl  12755  eluz4eluz2  12950  uzuzle23  12954  2eluzge1  12959  eluz2b1  12984  nn01to3  13006  nn0ge2m1nnALT  13007  ige2m1fz  13674  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  fzctr  13697  fzo0to2pr  13801  fzo0to42pr  13803  2tnp1ge0ge0  13880  flhalf  13881  m1modge3gt1  13969  2txmodxeq0  13982  f13idfv  14051  sqrecd  14200  znsqcld  14212  sq1  14244  expnass  14257  sqoddm1div8  14292  bcn2m1  14373  bcn2p1  14374  4bc2eq6  14378  hashtpg  14534  ccat2s1p2  14678  pfxtrcfv0  14742  pfxtrcfvl  14745  eqwrds3  15010  iseraltlem2  15731  iseraltlem3  15732  climcndslem1  15897  climcnds  15899  bpolydiflem  16102  efgt0  16151  tanval3  16182  cos01bnd  16234  cos01gt0  16239  odd2np1  16389  even2n  16390  oddm1even  16391  oddp1even  16392  oexpneg  16393  mod2eq1n2dvds  16395  2tp1odd  16400  2teven  16403  evend2  16405  oddp1d2  16406  ltoddhalfle  16409  opoe  16411  omoe  16412  opeo  16413  omeo  16414  z0even  16415  z2even  16418  z4even  16420  4dvdseven  16421  m1expo  16423  m1exp1  16424  nn0o  16431  sumeven  16435  flodddiv4  16461  bits0e  16475  bits0o  16476  bitsp1e  16478  bitsp1o  16479  bitsfzo  16481  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  bitsinv1  16488  6gcd4e2  16585  3lcm2e6woprm  16662  lcmf2a3a4e12  16694  isprm3  16730  dvdsnprmd  16737  2prm  16739  2mulprm  16740  oddprmge3  16747  ge2nprmge4  16748  isprm7  16755  divgcdodd  16757  oddprm  16857  pythagtriplem4  16866  pythagtriplem11  16872  pythagtriplem13  16874  iserodd  16882  prmgaplem3  17100  prmgaplem7  17104  dec2dvds  17110  prmlem0  17153  4001lem1  17188  psgnunilem4  19539  efgredleme  19785  lt6abl  19937  ablsimpgfindlem1  20151  ablsimpgfindlem2  20152  zringndrg  21502  znidomb  21603  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  minveclem2  25479  minveclem3  25482  pjthlem1  25490  dyaddisjlem  25649  mbfi1fseqlem5  25774  dvrecg  26031  dvexp3  26036  aaliou3lem6  26408  tanregt0  26599  efif1olem4  26605  tanarg  26679  cxpsqrtth  26790  2irrexpq  26791  2logb9irr  26856  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  cubic2  26909  asinlem3  26932  atantayl2  26999  cxp2limlem  27037  lgamgulmlem3  27092  lgamgulmlem4  27093  basellem2  27143  basellem3  27144  basellem4  27145  basellem5  27146  basellem8  27149  basellem9  27150  ppisval  27165  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  chtdif  27219  ppidif  27224  ppi1  27225  cht1  27226  cht3  27234  ppieq0  27237  ppiublem1  27264  chpeq0  27270  chtub  27274  chpval2  27280  chpub  27282  mersenne  27289  perfect1  27290  perfectlem1  27291  perfectlem2  27292  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgslem1  27359  lgsdir2lem2  27388  lgsdir2  27392  lgsqr  27413  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  gausslemma2dlem5a  27432  gausslemma2dlem5  27433  gausslemma2dlem6  27434  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem1  27446  lgsquad2lem2  27447  lgsquad2  27448  lgsquad3  27449  m1lgs  27450  2lgslem1a1  27451  2lgslem1a2  27452  2lgslem1b  27454  2lgslem3b1  27463  2lgslem3c1  27464  2lgs2  27467  2lgs  27469  2lgsoddprmlem2  27471  2lgsoddprmlem3  27476  2lgsoddprm  27478  2sqblem  27493  2sqmod  27498  chebbnd1lem1  27531  chebbnd1lem3  27533  chebbnd1  27534  dchrisum0lem1a  27548  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0lem3  27581  mulog2sumlem2  27597  pntlemd  27656  pntlema  27658  pntlemb  27659  pntlemh  27661  pntlemr  27664  pntlemf  27667  pntlemo  27669  istrkg2ld  28486  istrkg3ld  28487  axlowdimlem3  28977  axlowdimlem6  28980  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  usgrexmpldifpr  29293  usgrexmplef  29294  cusgrsizeindb1  29486  pthdlem1  29802  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwwisshclwwslem  30046  eupth2lem3lem3  30262  konigsberglem5  30288  2clwwlk2  30380  numclwwlk2lem1  30408  numclwlk2lem2f  30409  frgrreggt1  30425  ex-fl  30479  ex-mod  30481  ex-hash  30485  ex-dvds  30488  ex-ind-dvds  30493  minvecolem3  30908  pjhthlem1  31423  wrdt2ind  32920  archirngz  33169  archiabllem2c  33175  evl1deg2  33567  rtelextdg2  33718  2sqr3minply  33738  lmat22det  33768  dya2ub  34235  dya2icoseg  34242  oddpwdc  34319  eulerpartlemd  34331  eulerpartlemt  34336  ballotlem2  34453  signslema  34539  prodfzo03  34580  hgt750leme  34635  tgoldbachgtde  34637  nn0prpwlem  36288  knoppndvlem2  36479  knoppndvlem8  36485  irrdifflemf  37291  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  logblebd  41932  lcm2un  41971  lcm3un  41972  lcmineqlem18  42003  lcmineqlem19  42004  lcmineqlem21  42006  lcmineqlem22  42007  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  aks4d1p1p3  42026  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p3  42035  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  5bc2eq10  42099  2np3bcnp1  42101  2ap1caineq  42102  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7lem2  42138  flt4lem2  42602  flt4lem5  42605  flt4lem7  42614  nna4b4nsq  42615  acongrep  42937  acongeq  42940  jm2.18  42945  jm2.22  42952  jm2.23  42953  jm2.20nn  42954  jm2.26a  42957  jm2.26  42959  jm2.15nn0  42960  jm2.27a  42962  jm2.27c  42964  rmydioph  42971  jm3.1lem1  42974  jm3.1lem3  42976  expdiophlem1  42978  expdiophlem2  42979  hashnzfz2  44290  sumnnodd  45551  coskpi2  45787  cosknegpi  45790  dvdivbd  45844  stoweidlem26  45947  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem15  46009  dirkertrigeqlem1  46019  dirkercncflem2  46025  fourierdlem54  46081  fourierdlem56  46083  fourierdlem57  46084  fourierdlem102  46129  fourierdlem114  46141  fourierswlem  46151  fouriersw  46152  smfmullem4  46715  fmtnorec1  47411  goldbachthlem2  47420  odz2prm2pw  47437  fmtnoprmfac1  47439  fmtnoprmfac2lem1  47440  fmtnoprmfac2  47441  fmtno4prmfac  47446  31prm  47471  sfprmdvdsmersenne  47477  lighneallem1  47479  lighneallem4a  47482  lighneallem4b  47483  lighneallem4  47484  proththdlem  47487  proththd  47488  3exp4mod41  47490  41prothprmlem2  47492  m1expevenALTV  47521  dfeven2  47523  m2even  47528  gcd2odd1  47542  oexpnegALTV  47551  oexpnegnz  47552  2evenALTV  47566  2noddALTV  47567  nn0o1gt2ALTV  47568  nnpw2evenALTV  47576  perfectALTVlem1  47595  perfectALTVlem2  47596  fppr2odd  47605  341fppr2  47608  9fppr8  47611  nfermltl2rev  47617  sbgoldbalt  47655  mogoldbb  47659  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  2even  47962  zlmodzxzequa  48225  zlmodzxznm  48226  zlmodzxzequap  48228  zlmodzxzldeplem1  48229  zlmodzxzldeplem3  48231  zlmodzxzldep  48233  ldepsnlinclem1  48234  ldepsnlinc  48237  pw2m1lepw2m1  48249  fldivexpfllog2  48299  nnlog2ge0lt1  48300  logbpw2m1  48301  fllog2  48302  blennnelnn  48310  blenpw2  48312  nnpw2blenfzo  48315  blennnt2  48323  nnolog2flm1  48324  dig2nn0ld  48338  dig2nn1st  48339  0dig2pr01  48344  0dig2nn0o  48347  ackval42  48430  itsclc0xyqsolr  48503