Theorem 2z 12499

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

Syntax hints:   ∈ wcel 2111  2c2 12175  ℤcz 12463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-i2m1 11069  ax-1ne0 11070  ax-rrecex 11073  ax-cnre 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-neg 11342  df-nn 12121  df-2 12183  df-z 12464

This theorem is referenced by:  nn0lt2  12531  nn0le2is012  12532  zadd2cl  12580  2eluzge1  12775  uzuzle23  12777  uzuzle24  12778  eluz2b1  12812  nn01to3  12834  nn0ge2m1nnALT  12835  ige2m1fz  13512  fz0to3un2pr  13524  fz0to4untppr  13525  fz0to5un2tp  13526  fzctr  13535  fzo0to2pr  13645  fzo0to42pr  13648  2tnp1ge0ge0  13728  flhalf  13729  m1modge3gt1  13820  2txmodxeq0  13833  f13idfv  13902  sqrecd  14052  znsqcld  14064  sq1  14097  expnass  14110  sqoddm1div8  14145  bcn2m1  14226  bcn2p1  14227  4bc2eq6  14231  hashtpg  14387  ccat2s1p2  14533  pfxtrcfv0  14596  pfxtrcfvl  14599  eqwrds3  14863  iseraltlem2  15585  iseraltlem3  15586  climcndslem1  15751  climcnds  15753  bpolydiflem  15956  efgt0  16007  tanval3  16038  cos01bnd  16090  cos01gt0  16095  odd2np1  16247  even2n  16248  oddm1even  16249  oddp1even  16250  oexpneg  16251  mod2eq1n2dvds  16253  2tp1odd  16258  2teven  16261  evend2  16263  oddp1d2  16264  ltoddhalfle  16267  opoe  16269  omoe  16270  opeo  16271  omeo  16272  z0even  16273  z2even  16276  z4even  16278  4dvdseven  16279  m1expo  16281  m1exp1  16282  nn0o  16289  sumeven  16293  flodddiv4  16321  bits0e  16335  bits0o  16336  bitsp1e  16338  bitsp1o  16339  bitsfzo  16341  bitsmod  16342  bitscmp  16344  bitsinv1lem  16347  bitsinv1  16348  6gcd4e2  16444  3lcm2e6woprm  16521  lcmf2a3a4e12  16553  isprm3  16589  dvdsnprmd  16596  2prm  16598  2mulprm  16599  oddprmge3  16606  ge2nprmge4  16607  isprm7  16614  divgcdodd  16616  oddprm  16717  pythagtriplem4  16726  pythagtriplem11  16732  pythagtriplem13  16734  iserodd  16742  prmgaplem3  16960  prmgaplem7  16964  dec2dvds  16970  prmlem0  17012  4001lem1  17047  ex-chn1  18538  psgnunilem4  19404  efgredleme  19650  lt6abl  19802  ablsimpgfindlem1  20016  ablsimpgfindlem2  20017  zringndrg  21400  znidomb  21493  chfacfscmulfsupp  22769  chfacfpmmulfsupp  22773  minveclem2  25348  minveclem3  25351  pjthlem1  25359  dyaddisjlem  25518  mbfi1fseqlem5  25642  dvrecg  25899  dvexp3  25904  aaliou3lem6  26278  tanregt0  26470  efif1olem4  26476  tanarg  26550  cxpsqrtth  26661  2irrexpq  26662  2logb9irr  26727  2logb9irrALT  26730  sqrt2cxp2logb9e3  26731  cubic2  26780  asinlem3  26803  atantayl2  26870  cxp2limlem  26908  lgamgulmlem3  26963  lgamgulmlem4  26964  basellem2  27014  basellem3  27015  basellem4  27016  basellem5  27017  basellem8  27020  basellem9  27021  ppisval  27036  ppiprm  27083  ppinprm  27084  chtprm  27085  chtnprm  27086  chtdif  27090  ppidif  27095  ppi1  27096  cht1  27097  cht3  27105  ppieq0  27108  ppiublem1  27135  chpeq0  27141  chtub  27145  chpval2  27151  chpub  27153  mersenne  27160  perfect1  27161  perfectlem1  27162  perfectlem2  27163  bposlem1  27217  bposlem2  27218  bposlem3  27219  bposlem5  27221  bposlem6  27222  lgslem1  27230  lgsdir2lem2  27259  lgsdir2  27263  lgsqr  27284  gausslemma2dlem0i  27297  gausslemma2dlem1a  27298  gausslemma2dlem5a  27303  gausslemma2dlem5  27304  gausslemma2dlem6  27305  gausslemma2dlem7  27306  gausslemma2d  27307  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgseisenlem4  27311  lgsquadlem1  27313  lgsquadlem2  27314  lgsquad2lem1  27317  lgsquad2lem2  27318  lgsquad2  27319  lgsquad3  27320  m1lgs  27321  2lgslem1a1  27322  2lgslem1a2  27323  2lgslem1b  27325  2lgslem3b1  27334  2lgslem3c1  27335  2lgs2  27338  2lgs  27340  2lgsoddprmlem2  27342  2lgsoddprmlem3  27347  2lgsoddprm  27349  2sqblem  27364  2sqmod  27369  chebbnd1lem1  27402  chebbnd1lem3  27404  chebbnd1  27405  dchrisum0lem1a  27419  dchrvmasumiflem1  27434  dchrisum0flblem1  27441  dchrisum0flblem2  27442  dchrisum0lem1b  27448  dchrisum0lem1  27449  dchrisum0lem2a  27450  dchrisum0lem2  27451  dchrisum0lem3  27452  mulog2sumlem2  27468  pntlemd  27527  pntlema  27529  pntlemb  27530  pntlemh  27532  pntlemr  27535  pntlemf  27538  pntlemo  27540  istrkg2ld  28433  istrkg3ld  28434  axlowdimlem3  28917  axlowdimlem6  28920  axlowdimlem16  28930  axlowdimlem17  28931  axlowdim  28934  usgrexmpldifpr  29231  usgrexmplef  29232  cusgrsizeindb1  29424  pthdlem1  29739  clwlkclwwlklem2a1  29964  clwlkclwwlklem2fv1  29967  clwlkclwwlklem2fv2  29968  clwlkclwwlklem2a4  29969  clwlkclwwlklem2a  29970  clwwisshclwwslem  29986  eupth2lem3lem3  30202  konigsberglem5  30228  2clwwlk2  30320  numclwwlk2lem1  30348  numclwlk2lem2f  30349  frgrreggt1  30365  ex-fl  30419  ex-mod  30421  ex-hash  30425  ex-dvds  30428  ex-ind-dvds  30433  minvecolem3  30848  pjhthlem1  31363  wrdt2ind  32926  archirngz  33150  archiabllem2c  33156  evl1deg2  33532  rtelextdg2  33732  constrext2chnlem  33755  constrresqrtcl  33782  2sqr3minply  33785  cos9thpiminplylem2  33788  cos9thpiminplylem5  33791  lmat22det  33827  dya2ub  34275  dya2icoseg  34282  oddpwdc  34359  eulerpartlemd  34371  eulerpartlemt  34376  ballotlem2  34494  signslema  34567  prodfzo03  34608  hgt750leme  34663  tgoldbachgtde  34665  nn0prpwlem  36356  knoppndvlem2  36547  knoppndvlem8  36553  irrdifflemf  37359  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  logblebd  42009  lcm2un  42047  lcm3un  42048  lcmineqlem18  42079  lcmineqlem19  42080  lcmineqlem21  42082  lcmineqlem22  42083  3lexlogpow5ineq2  42088  3lexlogpow2ineq1  42091  aks4d1p1p3  42102  aks4d1p1p4  42104  aks4d1p1p6  42106  aks4d1p1p7  42107  aks4d1p1p5  42108  aks4d1p1  42109  aks4d1p3  42111  aks4d1p6  42114  aks4d1p7d1  42115  aks4d1p7  42116  aks4d1p8  42120  aks4d1p9  42121  posbezout  42133  5bc2eq10  42175  2np3bcnp1  42177  2ap1caineq  42178  aks6d1c6lem4  42206  aks6d1c7lem1  42213  aks6d1c7lem2  42214  flt4lem2  42680  flt4lem5  42683  flt4lem7  42692  nna4b4nsq  42693  acongrep  43013  acongeq  43016  jm2.18  43021  jm2.22  43028  jm2.23  43029  jm2.20nn  43030  jm2.26a  43033  jm2.26  43035  jm2.15nn0  43036  jm2.27a  43038  jm2.27c  43040  rmydioph  43047  jm3.1lem1  43050  jm3.1lem3  43052  expdiophlem1  43054  expdiophlem2  43055  hashnzfz2  44354  sumnnodd  45670  coskpi2  45904  cosknegpi  45907  dvdivbd  45961  stoweidlem26  46064  wallispilem4  46106  wallispi2lem1  46109  wallispi2lem2  46110  wallispi2  46111  stirlinglem1  46112  stirlinglem3  46114  stirlinglem7  46118  stirlinglem8  46119  stirlinglem10  46121  stirlinglem11  46122  stirlinglem15  46126  dirkertrigeqlem1  46136  dirkercncflem2  46142  fourierdlem54  46198  fourierdlem56  46200  fourierdlem57  46201  fourierdlem102  46246  fourierdlem114  46258  fourierswlem  46268  fouriersw  46269  smfmullem4  46832  evenwodadd  46916  ceil5half3  47371  addmodne  47375  m1modnep2mod  47383  minusmodnep2tmod  47384  modmkpkne  47392  modmknepk  47393  modm2nep1  47397  modp2nep1  47398  modm1nep2  47399  modm1nem2  47400  fmtnorec1  47568  goldbachthlem2  47577  odz2prm2pw  47594  fmtnoprmfac1  47596  fmtnoprmfac2lem1  47597  fmtnoprmfac2  47598  fmtno4prmfac  47603  31prm  47628  sfprmdvdsmersenne  47634  lighneallem1  47636  lighneallem4a  47639  lighneallem4b  47640  lighneallem4  47641  proththdlem  47644  proththd  47645  3exp4mod41  47647  41prothprmlem2  47649  m1expevenALTV  47678  dfeven2  47680  m2even  47685  gcd2odd1  47699  oexpnegALTV  47708  oexpnegnz  47709  2evenALTV  47723  2noddALTV  47724  nn0o1gt2ALTV  47725  nnpw2evenALTV  47733  perfectALTVlem1  47752  perfectALTVlem2  47753  fppr2odd  47762  341fppr2  47765  9fppr8  47768  nfermltl2rev  47774  sbgoldbalt  47812  mogoldbb  47816  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  gpg5order  48091  gpg5nbgrvtx13starlem2  48103  gpg3nbgrvtx0ALT  48108  gpg3kgrtriexlem5  48118  gpg5gricstgr3  48121  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  gpg5edgnedg  48161  2even  48270  zlmodzxzequa  48528  zlmodzxznm  48529  zlmodzxzequap  48531  zlmodzxzldeplem1  48532  zlmodzxzldeplem3  48534  zlmodzxzldep  48536  ldepsnlinclem1  48537  ldepsnlinc  48540  pw2m1lepw2m1  48552  fldivexpfllog2  48597  nnlog2ge0lt1  48598  logbpw2m1  48599  fllog2  48600  blennnelnn  48608  blenpw2  48610  nnpw2blenfzo  48613  blennnt2  48621  nnolog2flm1  48622  dig2nn0ld  48636  dig2nn1st  48637  0dig2pr01  48642  0dig2nn0o  48645  ackval42  48728  itsclc0xyqsolr  48801