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

Syntax hints:   ∈ wcel 2143  2c2 12296  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-neg 11445  df-nn 12235  df-2 12304  df-z 12593

This theorem is referenced by:  nn0lt2  12660  nn0le2is012  12661  zadd2cl  12709  2eluzge1  12907  uzuzle23  12909  uzuzle24  12910  eluz2b1  12944  nn01to3  12966  nn0ge2m1nnALT  12967  ige2m1fz  13647  fz0to3un2pr  13659  fz0to4untppr  13660  fz0to5un2tp  13661  fzctr  13670  fzo0to2pr  13781  fzo0to42pr  13784  2tnp1ge0ge0  13864  flhalf  13865  m1modge3gt1  13956  2txmodxeq0  13969  f13idfv  14038  sqrecd  14188  znsqcld  14200  sq1  14233  expnass  14246  sqoddm1div8  14281  bcn2m1  14362  bcn2p1  14363  4bc2eq6  14367  hashtpg  14524  ccat2s1p2  14670  pfxtrcfv0  14733  pfxtrcfvl  14736  eqwrds3  15000  iseraltlem2  15736  iseraltlem3  15737  climcndslem1  15905  climcnds  15907  bpolydiflem  16109  efgt0  16160  tanval3  16191  cos01bnd  16243  cos01gt0  16248  odd2np1  16400  even2n  16401  oddm1even  16402  oddp1even  16403  oexpneg  16404  mod2eq1n2dvds  16406  2tp1odd  16411  2teven  16414  evend2  16416  oddp1d2  16417  ltoddhalfle  16420  opoe  16422  omoe  16423  opeo  16424  omeo  16425  z0even  16426  z2even  16429  z4even  16431  4dvdseven  16432  m1expo  16434  m1exp1  16435  nn0o  16442  sumeven  16446  flodddiv4  16474  bits0e  16488  bits0o  16489  bitsp1e  16491  bitsp1o  16492  bitsfzo  16494  bitsmod  16495  bitscmp  16497  bitsinv1lem  16500  bitsinv1  16501  6gcd4e2  16597  3lcm2e6woprm  16674  lcmf2a3a4e12  16706  isprm3  16742  dvdsnprmd  16749  2prm  16751  2mulprm  16752  oddprmge3  16760  ge2nprmge4  16761  isprm7  16768  divgcdodd  16770  oddprm  16871  pythagtriplem4  16880  pythagtriplem11  16886  pythagtriplem13  16888  iserodd  16896  prmgaplem3  17114  prmgaplem7  17118  dec2dvds  17124  prmlem0  17166  4001lem1  17202  ex-chn1  18694  psgnunilem4  19568  efgredleme  19814  lt6abl  19966  ablsimpgfindlem1  20180  ablsimpgfindlem2  20181  zringndrg  21599  znidomb  21692  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  minveclem2  25566  minveclem3  25569  pjthlem1  25577  dyaddisjlem  25735  mbfi1fseqlem5  25859  dvrecg  26113  dvexp3  26118  aaliou3lem6  26492  tanregt0  26685  efif1olem4  26691  tanarg  26765  cxpsqrtth  26876  2irrexpq  26877  2logb9irr  26941  2logb9irrALT  26944  sqrt2cxp2logb9e3  26945  cubic2  26994  asinlem3  27017  atantayl2  27084  cxp2limlem  27121  lgamgulmlem3  27176  lgamgulmlem4  27177  basellem2  27227  basellem3  27228  basellem4  27229  basellem5  27230  basellem8  27233  basellem9  27234  ppisval  27249  ppiprm  27296  ppinprm  27297  chtprm  27298  chtnprm  27299  chtdif  27303  ppidif  27308  ppi1  27309  cht1  27310  cht3  27318  ppieq0  27321  ppiublem1  27347  chpeq0  27353  chtub  27357  chpval2  27363  chpub  27365  mersenne  27372  perfect1  27373  perfectlem1  27374  perfectlem2  27375  bposlem1  27429  bposlem2  27430  bposlem3  27431  bposlem5  27433  bposlem6  27434  lgslem1  27442  lgsdir2lem2  27471  lgsdir2  27475  lgsqr  27496  gausslemma2dlem0i  27509  gausslemma2dlem1a  27510  gausslemma2dlem5a  27515  gausslemma2dlem5  27516  gausslemma2dlem6  27517  gausslemma2dlem7  27518  gausslemma2d  27519  lgseisenlem1  27520  lgseisenlem2  27521  lgseisenlem3  27522  lgseisenlem4  27523  lgsquadlem1  27525  lgsquadlem2  27526  lgsquad2lem1  27529  lgsquad2lem2  27530  lgsquad2  27531  lgsquad3  27532  m1lgs  27533  2lgslem1a1  27534  2lgslem1a2  27535  2lgslem1b  27537  2lgslem3b1  27546  2lgslem3c1  27547  2lgs2  27550  2lgs  27552  2lgsoddprmlem2  27554  2lgsoddprmlem3  27559  2lgsoddprm  27561  2sqblem  27576  2sqmod  27581  chebbnd1lem1  27614  chebbnd1lem3  27616  chebbnd1  27617  dchrisum0lem1a  27631  dchrvmasumiflem1  27646  dchrisum0flblem1  27653  dchrisum0flblem2  27654  dchrisum0lem1b  27660  dchrisum0lem1  27661  dchrisum0lem2a  27662  dchrisum0lem2  27663  dchrisum0lem3  27664  mulog2sumlem2  27680  pntlemd  27739  pntlema  27741  pntlemb  27742  pntlemh  27744  pntlemr  27747  pntlemf  27750  pntlemo  27752  istrkg2ld  28710  istrkg3ld  28711  axlowdimlem3  29275  axlowdimlem6  29278  axlowdimlem16  29288  axlowdimlem17  29289  axlowdim  29292  usgrexmpldifpr  29589  usgrexmplef  29590  cusgrsizeindb1  29781  pthdlem1  30096  clwlkclwwlklem2a1  30324  clwlkclwwlklem2fv1  30327  clwlkclwwlklem2fv2  30328  clwlkclwwlklem2a4  30329  clwlkclwwlklem2a  30330  clwwisshclwwslem  30346  eupth2lem3lem3  30562  konigsberglem5  30588  2clwwlk2  30680  numclwwlk2lem1  30708  numclwlk2lem2f  30709  frgrreggt1  30725  ex-fl  30779  ex-mod  30781  ex-hash  30785  ex-dvds  30788  ex-ind-dvds  30793  minvecolem3  31209  pjhthlem1  31724  wrdt2ind  33254  archirngz  33490  archiabllem2c  33496  evl1deg2  33848  rtelextdg2  34098  constrext2chnlem  34121  constrresqrtcl  34148  2sqr3minply  34151  cos9thpiminplylem2  34154  cos9thpiminplylem5  34157  lmat22det  34193  dya2ub  34641  dya2icoseg  34648  oddpwdc  34725  eulerpartlemd  34737  eulerpartlemt  34742  ballotlem2  34860  signslema  34930  prodfzo03  34971  hgt750leme  35026  tgoldbachgtde  35028  nn0prpwlem  36814  knoppndvlem2  37083  knoppndvlem8  37089  irrdifflemf  37950  qdiff  37952  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  logblebd  42725  lcm2un  42762  lcm3un  42763  lcmineqlem18  42794  lcmineqlem19  42795  lcmineqlem21  42797  lcmineqlem22  42798  3lexlogpow5ineq2  42803  3lexlogpow2ineq1  42806  aks4d1p1p3  42817  aks4d1p1p4  42819  aks4d1p1p6  42821  aks4d1p1p7  42822  aks4d1p1p5  42823  aks4d1p1  42824  aks4d1p3  42826  aks4d1p6  42829  aks4d1p7d1  42830  aks4d1p7  42831  aks4d1p8  42835  aks4d1p9  42836  posbezout  42848  5bc2eq10  42890  2np3bcnp1  42892  2ap1caineq  42893  aks6d1c6lem4  42921  aks6d1c7lem1  42928  aks6d1c7lem2  42929  flt4lem2  43362  flt4lem5  43365  flt4lem7  43374  nna4b4nsq  43375  acongrep  43690  acongeq  43693  jm2.18  43698  jm2.22  43705  jm2.23  43706  jm2.20nn  43707  jm2.26a  43710  jm2.26  43712  jm2.15nn0  43713  jm2.27a  43715  jm2.27c  43717  rmydioph  43724  jm3.1lem1  43727  jm3.1lem3  43729  expdiophlem1  43731  expdiophlem2  43732  hashnzfz2  45014  sumnnodd  46329  coskpi2  46563  cosknegpi  46566  dvdivbd  46620  stoweidlem26  46723  wallispilem4  46765  wallispi2lem1  46768  wallispi2lem2  46769  wallispi2  46770  stirlinglem1  46771  stirlinglem3  46773  stirlinglem7  46777  stirlinglem8  46778  stirlinglem10  46780  stirlinglem11  46781  stirlinglem15  46785  dirkertrigeqlem1  46795  dirkercncflem2  46801  fourierdlem54  46857  fourierdlem56  46859  fourierdlem57  46860  fourierdlem102  46905  fourierdlem114  46917  fourierswlem  46927  fouriersw  46928  smfmullem4  47491  evenwodadd  47585  nnmul2  48050  ceil5half3  48066  addmodne  48070  m1modnep2mod  48078  minusmodnep2tmod  48079  modmkpkne  48087  modmknepk  48088  modm2nep1  48092  modp2nep1  48093  modm1nep2  48094  modm1nem2  48095  2timesltsq  48098  2timesltsqm1  48099  fmtnorec1  48272  goldbachthlem2  48281  odz2prm2pw  48298  fmtnoprmfac1  48300  fmtnoprmfac2lem1  48301  fmtnoprmfac2  48302  fmtno4prmfac  48307  31prm  48332  sfprmdvdsmersenne  48338  lighneallem1  48340  lighneallem4a  48343  lighneallem4b  48344  lighneallem4  48345  proththdlem  48348  proththd  48349  3exp4mod41  48351  41prothprmlem2  48353  nprmdvdsfacm1lem1  48355  nprmdvdsfacm1lem2  48356  nprmdvdsfacm1lem4  48358  ppivalnnnprmge6  48361  ppivalnn  48367  m1expevenALTV  48395  dfeven2  48397  m2even  48402  gcd2odd1  48416  oexpnegALTV  48425  oexpnegnz  48426  2evenALTV  48440  2noddALTV  48441  nn0o1gt2ALTV  48442  nnpw2evenALTV  48450  perfectALTVlem1  48469  perfectALTVlem2  48470  fppr2odd  48479  341fppr2  48482  9fppr8  48485  nfermltl2rev  48491  sbgoldbalt  48529  mogoldbb  48533  nnsum4primesodd  48544  nnsum4primesoddALTV  48545  wtgoldbnnsum4prm  48550  bgoldbnnsum3prm  48552  gpg5order  48808  gpg5nbgrvtx13starlem2  48820  gpg3nbgrvtx0ALT  48825  gpg3kgrtriexlem5  48835  gpg5gricstgr3  48838  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  gpg5edgnedg  48878  2even  48987  zlmodzxzequa  49259  zlmodzxznm  49260  zlmodzxzequap  49262  zlmodzxzldeplem1  49263  zlmodzxzldeplem3  49265  zlmodzxzldep  49267  ldepsnlinclem1  49268  ldepsnlinc  49271  pw2m1lepw2m1  49283  fldivexpfllog2  49328  nnlog2ge0lt1  49329  logbpw2m1  49330  fllog2  49331  blennnelnn  49339  blenpw2  49341  nnpw2blenfzo  49344  blennnt2  49352  nnolog2flm1  49353  dig2nn0ld  49367  dig2nn1st  49368  0dig2pr01  49373  0dig2nn0o  49376  ackval42  49459  itsclc0xyqsolr  49532