Theorem 2z 11671

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

Syntax hints:   ∈ wcel 2158  2c2 11352  ℤcz 11639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-er 7976  df-en 8190  df-dom 8191  df-sdom 8192  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-nn 11303  df-2 11360  df-z 11640

This theorem is referenced by:  nn0lt2  11702  nn0le2is012  11703  zadd2cl  11752  uzuzle23  11943  2eluzge1  11948  eluz2b1  11974  nn01to3  11996  nn0ge2m1nnALT  11997  ige2m1fz  12649  fz0to3un2pr  12661  fz0to4untppr  12662  fzctr  12671  fzo0to2pr  12773  fzo0to42pr  12775  2tnp1ge0ge0  12850  flhalf  12851  m1modge3gt1  12937  2txmodxeq0  12950  f13idfv  13019  sq1  13177  expnass  13189  sqrecd  13231  sqoddm1div8  13247  bcn2m1  13327  bcn2p1  13328  4bc2eq6  13332  hashtpg  13480  ccat2s1p2  13624  swrdtrcfv0  13662  swrdtrcfvl  13670  eqwrds3  13925  iseraltlem2  14632  iseraltlem3  14633  climcndslem1  14799  climcnds  14801  bpolydiflem  15001  efgt0  15049  tanval3  15080  cos01bnd  15132  cos01gt0  15137  odd2np1  15281  even2n  15282  oddm1even  15283  oddp1even  15284  oexpneg  15285  mod2eq1n2dvds  15287  2tp1odd  15292  2teven  15295  evend2  15297  oddp1d2  15298  ltoddhalfle  15301  opoe  15303  omoe  15304  opeo  15305  omeo  15306  m1expo  15308  m1exp1  15309  nn0o  15315  z0even  15319  n2dvds1  15320  z2even  15322  n2dvds3  15323  z4even  15324  4dvdseven  15325  sumeven  15326  flodddiv4  15352  bits0e  15366  bits0o  15367  bitsp1e  15369  bitsp1o  15370  bitsfzo  15372  bitsmod  15373  bitscmp  15375  bitsinv1lem  15378  bitsinv1  15379  6gcd4e2  15470  3lcm2e6woprm  15543  lcmf2a3a4e12  15575  isprm3  15610  dvdsnprmd  15617  2prm  15619  3prm  15620  oddprmge3  15626  isprm7  15633  divgcdodd  15635  oddprm  15728  pythagtriplem4  15737  pythagtriplem11  15743  pythagtriplem13  15745  iserodd  15753  prmgaplem3  15970  prmgaplem7  15974  dec2dvds  15980  prmlem0  16020  4001lem1  16055  psgnunilem4  18114  efgredleme  18353  lt6abl  18493  zringndrg  20042  znidomb  20113  chfacfscmulfsupp  20873  chfacfpmmulfsupp  20877  minveclem2  23405  minveclem3  23408  pjthlem1  23416  dyaddisjlem  23572  mbfi1fseqlem5  23696  iblcnlem1  23764  dvrecg  23946  dvexp3  23951  aaliou3lem6  24313  tanregt0  24496  efif1olem4  24502  tanarg  24575  cubic2  24785  asinlem3  24808  atantayl2  24875  cxp2limlem  24912  lgamgulmlem3  24967  lgamgulmlem4  24968  basellem2  25018  basellem3  25019  basellem4  25020  basellem5  25021  basellem8  25024  basellem9  25025  ppisval  25040  ppiprm  25087  ppinprm  25088  chtprm  25089  chtnprm  25090  chtdif  25094  ppidif  25099  ppi1  25100  cht1  25101  cht3  25109  ppieq0  25112  ppiublem1  25137  ppiublem2  25138  chpeq0  25143  chtub  25147  chpval2  25153  chpub  25155  mersenne  25162  perfect1  25163  perfectlem1  25164  perfectlem2  25165  bposlem1  25219  bposlem2  25220  bposlem3  25221  bposlem5  25223  bposlem6  25224  lgslem1  25232  lgsdir2lem2  25261  lgsdir2lem3  25262  lgsdir2  25265  lgsqr  25286  gausslemma2dlem0i  25299  gausslemma2dlem1a  25300  gausslemma2dlem5a  25305  gausslemma2dlem5  25306  gausslemma2dlem6  25307  gausslemma2dlem7  25308  gausslemma2d  25309  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem3  25312  lgseisenlem4  25313  lgsquadlem1  25315  lgsquadlem2  25316  lgsquad2lem1  25319  lgsquad2lem2  25320  lgsquad2  25321  lgsquad3  25322  m1lgs  25323  2lgslem1a1  25324  2lgslem1a2  25325  2lgslem1b  25327  2lgslem2  25330  2lgslem3b1  25336  2lgslem3c1  25337  2lgs2  25340  2lgs  25342  2lgsoddprmlem2  25344  2lgsoddprmlem3  25349  2lgsoddprm  25351  2sqblem  25366  chebbnd1lem1  25368  chebbnd1lem3  25370  chebbnd1  25371  dchrisum0lem1a  25385  dchrvmasumiflem1  25400  dchrisum0flblem1  25407  dchrisum0flblem2  25408  dchrisum0lem1b  25414  dchrisum0lem1  25415  dchrisum0lem2a  25416  dchrisum0lem2  25417  dchrisum0lem3  25418  mulog2sumlem2  25434  pntlemd  25493  pntlema  25495  pntlemb  25496  pntlemh  25498  pntlemr  25501  pntlemf  25504  pntlemo  25506  istrkg2ld  25569  istrkg3ld  25570  axlowdimlem3  26034  axlowdimlem6  26037  axlowdimlem16  26047  axlowdimlem17  26048  axlowdim  26051  usgrexmpldifpr  26362  usgrexmplef  26363  cusgrsizeindb1  26570  pthdlem1  26886  clwlkclwwlklem2a1  27131  clwlkclwwlklem2fv1  27134  clwlkclwwlklem2fv2  27135  clwlkclwwlklem2a4  27136  clwlkclwwlklem2a  27137  clwwisshclwwslem  27153  eupth2lem3lem3  27399  eupth2lemb  27406  konigsberglem5  27425  2clwwlk2  27521  numclwwlk2lem1  27552  numclwlk2lem2f  27553  numclwwlk2lem1OLD  27559  numclwlk2lem2fOLD  27560  frgrreggt1  27577  ex-fl  27631  ex-mod  27633  ex-hash  27637  ex-dvds  27640  ex-ind-dvds  27645  minvecolem3  28057  pjhthlem1  28575  znsqcld  29836  2sqmod  29970  archirngz  30065  archiabllem2c  30071  lmat22det  30210  dya2ub  30654  dya2icoseg  30661  oddpwdc  30738  eulerpartlemd  30750  eulerpartlemt  30755  ballotlem2  30872  signslema  30961  prodfzo03  31003  hgt750leme  31058  tgoldbachgtde  31060  nn0prpwlem  32635  knoppndvlem2  32818  knoppndvlem8  32824  poimirlem25  33744  poimirlem26  33745  poimirlem27  33746  poimirlem28  33747  acongrep  38045  acongeq  38048  jm2.18  38053  jm2.22  38060  jm2.23  38061  jm2.20nn  38062  jm2.26a  38065  jm2.26  38067  jm2.15nn0  38068  jm2.27a  38070  jm2.27c  38072  rmydioph  38079  jm3.1lem1  38082  jm3.1lem3  38084  expdiophlem1  38086  expdiophlem2  38087  hashnzfz2  39017  sumnnodd  40339  coskpi2  40554  cosknegpi  40557  dvdivbd  40615  stoweidlem26  40719  wallispilem4  40761  wallispi2lem1  40764  wallispi2lem2  40765  wallispi2  40766  stirlinglem1  40767  stirlinglem3  40769  stirlinglem7  40773  stirlinglem8  40774  stirlinglem10  40776  stirlinglem11  40777  stirlinglem15  40781  dirkertrigeqlem1  40791  dirkercncflem2  40797  fourierdlem54  40853  fourierdlem56  40855  fourierdlem57  40856  fourierdlem102  40901  fourierdlem114  40913  fourierswlem  40923  fouriersw  40924  smfmullem4  41480  pfxtrcfv0  41974  pfxtrcfvl  41977  fmtnorec1  42021  goldbachthlem2  42030  odz2prm2pw  42047  fmtnoprmfac1  42049  fmtnoprmfac2lem1  42050  fmtnoprmfac2  42051  fmtno4prmfac  42056  31prm  42084  sfprmdvdsmersenne  42092  lighneallem1  42094  lighneallem4a  42097  lighneallem4b  42098  lighneallem4  42099  proththdlem  42102  proththd  42103  3exp4mod41  42105  41prothprmlem2  42107  m1expevenALTV  42132  dfeven2  42134  oexpnegALTV  42160  oexpnegnz  42161  2evenALTV  42175  2noddALTV  42176  nn0o1gt2ALTV  42177  nnpw2evenALTV  42183  perfectALTVlem1  42202  perfectALTVlem2  42203  sbgoldbalt  42241  mogoldbb  42245  nnsum4primesodd  42256  nnsum4primesoddALTV  42257  wtgoldbnnsum4prm  42262  bgoldbnnsum3prm  42264  2even  42498  zlmodzxzequa  42850  zlmodzxznm  42851  zlmodzxzequap  42853  zlmodzxzldeplem1  42854  zlmodzxzldeplem3  42856  zlmodzxzldep  42858  ldepsnlinclem1  42859  ldepsnlinc  42862  pw2m1lepw2m1  42875  fldivexpfllog2  42924  nnlog2ge0lt1  42925  logbpw2m1  42926  fllog2  42927  blennnelnn  42935  blenpw2  42937  nnpw2blenfzo  42940  blennnt2  42948  nnolog2flm1  42949  dig2nn0ld  42963  dig2nn1st  42964  0dig2pr01  42969  0dig2nn0o  42972