Theorem 2z 12398

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

Syntax hints:   ∈ wcel 2104  2c2 12074  ℤcz 12365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rrecex 10989  ax-cnre 10990

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-neg 11254  df-nn 12020  df-2 12082  df-z 12366

This theorem is referenced by:  nn0lt2  12429  nn0le2is012  12430  zadd2cl  12480  eluz4eluz2  12671  uzuzle23  12675  2eluzge1  12680  eluz2b1  12705  nn01to3  12727  nn0ge2m1nnALT  12728  ige2m1fz  13392  fz0to3un2pr  13404  fz0to4untppr  13405  fzctr  13414  fzo0to2pr  13518  fzo0to42pr  13520  2tnp1ge0ge0  13595  flhalf  13596  m1modge3gt1  13684  2txmodxeq0  13697  f13idfv  13766  sqrecd  13914  znsqcld  13926  sq1  13958  expnass  13970  sqoddm1div8  14004  bcn2m1  14084  bcn2p1  14085  4bc2eq6  14089  hashtpg  14244  ccat2s1p2  14382  ccat2s1p2OLD  14384  pfxtrcfv0  14452  pfxtrcfvl  14455  eqwrds3  14721  iseraltlem2  15439  iseraltlem3  15440  climcndslem1  15606  climcnds  15608  bpolydiflem  15809  efgt0  15857  tanval3  15888  cos01bnd  15940  cos01gt0  15945  odd2np1  16095  even2n  16096  oddm1even  16097  oddp1even  16098  oexpneg  16099  mod2eq1n2dvds  16101  2tp1odd  16106  2teven  16109  evend2  16111  oddp1d2  16112  ltoddhalfle  16115  opoe  16117  omoe  16118  opeo  16119  omeo  16120  z0even  16121  z2even  16124  z4even  16126  4dvdseven  16127  m1expo  16129  m1exp1  16130  nn0o  16137  sumeven  16141  flodddiv4  16167  bits0e  16181  bits0o  16182  bitsp1e  16184  bitsp1o  16185  bitsfzo  16187  bitsmod  16188  bitscmp  16190  bitsinv1lem  16193  bitsinv1  16194  6gcd4e2  16291  3lcm2e6woprm  16365  lcmf2a3a4e12  16397  isprm3  16433  dvdsnprmd  16440  2prm  16442  2mulprm  16443  oddprmge3  16450  ge2nprmge4  16451  isprm7  16458  divgcdodd  16460  oddprm  16556  pythagtriplem4  16565  pythagtriplem11  16571  pythagtriplem13  16573  iserodd  16581  prmgaplem3  16799  prmgaplem7  16803  dec2dvds  16809  prmlem0  16852  4001lem1  16887  psgnunilem4  19150  efgredleme  19394  lt6abl  19541  ablsimpgfindlem1  19755  ablsimpgfindlem2  19756  zringndrg  20735  znidomb  20814  chfacfscmulfsupp  22053  chfacfpmmulfsupp  22057  minveclem2  24635  minveclem3  24638  pjthlem1  24646  dyaddisjlem  24804  mbfi1fseqlem5  24929  dvrecg  25182  dvexp3  25187  aaliou3lem6  25553  tanregt0  25740  efif1olem4  25746  tanarg  25819  cxpsqrtth  25929  2irrexpq  25930  2logb9irr  25990  2logb9irrALT  25993  sqrt2cxp2logb9e3  25994  cubic2  26043  asinlem3  26066  atantayl2  26133  cxp2limlem  26170  lgamgulmlem3  26225  lgamgulmlem4  26226  basellem2  26276  basellem3  26277  basellem4  26278  basellem5  26279  basellem8  26282  basellem9  26283  ppisval  26298  ppiprm  26345  ppinprm  26346  chtprm  26347  chtnprm  26348  chtdif  26352  ppidif  26357  ppi1  26358  cht1  26359  cht3  26367  ppieq0  26370  ppiublem1  26395  chpeq0  26401  chtub  26405  chpval2  26411  chpub  26413  mersenne  26420  perfect1  26421  perfectlem1  26422  perfectlem2  26423  bposlem1  26477  bposlem2  26478  bposlem3  26479  bposlem5  26481  bposlem6  26482  lgslem1  26490  lgsdir2lem2  26519  lgsdir2  26523  lgsqr  26544  gausslemma2dlem0i  26557  gausslemma2dlem1a  26558  gausslemma2dlem5a  26563  gausslemma2dlem5  26564  gausslemma2dlem6  26565  gausslemma2dlem7  26566  gausslemma2d  26567  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgseisenlem4  26571  lgsquadlem1  26573  lgsquadlem2  26574  lgsquad2lem1  26577  lgsquad2lem2  26578  lgsquad2  26579  lgsquad3  26580  m1lgs  26581  2lgslem1a1  26582  2lgslem1a2  26583  2lgslem1b  26585  2lgslem3b1  26594  2lgslem3c1  26595  2lgs2  26598  2lgs  26600  2lgsoddprmlem2  26602  2lgsoddprmlem3  26607  2lgsoddprm  26609  2sqblem  26624  2sqmod  26629  chebbnd1lem1  26662  chebbnd1lem3  26664  chebbnd1  26665  dchrisum0lem1a  26679  dchrvmasumiflem1  26694  dchrisum0flblem1  26701  dchrisum0flblem2  26702  dchrisum0lem1b  26708  dchrisum0lem1  26709  dchrisum0lem2a  26710  dchrisum0lem2  26711  dchrisum0lem3  26712  mulog2sumlem2  26728  pntlemd  26787  pntlema  26789  pntlemb  26790  pntlemh  26792  pntlemr  26795  pntlemf  26798  pntlemo  26800  istrkg2ld  26866  istrkg3ld  26867  axlowdimlem3  27357  axlowdimlem6  27360  axlowdimlem16  27370  axlowdimlem17  27371  axlowdim  27374  usgrexmpldifpr  27670  usgrexmplef  27671  cusgrsizeindb1  27862  pthdlem1  28179  clwlkclwwlklem2a1  28401  clwlkclwwlklem2fv1  28404  clwlkclwwlklem2fv2  28405  clwlkclwwlklem2a4  28406  clwlkclwwlklem2a  28407  clwwisshclwwslem  28423  eupth2lem3lem3  28639  konigsberglem5  28665  2clwwlk2  28757  numclwwlk2lem1  28785  numclwlk2lem2f  28786  frgrreggt1  28802  ex-fl  28856  ex-mod  28858  ex-hash  28862  ex-dvds  28865  ex-ind-dvds  28870  minvecolem3  29283  pjhthlem1  29798  wrdt2ind  31270  archirngz  31488  archiabllem2c  31494  lmat22det  31817  dya2ub  32282  dya2icoseg  32289  oddpwdc  32366  eulerpartlemd  32378  eulerpartlemt  32383  ballotlem2  32500  signslema  32586  prodfzo03  32628  hgt750leme  32683  tgoldbachgtde  32685  nn0prpwlem  34556  knoppndvlem2  34738  knoppndvlem8  34744  irrdifflemf  35540  poimirlem25  35846  poimirlem26  35847  poimirlem27  35848  poimirlem28  35849  logblebd  40026  lcm2un  40064  lcm3un  40065  lcmineqlem18  40096  lcmineqlem19  40097  lcmineqlem21  40099  lcmineqlem22  40100  3lexlogpow5ineq2  40105  3lexlogpow2ineq1  40108  aks4d1p1p3  40119  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p3  40128  aks4d1p6  40131  aks4d1p7d1  40132  aks4d1p7  40133  aks4d1p8  40137  aks4d1p9  40138  5bc2eq10  40140  2np3bcnp1  40142  2ap1caineq  40143  flt4lem2  40521  flt4lem5  40524  flt4lem7  40533  nna4b4nsq  40534  acongrep  40840  acongeq  40843  jm2.18  40848  jm2.22  40855  jm2.23  40856  jm2.20nn  40857  jm2.26a  40860  jm2.26  40862  jm2.15nn0  40863  jm2.27a  40865  jm2.27c  40867  rmydioph  40874  jm3.1lem1  40877  jm3.1lem3  40879  expdiophlem1  40881  expdiophlem2  40882  hashnzfz2  41977  sumnnodd  43220  coskpi2  43456  cosknegpi  43459  dvdivbd  43513  stoweidlem26  43616  wallispilem4  43658  wallispi2lem1  43661  wallispi2lem2  43662  wallispi2  43663  stirlinglem1  43664  stirlinglem3  43666  stirlinglem7  43670  stirlinglem8  43671  stirlinglem10  43673  stirlinglem11  43674  stirlinglem15  43678  dirkertrigeqlem1  43688  dirkercncflem2  43694  fourierdlem54  43750  fourierdlem56  43752  fourierdlem57  43753  fourierdlem102  43798  fourierdlem114  43810  fourierswlem  43820  fouriersw  43821  smfmullem4  44382  fmtnorec1  45047  goldbachthlem2  45056  odz2prm2pw  45073  fmtnoprmfac1  45075  fmtnoprmfac2lem1  45076  fmtnoprmfac2  45077  fmtno4prmfac  45082  31prm  45107  sfprmdvdsmersenne  45113  lighneallem1  45115  lighneallem4a  45118  lighneallem4b  45119  lighneallem4  45120  proththdlem  45123  proththd  45124  3exp4mod41  45126  41prothprmlem2  45128  m1expevenALTV  45157  dfeven2  45159  m2even  45164  gcd2odd1  45178  oexpnegALTV  45187  oexpnegnz  45188  2evenALTV  45202  2noddALTV  45203  nn0o1gt2ALTV  45204  nnpw2evenALTV  45212  perfectALTVlem1  45231  perfectALTVlem2  45232  fppr2odd  45241  341fppr2  45244  9fppr8  45247  nfermltl2rev  45253  sbgoldbalt  45291  mogoldbb  45295  nnsum4primesodd  45306  nnsum4primesoddALTV  45307  wtgoldbnnsum4prm  45312  bgoldbnnsum3prm  45314  2even  45549  zlmodzxzequa  45895  zlmodzxznm  45896  zlmodzxzequap  45898  zlmodzxzldeplem1  45899  zlmodzxzldeplem3  45901  zlmodzxzldep  45903  ldepsnlinclem1  45904  ldepsnlinc  45907  pw2m1lepw2m1  45919  fldivexpfllog2  45969  nnlog2ge0lt1  45970  logbpw2m1  45971  fllog2  45972  blennnelnn  45980  blenpw2  45982  nnpw2blenfzo  45985  blennnt2  45993  nnolog2flm1  45994  dig2nn0ld  46008  dig2nn1st  46009  0dig2pr01  46014  0dig2nn0o  46017  ackval42  46100  itsclc0xyqsolr  46173