Theorem 2z 12650

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

This proof depends on syntax axioms:   ∈ wcel 2145  2c2 12319  ℤcz 12615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rrecex 11196  ax-cnre 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11468  df-nn 12258  df-2 12327  df-z 12616

This theorem is used by:  nn0lt2  12684  nn0le2is012  12685  zadd2cl  12733  2eluzge1  12931  uzuzle23  12933  uzuzle24  12934  eluz2b1  12968  nn01to3  12990  nn0ge2m1nnALT  12991  ige2m1fz  13672  fz0to3un2pr  13684  fz0to4untppr  13685  fz0to5un2tp  13686  fzctr  13695  fzo0to2pr  13806  fzo0to42pr  13809  2tnp1ge0ge0  13890  flhalf  13891  m1modge3gt1  13982  2txmodxeq0  13995  f13idfv  14064  sqrecd  14214  znsqcld  14226  sq1  14259  expnass  14272  sqoddm1div8  14307  bcn2m1  14388  bcn2p1  14389  4bc2eq6  14393  hashtpg  14550  ccat2s1p2  14698  pfxtrcfv0  14763  pfxtrcfvl  14766  eqwrds3  15034  iseraltlem2  15770  iseraltlem3  15771  climcndslem1  15938  climcnds  15940  bpolydiflem  16140  efgt0  16191  tanval3  16222  cos01bnd  16274  cos01gt0  16279  odd2np1  16431  even2n  16432  oddm1even  16433  oddp1even  16434  oexpneg  16435  mod2eq1n2dvds  16437  2tp1odd  16442  2teven  16445  evend2  16447  oddp1d2  16448  ltoddhalfle  16451  opoe  16453  omoe  16454  opeo  16455  omeo  16456  z0even  16457  z2even  16460  z4even  16462  4dvdseven  16463  m1expo  16465  m1exp1  16466  nn0o  16473  sumeven  16477  flodddiv4  16505  bits0e  16519  bits0o  16520  bitsp1e  16522  bitsp1o  16523  bitsfzo  16525  bitsmod  16526  bitscmp  16528  bitsinv1lem  16531  bitsinv1  16532  6gcd4e2  16628  3lcm2e6woprm  16705  lcmf2a3a4e12  16737  isprm3  16773  dvdsnprmd  16780  2prm  16782  2mulprm  16783  oddprmge3  16791  ge2nprmge4  16792  isprm7  16799  divgcdodd  16801  oddprm  16902  pythagtriplem4  16911  pythagtriplem11  16917  pythagtriplem13  16919  iserodd  16927  prmgaplem3  17145  prmgaplem7  17149  dec2dvds  17155  prmlem0  17197  4001lem1  17233  ex-chn1  18725  psgnunilem4  19624  efgredleme  19870  lt6abl  20022  ablsimpgfindlem1  20236  ablsimpgfindlem2  20237  zringndrg  21681  znidomb  21774  chfacfscmulfsupp  23084  chfacfpmmulfsupp  23088  minveclem2  25654  minveclem3  25657  pjthlem1  25665  dyaddisjlem  25823  mbfi1fseqlem5  25947  dvrecg  26200  dvexp3  26205  aaliou3lem6  26584  tanregt0  26776  efif1olem4  26782  tanarg  26856  cxpsqrtth  26967  2irrexpq  26968  2logb9irr  27032  2logb9irrALT  27035  sqrt2cxp2logb9e3  27036  cubic2  27085  asinlem3  27108  atantayl2  27175  cxp2limlem  27212  lgamgulmlem3  27267  lgamgulmlem4  27268  basellem2  27318  basellem3  27319  basellem4  27320  basellem5  27321  basellem8  27324  basellem9  27325  ppisval  27340  ppiprm  27387  ppinprm  27388  chtprm  27389  chtnprm  27390  chtdif  27394  ppidif  27399  ppi1  27400  cht1  27401  cht3  27409  ppieq0  27412  ppiublem1  27438  chpeq0  27444  chtub  27448  chpval2  27454  chpub  27456  mersenne  27463  perfect1  27464  perfectlem1  27465  perfectlem2  27466  bposlem1  27520  bposlem2  27521  bposlem3  27522  bposlem5  27524  bposlem6  27525  lgslem1  27533  lgsdir2lem2  27562  lgsdir2  27566  lgsqr  27587  gausslemma2dlem0i  27600  gausslemma2dlem1a  27601  gausslemma2dlem5a  27606  gausslemma2dlem5  27607  gausslemma2dlem6  27608  gausslemma2dlem7  27609  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  lgsquadlem2  27617  lgsquad2lem1  27620  lgsquad2lem2  27621  lgsquad2  27622  lgsquad3  27623  m1lgs  27624  2lgslem1a1  27625  2lgslem1a2  27626  2lgslem1b  27628  2lgslem3b1  27637  2lgslem3c1  27638  2lgs2  27641  2lgs  27643  2lgsoddprmlem2  27645  2lgsoddprmlem3  27650  2lgsoddprm  27652  2sqblem  27667  2sqmod  27672  chebbnd1lem1  27705  chebbnd1lem3  27707  chebbnd1  27708  dchrisum0lem1a  27722  dchrvmasumiflem1  27737  dchrisum0flblem1  27744  dchrisum0flblem2  27745  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  mulog2sumlem2  27771  pntlemd  27830  pntlema  27832  pntlemb  27833  pntlemh  27835  pntlemr  27838  pntlemf  27841  pntlemo  27843  istrkg2ld  28801  istrkg3ld  28802  axlowdimlem3  29401  axlowdimlem6  29404  axlowdimlem16  29414  axlowdimlem17  29415  axlowdim  29418  usgrexmpldifpr  29718  usgrexmplef  29719  cusgrsizeindb1  29910  pthdlem1  30231  clwlkclwwlklem2a1  30462  clwlkclwwlklem2fv1  30465  clwlkclwwlklem2fv2  30466  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwwisshclwwslem  30484  eupth2lem3lem3  30710  konigsberglem5  30736  2clwwlk2  30828  numclwwlk2lem1  30856  numclwlk2lem2f  30857  frgrreggt1  30873  ex-fl  30927  ex-mod  30929  ex-hash  30933  ex-dvds  30936  ex-ind-dvds  30941  minvecolem3  31357  pjhthlem1  31872  wrdt2ind  33395  archirngz  33629  archiabllem2c  33635  evl1deg2  33987  rtelextdg2  34237  constrext2chnlem  34260  constrresqrtcl  34287  2sqr3minply  34290  cos9thpiminplylem2  34293  cos9thpiminplylem5  34296  lmat22det  34332  dya2ub  34781  dya2icoseg  34788  oddpwdc  34865  eulerpartlemd  34877  eulerpartlemt  34882  ballotlem2  35000  signslema  35070  prodfzo03  35111  hgt750leme  35166  tgoldbachgtde  35168  nn0prpwlem  36941  knoppndvlem2  37210  knoppndvlem8  37216  irrdifflemf  38077  qdiff  38079  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  logblebd  42843  lcm2un  42880  lcm3un  42881  lcmineqlem18  42912  lcmineqlem19  42913  lcmineqlem21  42915  lcmineqlem22  42916  3lexlogpow5ineq2  42921  3lexlogpow2ineq1  42924  aks4d1p1p3  42935  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p3  42944  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  5bc2eq10  43008  2np3bcnp1  43010  2ap1caineq  43011  aks6d1c6lem4  43039  aks6d1c7lem1  43046  aks6d1c7lem2  43047  flt4lem2  43493  flt4lem5  43496  flt4lem7  43505  nna4b4nsq  43506  acongrep  43821  acongeq  43824  jm2.18  43829  jm2.22  43836  jm2.23  43837  jm2.20nn  43838  jm2.26a  43841  jm2.26  43843  jm2.15nn0  43844  jm2.27a  43846  jm2.27c  43848  rmydioph  43855  jm3.1lem1  43858  jm3.1lem3  43860  expdiophlem1  43862  expdiophlem2  43863  hashnzfz2  45145  sumnnodd  46460  coskpi2  46694  cosknegpi  46697  dvdivbd  46751  stoweidlem26  46854  wallispilem4  46896  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem3  46904  stirlinglem7  46908  stirlinglem8  46909  stirlinglem10  46911  stirlinglem11  46912  stirlinglem15  46916  dirkertrigeqlem1  46926  dirkercncflem2  46932  fourierdlem54  46988  fourierdlem56  46990  fourierdlem57  46991  fourierdlem102  47036  fourierdlem114  47048  fourierswlem  47058  fouriersw  47059  smfmullem4  47622  evenwodadd  47729  sqrtnpoly  47761  nnmul2  48218  ceil5half3  48234  addmodne  48238  m1modnep2mod  48246  minusmodnep2tmod  48247  modmkpkne  48255  modmknepk  48256  modm2nep1  48260  modp2nep1  48261  modm1nep2  48262  modm1nem2  48263  2timesltsq  48266  2timesltsqm1  48267  fmtnorec1  48440  goldbachthlem2  48449  odz2prm2pw  48466  fmtnoprmfac1  48468  fmtnoprmfac2lem1  48469  fmtnoprmfac2  48470  fmtno4prmfac  48475  31prm  48500  sfprmdvdsmersenne  48506  lighneallem1  48508  lighneallem4a  48511  lighneallem4b  48512  lighneallem4  48513  proththdlem  48516  proththd  48517  3exp4mod41  48519  41prothprmlem2  48521  nprmdvdsfacm1lem1  48523  nprmdvdsfacm1lem2  48524  nprmdvdsfacm1lem4  48526  ppivalnnnprmge6  48529  ppivalnn  48535  m1expevenALTV  48563  dfeven2  48565  m2even  48570  gcd2odd1  48584  oexpnegALTV  48593  oexpnegnz  48594  2evenALTV  48608  2noddALTV  48609  nn0o1gt2ALTV  48610  nnpw2evenALTV  48618  perfectALTVlem1  48637  perfectALTVlem2  48638  fppr2odd  48647  341fppr2  48650  9fppr8  48653  nfermltl2rev  48659  sbgoldbalt  48697  mogoldbb  48701  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  gpg5order  48976  gpg5nbgrvtx13starlem2  48988  gpg3nbgrvtx0ALT  48993  gpg3kgrtriexlem5  49003  gpg5gricstgr3  49006  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  gpg5edgnedg  49046  2even  49154  zlmodzxzequa  49426  zlmodzxznm  49427  zlmodzxzequap  49429  zlmodzxzldeplem1  49430  zlmodzxzldeplem3  49432  zlmodzxzldep  49434  ldepsnlinclem1  49435  ldepsnlinc  49438  pw2m1lepw2m1  49450  fldivexpfllog2  49495  nnlog2ge0lt1  49496  logbpw2m1  49497  fllog2  49498  blennnelnn  49506  blenpw2  49508  nnpw2blenfzo  49511  blennnt2  49519  nnolog2flm1  49520  dig2nn0ld  49534  dig2nn1st  49535  0dig2pr01  49540  0dig2nn0o  49543  ackval42  49626  itsclc0xyqsolr  49699  crosspdotsumlem  50797  veronesev2lem  50807