Theorem 2z 12541

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

Syntax hints:   ∈ wcel 2109  2c2 12217  ℤcz 12505

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-neg 11384  df-nn 12163  df-2 12225  df-z 12506

This theorem is referenced by:  nn0lt2  12573  nn0le2is012  12574  zadd2cl  12622  2eluzge1  12817  uzuzle23  12819  uzuzle24  12820  eluz2b1  12854  nn01to3  12876  nn0ge2m1nnALT  12877  ige2m1fz  13554  fz0to3un2pr  13566  fz0to4untppr  13567  fz0to5un2tp  13568  fzctr  13577  fzo0to2pr  13687  fzo0to42pr  13690  2tnp1ge0ge0  13767  flhalf  13768  m1modge3gt1  13859  2txmodxeq0  13872  f13idfv  13941  sqrecd  14091  znsqcld  14103  sq1  14136  expnass  14149  sqoddm1div8  14184  bcn2m1  14265  bcn2p1  14266  4bc2eq6  14270  hashtpg  14426  ccat2s1p2  14571  pfxtrcfv0  14635  pfxtrcfvl  14638  eqwrds3  14903  iseraltlem2  15625  iseraltlem3  15626  climcndslem1  15791  climcnds  15793  bpolydiflem  15996  efgt0  16047  tanval3  16078  cos01bnd  16130  cos01gt0  16135  odd2np1  16287  even2n  16288  oddm1even  16289  oddp1even  16290  oexpneg  16291  mod2eq1n2dvds  16293  2tp1odd  16298  2teven  16301  evend2  16303  oddp1d2  16304  ltoddhalfle  16307  opoe  16309  omoe  16310  opeo  16311  omeo  16312  z0even  16313  z2even  16316  z4even  16318  4dvdseven  16319  m1expo  16321  m1exp1  16322  nn0o  16329  sumeven  16333  flodddiv4  16361  bits0e  16375  bits0o  16376  bitsp1e  16378  bitsp1o  16379  bitsfzo  16381  bitsmod  16382  bitscmp  16384  bitsinv1lem  16387  bitsinv1  16388  6gcd4e2  16484  3lcm2e6woprm  16561  lcmf2a3a4e12  16593  isprm3  16629  dvdsnprmd  16636  2prm  16638  2mulprm  16639  oddprmge3  16646  ge2nprmge4  16647  isprm7  16654  divgcdodd  16656  oddprm  16757  pythagtriplem4  16766  pythagtriplem11  16772  pythagtriplem13  16774  iserodd  16782  prmgaplem3  17000  prmgaplem7  17004  dec2dvds  17010  prmlem0  17052  4001lem1  17087  psgnunilem4  19403  efgredleme  19649  lt6abl  19801  ablsimpgfindlem1  20015  ablsimpgfindlem2  20016  zringndrg  21354  znidomb  21447  chfacfscmulfsupp  22722  chfacfpmmulfsupp  22726  minveclem2  25302  minveclem3  25305  pjthlem1  25313  dyaddisjlem  25472  mbfi1fseqlem5  25596  dvrecg  25853  dvexp3  25858  aaliou3lem6  26232  tanregt0  26424  efif1olem4  26430  tanarg  26504  cxpsqrtth  26615  2irrexpq  26616  2logb9irr  26681  2logb9irrALT  26684  sqrt2cxp2logb9e3  26685  cubic2  26734  asinlem3  26757  atantayl2  26824  cxp2limlem  26862  lgamgulmlem3  26917  lgamgulmlem4  26918  basellem2  26968  basellem3  26969  basellem4  26970  basellem5  26971  basellem8  26974  basellem9  26975  ppisval  26990  ppiprm  27037  ppinprm  27038  chtprm  27039  chtnprm  27040  chtdif  27044  ppidif  27049  ppi1  27050  cht1  27051  cht3  27059  ppieq0  27062  ppiublem1  27089  chpeq0  27095  chtub  27099  chpval2  27105  chpub  27107  mersenne  27114  perfect1  27115  perfectlem1  27116  perfectlem2  27117  bposlem1  27171  bposlem2  27172  bposlem3  27173  bposlem5  27175  bposlem6  27176  lgslem1  27184  lgsdir2lem2  27213  lgsdir2  27217  lgsqr  27238  gausslemma2dlem0i  27251  gausslemma2dlem1a  27252  gausslemma2dlem5a  27257  gausslemma2dlem5  27258  gausslemma2dlem6  27259  gausslemma2dlem7  27260  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  lgsquadlem2  27268  lgsquad2lem1  27271  lgsquad2lem2  27272  lgsquad2  27273  lgsquad3  27274  m1lgs  27275  2lgslem1a1  27276  2lgslem1a2  27277  2lgslem1b  27279  2lgslem3b1  27288  2lgslem3c1  27289  2lgs2  27292  2lgs  27294  2lgsoddprmlem2  27296  2lgsoddprmlem3  27301  2lgsoddprm  27303  2sqblem  27318  2sqmod  27323  chebbnd1lem1  27356  chebbnd1lem3  27358  chebbnd1  27359  dchrisum0lem1a  27373  dchrvmasumiflem1  27388  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  dchrisum0lem3  27406  mulog2sumlem2  27422  pntlemd  27481  pntlema  27483  pntlemb  27484  pntlemh  27486  pntlemr  27489  pntlemf  27492  pntlemo  27494  istrkg2ld  28363  istrkg3ld  28364  axlowdimlem3  28847  axlowdimlem6  28850  axlowdimlem16  28860  axlowdimlem17  28861  axlowdim  28864  usgrexmpldifpr  29161  usgrexmplef  29162  cusgrsizeindb1  29354  pthdlem1  29669  clwlkclwwlklem2a1  29894  clwlkclwwlklem2fv1  29897  clwlkclwwlklem2fv2  29898  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwwisshclwwslem  29916  eupth2lem3lem3  30132  konigsberglem5  30158  2clwwlk2  30250  numclwwlk2lem1  30278  numclwlk2lem2f  30279  frgrreggt1  30295  ex-fl  30349  ex-mod  30351  ex-hash  30355  ex-dvds  30358  ex-ind-dvds  30363  minvecolem3  30778  pjhthlem1  31293  wrdt2ind  32848  archirngz  33116  archiabllem2c  33122  evl1deg2  33519  rtelextdg2  33690  constrext2chnlem  33713  constrresqrtcl  33740  2sqr3minply  33743  cos9thpiminplylem2  33746  cos9thpiminplylem5  33749  lmat22det  33785  dya2ub  34234  dya2icoseg  34241  oddpwdc  34318  eulerpartlemd  34330  eulerpartlemt  34335  ballotlem2  34453  signslema  34526  prodfzo03  34567  hgt750leme  34622  tgoldbachgtde  34624  nn0prpwlem  36283  knoppndvlem2  36474  knoppndvlem8  36480  irrdifflemf  37286  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  logblebd  41937  lcm2un  41975  lcm3un  41976  lcmineqlem18  42007  lcmineqlem19  42008  lcmineqlem21  42010  lcmineqlem22  42011  3lexlogpow5ineq2  42016  3lexlogpow2ineq1  42019  aks4d1p1p3  42030  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p3  42039  aks4d1p6  42042  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  5bc2eq10  42103  2np3bcnp1  42105  2ap1caineq  42106  aks6d1c6lem4  42134  aks6d1c7lem1  42141  aks6d1c7lem2  42142  flt4lem2  42608  flt4lem5  42611  flt4lem7  42620  nna4b4nsq  42621  acongrep  42942  acongeq  42945  jm2.18  42950  jm2.22  42957  jm2.23  42958  jm2.20nn  42959  jm2.26a  42962  jm2.26  42964  jm2.15nn0  42965  jm2.27a  42967  jm2.27c  42969  rmydioph  42976  jm3.1lem1  42979  jm3.1lem3  42981  expdiophlem1  42983  expdiophlem2  42984  hashnzfz2  44283  sumnnodd  45601  coskpi2  45837  cosknegpi  45840  dvdivbd  45894  stoweidlem26  45997  wallispilem4  46039  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem7  46051  stirlinglem8  46052  stirlinglem10  46054  stirlinglem11  46055  stirlinglem15  46059  dirkertrigeqlem1  46069  dirkercncflem2  46075  fourierdlem54  46131  fourierdlem56  46133  fourierdlem57  46134  fourierdlem102  46179  fourierdlem114  46191  fourierswlem  46201  fouriersw  46202  smfmullem4  46765  evenwodadd  46859  ceil5half3  47314  addmodne  47318  m1modnep2mod  47326  minusmodnep2tmod  47327  modmkpkne  47335  modmknepk  47336  modm2nep1  47340  modp2nep1  47341  modm1nep2  47342  modm1nem2  47343  fmtnorec1  47511  goldbachthlem2  47520  odz2prm2pw  47537  fmtnoprmfac1  47539  fmtnoprmfac2lem1  47540  fmtnoprmfac2  47541  fmtno4prmfac  47546  31prm  47571  sfprmdvdsmersenne  47577  lighneallem1  47579  lighneallem4a  47582  lighneallem4b  47583  lighneallem4  47584  proththdlem  47587  proththd  47588  3exp4mod41  47590  41prothprmlem2  47592  m1expevenALTV  47621  dfeven2  47623  m2even  47628  gcd2odd1  47642  oexpnegALTV  47651  oexpnegnz  47652  2evenALTV  47666  2noddALTV  47667  nn0o1gt2ALTV  47668  nnpw2evenALTV  47676  perfectALTVlem1  47695  perfectALTVlem2  47696  fppr2odd  47705  341fppr2  47708  9fppr8  47711  nfermltl2rev  47717  sbgoldbalt  47755  mogoldbb  47759  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  gpg5order  48024  gpg5nbgrvtx13starlem2  48036  gpg3nbgrvtx0ALT  48041  gpg3kgrtriexlem5  48051  gpg5gricstgr3  48054  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  2even  48200  zlmodzxzequa  48458  zlmodzxznm  48459  zlmodzxzequap  48461  zlmodzxzldeplem1  48462  zlmodzxzldeplem3  48464  zlmodzxzldep  48466  ldepsnlinclem1  48467  ldepsnlinc  48470  pw2m1lepw2m1  48482  fldivexpfllog2  48527  nnlog2ge0lt1  48528  logbpw2m1  48529  fllog2  48530  blennnelnn  48538  blenpw2  48540  nnpw2blenfzo  48543  blennnt2  48551  nnolog2flm1  48552  dig2nn0ld  48566  dig2nn1st  48567  0dig2pr01  48572  0dig2nn0o  48575  ackval42  48658  itsclc0xyqsolr  48731