Theorem 2z 12572

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

Syntax hints:   ∈ wcel 2109  2c2 12248  ℤcz 12536

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-2 12256  df-z 12537

This theorem is referenced by:  nn0lt2  12604  nn0le2is012  12605  zadd2cl  12653  2eluzge1  12848  uzuzle23  12850  uzuzle24  12851  eluz2b1  12885  nn01to3  12907  nn0ge2m1nnALT  12908  ige2m1fz  13585  fz0to3un2pr  13597  fz0to4untppr  13598  fz0to5un2tp  13599  fzctr  13608  fzo0to2pr  13718  fzo0to42pr  13721  2tnp1ge0ge0  13798  flhalf  13799  m1modge3gt1  13890  2txmodxeq0  13903  f13idfv  13972  sqrecd  14122  znsqcld  14134  sq1  14167  expnass  14180  sqoddm1div8  14215  bcn2m1  14296  bcn2p1  14297  4bc2eq6  14301  hashtpg  14457  ccat2s1p2  14602  pfxtrcfv0  14666  pfxtrcfvl  14669  eqwrds3  14934  iseraltlem2  15656  iseraltlem3  15657  climcndslem1  15822  climcnds  15824  bpolydiflem  16027  efgt0  16078  tanval3  16109  cos01bnd  16161  cos01gt0  16166  odd2np1  16318  even2n  16319  oddm1even  16320  oddp1even  16321  oexpneg  16322  mod2eq1n2dvds  16324  2tp1odd  16329  2teven  16332  evend2  16334  oddp1d2  16335  ltoddhalfle  16338  opoe  16340  omoe  16341  opeo  16342  omeo  16343  z0even  16344  z2even  16347  z4even  16349  4dvdseven  16350  m1expo  16352  m1exp1  16353  nn0o  16360  sumeven  16364  flodddiv4  16392  bits0e  16406  bits0o  16407  bitsp1e  16409  bitsp1o  16410  bitsfzo  16412  bitsmod  16413  bitscmp  16415  bitsinv1lem  16418  bitsinv1  16419  6gcd4e2  16515  3lcm2e6woprm  16592  lcmf2a3a4e12  16624  isprm3  16660  dvdsnprmd  16667  2prm  16669  2mulprm  16670  oddprmge3  16677  ge2nprmge4  16678  isprm7  16685  divgcdodd  16687  oddprm  16788  pythagtriplem4  16797  pythagtriplem11  16803  pythagtriplem13  16805  iserodd  16813  prmgaplem3  17031  prmgaplem7  17035  dec2dvds  17041  prmlem0  17083  4001lem1  17118  psgnunilem4  19434  efgredleme  19680  lt6abl  19832  ablsimpgfindlem1  20046  ablsimpgfindlem2  20047  zringndrg  21385  znidomb  21478  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  minveclem2  25333  minveclem3  25336  pjthlem1  25344  dyaddisjlem  25503  mbfi1fseqlem5  25627  dvrecg  25884  dvexp3  25889  aaliou3lem6  26263  tanregt0  26455  efif1olem4  26461  tanarg  26535  cxpsqrtth  26646  2irrexpq  26647  2logb9irr  26712  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  cubic2  26765  asinlem3  26788  atantayl2  26855  cxp2limlem  26893  lgamgulmlem3  26948  lgamgulmlem4  26949  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  basellem8  27005  basellem9  27006  ppisval  27021  ppiprm  27068  ppinprm  27069  chtprm  27070  chtnprm  27071  chtdif  27075  ppidif  27080  ppi1  27081  cht1  27082  cht3  27090  ppieq0  27093  ppiublem1  27120  chpeq0  27126  chtub  27130  chpval2  27136  chpub  27138  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgslem1  27215  lgsdir2lem2  27244  lgsdir2  27248  lgsqr  27269  gausslemma2dlem0i  27282  gausslemma2dlem1a  27283  gausslemma2dlem5a  27288  gausslemma2dlem5  27289  gausslemma2dlem6  27290  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem1  27302  lgsquad2lem2  27303  lgsquad2  27304  lgsquad3  27305  m1lgs  27306  2lgslem1a1  27307  2lgslem1a2  27308  2lgslem1b  27310  2lgslem3b1  27319  2lgslem3c1  27320  2lgs2  27323  2lgs  27325  2lgsoddprmlem2  27327  2lgsoddprmlem3  27332  2lgsoddprm  27334  2sqblem  27349  2sqmod  27354  chebbnd1lem1  27387  chebbnd1lem3  27389  chebbnd1  27390  dchrisum0lem1a  27404  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  mulog2sumlem2  27453  pntlemd  27512  pntlema  27514  pntlemb  27515  pntlemh  27517  pntlemr  27520  pntlemf  27523  pntlemo  27525  istrkg2ld  28394  istrkg3ld  28395  axlowdimlem3  28878  axlowdimlem6  28881  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  usgrexmpldifpr  29192  usgrexmplef  29193  cusgrsizeindb1  29385  pthdlem1  29703  clwlkclwwlklem2a1  29928  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwwisshclwwslem  29950  eupth2lem3lem3  30166  konigsberglem5  30192  2clwwlk2  30284  numclwwlk2lem1  30312  numclwlk2lem2f  30313  frgrreggt1  30329  ex-fl  30383  ex-mod  30385  ex-hash  30389  ex-dvds  30392  ex-ind-dvds  30397  minvecolem3  30812  pjhthlem1  31327  wrdt2ind  32882  archirngz  33150  archiabllem2c  33156  evl1deg2  33553  rtelextdg2  33724  constrext2chnlem  33747  constrresqrtcl  33774  2sqr3minply  33777  cos9thpiminplylem2  33780  cos9thpiminplylem5  33783  lmat22det  33819  dya2ub  34268  dya2icoseg  34275  oddpwdc  34352  eulerpartlemd  34364  eulerpartlemt  34369  ballotlem2  34487  signslema  34560  prodfzo03  34601  hgt750leme  34656  tgoldbachgtde  34658  nn0prpwlem  36317  knoppndvlem2  36508  knoppndvlem8  36514  irrdifflemf  37320  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  logblebd  41971  lcm2un  42009  lcm3un  42010  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem21  42044  lcmineqlem22  42045  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  aks4d1p1p3  42064  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  5bc2eq10  42137  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c6lem4  42168  aks6d1c7lem1  42175  aks6d1c7lem2  42176  flt4lem2  42642  flt4lem5  42645  flt4lem7  42654  nna4b4nsq  42655  acongrep  42976  acongeq  42979  jm2.18  42984  jm2.22  42991  jm2.23  42992  jm2.20nn  42993  jm2.26a  42996  jm2.26  42998  jm2.15nn0  42999  jm2.27a  43001  jm2.27c  43003  rmydioph  43010  jm3.1lem1  43013  jm3.1lem3  43015  expdiophlem1  43017  expdiophlem2  43018  hashnzfz2  44317  sumnnodd  45635  coskpi2  45871  cosknegpi  45874  dvdivbd  45928  stoweidlem26  46031  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem15  46093  dirkertrigeqlem1  46103  dirkercncflem2  46109  fourierdlem54  46165  fourierdlem56  46167  fourierdlem57  46168  fourierdlem102  46213  fourierdlem114  46225  fourierswlem  46235  fouriersw  46236  smfmullem4  46799  evenwodadd  46893  ceil5half3  47345  addmodne  47349  m1modnep2mod  47357  minusmodnep2tmod  47358  modmkpkne  47366  modmknepk  47367  modm2nep1  47371  modp2nep1  47372  modm1nep2  47373  modm1nem2  47374  fmtnorec1  47542  goldbachthlem2  47551  odz2prm2pw  47568  fmtnoprmfac1  47570  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  fmtno4prmfac  47577  31prm  47602  sfprmdvdsmersenne  47608  lighneallem1  47610  lighneallem4a  47613  lighneallem4b  47614  lighneallem4  47615  proththdlem  47618  proththd  47619  3exp4mod41  47621  41prothprmlem2  47623  m1expevenALTV  47652  dfeven2  47654  m2even  47659  gcd2odd1  47673  oexpnegALTV  47682  oexpnegnz  47683  2evenALTV  47697  2noddALTV  47698  nn0o1gt2ALTV  47699  nnpw2evenALTV  47707  perfectALTVlem1  47726  perfectALTVlem2  47727  fppr2odd  47736  341fppr2  47739  9fppr8  47742  nfermltl2rev  47748  sbgoldbalt  47786  mogoldbb  47790  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  gpg5order  48055  gpg5nbgrvtx13starlem2  48067  gpg3nbgrvtx0ALT  48072  gpg3kgrtriexlem5  48082  gpg5gricstgr3  48085  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  2even  48231  zlmodzxzequa  48489  zlmodzxznm  48490  zlmodzxzequap  48492  zlmodzxzldeplem1  48493  zlmodzxzldeplem3  48495  zlmodzxzldep  48497  ldepsnlinclem1  48498  ldepsnlinc  48501  pw2m1lepw2m1  48513  fldivexpfllog2  48558  nnlog2ge0lt1  48559  logbpw2m1  48560  fllog2  48561  blennnelnn  48569  blenpw2  48571  nnpw2blenfzo  48574  blennnt2  48582  nnolog2flm1  48583  dig2nn0ld  48597  dig2nn1st  48598  0dig2pr01  48603  0dig2nn0o  48606  ackval42  48689  itsclc0xyqsolr  48762