Theorem 2z 12627

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

Syntax hints:   ∈ wcel 2098  2c2 12300  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rrecex 11212  ax-cnre 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-neg 11479  df-nn 12246  df-2 12308  df-z 12592

This theorem is referenced by:  nn0lt2  12658  nn0le2is012  12659  zadd2cl  12707  eluz4eluz2  12902  uzuzle23  12906  2eluzge1  12911  eluz2b1  12936  nn01to3  12958  nn0ge2m1nnALT  12959  ige2m1fz  13626  fz0to3un2pr  13638  fz0to4untppr  13639  fzctr  13648  fzo0to2pr  13752  fzo0to42pr  13754  2tnp1ge0ge0  13830  flhalf  13831  m1modge3gt1  13919  2txmodxeq0  13932  f13idfv  14001  sqrecd  14150  znsqcld  14162  sq1  14194  expnass  14207  sqoddm1div8  14241  bcn2m1  14319  bcn2p1  14320  4bc2eq6  14324  hashtpg  14482  ccat2s1p2  14616  pfxtrcfv0  14680  pfxtrcfvl  14683  eqwrds3  14948  iseraltlem2  15665  iseraltlem3  15666  climcndslem1  15831  climcnds  15833  bpolydiflem  16034  efgt0  16083  tanval3  16114  cos01bnd  16166  cos01gt0  16171  odd2np1  16321  even2n  16322  oddm1even  16323  oddp1even  16324  oexpneg  16325  mod2eq1n2dvds  16327  2tp1odd  16332  2teven  16335  evend2  16337  oddp1d2  16338  ltoddhalfle  16341  opoe  16343  omoe  16344  opeo  16345  omeo  16346  z0even  16347  z2even  16350  z4even  16352  4dvdseven  16353  m1expo  16355  m1exp1  16356  nn0o  16363  sumeven  16367  flodddiv4  16393  bits0e  16407  bits0o  16408  bitsp1e  16410  bitsp1o  16411  bitsfzo  16413  bitsmod  16414  bitscmp  16416  bitsinv1lem  16419  bitsinv1  16420  6gcd4e2  16517  3lcm2e6woprm  16589  lcmf2a3a4e12  16621  isprm3  16657  dvdsnprmd  16664  2prm  16666  2mulprm  16667  oddprmge3  16674  ge2nprmge4  16675  isprm7  16682  divgcdodd  16684  oddprm  16782  pythagtriplem4  16791  pythagtriplem11  16797  pythagtriplem13  16799  iserodd  16807  prmgaplem3  17025  prmgaplem7  17029  dec2dvds  17035  prmlem0  17078  4001lem1  17113  psgnunilem4  19464  efgredleme  19710  lt6abl  19862  ablsimpgfindlem1  20076  ablsimpgfindlem2  20077  zringndrg  21411  znidomb  21512  chfacfscmulfsupp  22805  chfacfpmmulfsupp  22809  minveclem2  25398  minveclem3  25401  pjthlem1  25409  dyaddisjlem  25568  mbfi1fseqlem5  25693  dvrecg  25949  dvexp3  25954  aaliou3lem6  26328  tanregt0  26518  efif1olem4  26524  tanarg  26598  cxpsqrtth  26709  2irrexpq  26710  2logb9irr  26772  2logb9irrALT  26775  sqrt2cxp2logb9e3  26776  cubic2  26825  asinlem3  26848  atantayl2  26915  cxp2limlem  26953  lgamgulmlem3  27008  lgamgulmlem4  27009  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  basellem8  27065  basellem9  27066  ppisval  27081  ppiprm  27128  ppinprm  27129  chtprm  27130  chtnprm  27131  chtdif  27135  ppidif  27140  ppi1  27141  cht1  27142  cht3  27150  ppieq0  27153  ppiublem1  27180  chpeq0  27186  chtub  27190  chpval2  27196  chpub  27198  mersenne  27205  perfect1  27206  perfectlem1  27207  perfectlem2  27208  bposlem1  27262  bposlem2  27263  bposlem3  27264  bposlem5  27266  bposlem6  27267  lgslem1  27275  lgsdir2lem2  27304  lgsdir2  27308  lgsqr  27329  gausslemma2dlem0i  27342  gausslemma2dlem1a  27343  gausslemma2dlem5a  27348  gausslemma2dlem5  27349  gausslemma2dlem6  27350  gausslemma2dlem7  27351  gausslemma2d  27352  lgseisenlem1  27353  lgseisenlem2  27354  lgseisenlem3  27355  lgseisenlem4  27356  lgsquadlem1  27358  lgsquadlem2  27359  lgsquad2lem1  27362  lgsquad2lem2  27363  lgsquad2  27364  lgsquad3  27365  m1lgs  27366  2lgslem1a1  27367  2lgslem1a2  27368  2lgslem1b  27370  2lgslem3b1  27379  2lgslem3c1  27380  2lgs2  27383  2lgs  27385  2lgsoddprmlem2  27387  2lgsoddprmlem3  27392  2lgsoddprm  27394  2sqblem  27409  2sqmod  27414  chebbnd1lem1  27447  chebbnd1lem3  27449  chebbnd1  27450  dchrisum0lem1a  27464  dchrvmasumiflem1  27479  dchrisum0flblem1  27486  dchrisum0flblem2  27487  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2a  27495  dchrisum0lem2  27496  dchrisum0lem3  27497  mulog2sumlem2  27513  pntlemd  27572  pntlema  27574  pntlemb  27575  pntlemh  27577  pntlemr  27580  pntlemf  27583  pntlemo  27585  istrkg2ld  28336  istrkg3ld  28337  axlowdimlem3  28827  axlowdimlem6  28830  axlowdimlem16  28840  axlowdimlem17  28841  axlowdim  28844  usgrexmpldifpr  29143  usgrexmplef  29144  cusgrsizeindb1  29336  pthdlem1  29652  clwlkclwwlklem2a1  29874  clwlkclwwlklem2fv1  29877  clwlkclwwlklem2fv2  29878  clwlkclwwlklem2a4  29879  clwlkclwwlklem2a  29880  clwwisshclwwslem  29896  eupth2lem3lem3  30112  konigsberglem5  30138  2clwwlk2  30230  numclwwlk2lem1  30258  numclwlk2lem2f  30259  frgrreggt1  30275  ex-fl  30329  ex-mod  30331  ex-hash  30335  ex-dvds  30338  ex-ind-dvds  30343  minvecolem3  30758  pjhthlem1  31273  wrdt2ind  32763  archirngz  32989  archiabllem2c  32995  lmat22det  33551  dya2ub  34018  dya2icoseg  34025  oddpwdc  34102  eulerpartlemd  34114  eulerpartlemt  34119  ballotlem2  34236  signslema  34322  prodfzo03  34363  hgt750leme  34418  tgoldbachgtde  34420  nn0prpwlem  35934  knoppndvlem2  36116  knoppndvlem8  36122  irrdifflemf  36932  poimirlem25  37246  poimirlem26  37247  poimirlem27  37248  poimirlem28  37249  logblebd  41575  lcm2un  41614  lcm3un  41615  lcmineqlem18  41646  lcmineqlem19  41647  lcmineqlem21  41649  lcmineqlem22  41650  3lexlogpow5ineq2  41655  3lexlogpow2ineq1  41658  aks4d1p1p3  41669  aks4d1p1p4  41671  aks4d1p1p6  41673  aks4d1p1p7  41674  aks4d1p1p5  41675  aks4d1p1  41676  aks4d1p3  41678  aks4d1p6  41681  aks4d1p7d1  41682  aks4d1p7  41683  aks4d1p8  41687  aks4d1p9  41688  posbezout  41700  5bc2eq10  41742  2np3bcnp1  41744  2ap1caineq  41745  aks6d1c6lem4  41773  aks6d1c7lem1  41780  aks6d1c7lem2  41781  flt4lem2  42203  flt4lem5  42206  flt4lem7  42215  nna4b4nsq  42216  acongrep  42540  acongeq  42543  jm2.18  42548  jm2.22  42555  jm2.23  42556  jm2.20nn  42557  jm2.26a  42560  jm2.26  42562  jm2.15nn0  42563  jm2.27a  42565  jm2.27c  42567  rmydioph  42574  jm3.1lem1  42577  jm3.1lem3  42579  expdiophlem1  42581  expdiophlem2  42582  hashnzfz2  43897  sumnnodd  45153  coskpi2  45389  cosknegpi  45392  dvdivbd  45446  stoweidlem26  45549  wallispilem4  45591  wallispi2lem1  45594  wallispi2lem2  45595  wallispi2  45596  stirlinglem1  45597  stirlinglem3  45599  stirlinglem7  45603  stirlinglem8  45604  stirlinglem10  45606  stirlinglem11  45607  stirlinglem15  45611  dirkertrigeqlem1  45621  dirkercncflem2  45627  fourierdlem54  45683  fourierdlem56  45685  fourierdlem57  45686  fourierdlem102  45731  fourierdlem114  45743  fourierswlem  45753  fouriersw  45754  smfmullem4  46317  fmtnorec1  47011  goldbachthlem2  47020  odz2prm2pw  47037  fmtnoprmfac1  47039  fmtnoprmfac2lem1  47040  fmtnoprmfac2  47041  fmtno4prmfac  47046  31prm  47071  sfprmdvdsmersenne  47077  lighneallem1  47079  lighneallem4a  47082  lighneallem4b  47083  lighneallem4  47084  proththdlem  47087  proththd  47088  3exp4mod41  47090  41prothprmlem2  47092  m1expevenALTV  47121  dfeven2  47123  m2even  47128  gcd2odd1  47142  oexpnegALTV  47151  oexpnegnz  47152  2evenALTV  47166  2noddALTV  47167  nn0o1gt2ALTV  47168  nnpw2evenALTV  47176  perfectALTVlem1  47195  perfectALTVlem2  47196  fppr2odd  47205  341fppr2  47208  9fppr8  47211  nfermltl2rev  47217  sbgoldbalt  47255  mogoldbb  47259  nnsum4primesodd  47270  nnsum4primesoddALTV  47271  wtgoldbnnsum4prm  47276  bgoldbnnsum3prm  47278  2even  47484  zlmodzxzequa  47747  zlmodzxznm  47748  zlmodzxzequap  47750  zlmodzxzldeplem1  47751  zlmodzxzldeplem3  47753  zlmodzxzldep  47755  ldepsnlinclem1  47756  ldepsnlinc  47759  pw2m1lepw2m1  47771  fldivexpfllog2  47821  nnlog2ge0lt1  47822  logbpw2m1  47823  fllog2  47824  blennnelnn  47832  blenpw2  47834  nnpw2blenfzo  47837  blennnt2  47845  nnolog2flm1  47846  dig2nn0ld  47860  dig2nn1st  47861  0dig2pr01  47866  0dig2nn0o  47869  ackval42  47952  itsclc0xyqsolr  48025