Theorem 2z 12510

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

Syntax hints:   ∈ wcel 2111  2c2 12186  ℤcz 12474

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 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-i2m1 11080  ax-1ne0 11081  ax-rrecex 11084  ax-cnre 11085

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 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11353  df-nn 12132  df-2 12194  df-z 12475

This theorem is referenced by:  nn0lt2  12542  nn0le2is012  12543  zadd2cl  12591  2eluzge1  12786  uzuzle23  12788  uzuzle24  12789  eluz2b1  12823  nn01to3  12845  nn0ge2m1nnALT  12846  ige2m1fz  13523  fz0to3un2pr  13535  fz0to4untppr  13536  fz0to5un2tp  13537  fzctr  13546  fzo0to2pr  13656  fzo0to42pr  13659  2tnp1ge0ge0  13739  flhalf  13740  m1modge3gt1  13831  2txmodxeq0  13844  f13idfv  13913  sqrecd  14063  znsqcld  14075  sq1  14108  expnass  14121  sqoddm1div8  14156  bcn2m1  14237  bcn2p1  14238  4bc2eq6  14242  hashtpg  14398  ccat2s1p2  14544  pfxtrcfv0  14607  pfxtrcfvl  14610  eqwrds3  14874  iseraltlem2  15596  iseraltlem3  15597  climcndslem1  15762  climcnds  15764  bpolydiflem  15967  efgt0  16018  tanval3  16049  cos01bnd  16101  cos01gt0  16106  odd2np1  16258  even2n  16259  oddm1even  16260  oddp1even  16261  oexpneg  16262  mod2eq1n2dvds  16264  2tp1odd  16269  2teven  16272  evend2  16274  oddp1d2  16275  ltoddhalfle  16278  opoe  16280  omoe  16281  opeo  16282  omeo  16283  z0even  16284  z2even  16287  z4even  16289  4dvdseven  16290  m1expo  16292  m1exp1  16293  nn0o  16300  sumeven  16304  flodddiv4  16332  bits0e  16346  bits0o  16347  bitsp1e  16349  bitsp1o  16350  bitsfzo  16352  bitsmod  16353  bitscmp  16355  bitsinv1lem  16358  bitsinv1  16359  6gcd4e2  16455  3lcm2e6woprm  16532  lcmf2a3a4e12  16564  isprm3  16600  dvdsnprmd  16607  2prm  16609  2mulprm  16610  oddprmge3  16617  ge2nprmge4  16618  isprm7  16625  divgcdodd  16627  oddprm  16728  pythagtriplem4  16737  pythagtriplem11  16743  pythagtriplem13  16745  iserodd  16753  prmgaplem3  16971  prmgaplem7  16975  dec2dvds  16981  prmlem0  17023  4001lem1  17058  ex-chn1  18549  psgnunilem4  19415  efgredleme  19661  lt6abl  19813  ablsimpgfindlem1  20027  ablsimpgfindlem2  20028  zringndrg  21411  znidomb  21504  chfacfscmulfsupp  22780  chfacfpmmulfsupp  22784  minveclem2  25359  minveclem3  25362  pjthlem1  25370  dyaddisjlem  25529  mbfi1fseqlem5  25653  dvrecg  25910  dvexp3  25915  aaliou3lem6  26289  tanregt0  26481  efif1olem4  26487  tanarg  26561  cxpsqrtth  26672  2irrexpq  26673  2logb9irr  26738  2logb9irrALT  26741  sqrt2cxp2logb9e3  26742  cubic2  26791  asinlem3  26814  atantayl2  26881  cxp2limlem  26919  lgamgulmlem3  26974  lgamgulmlem4  26975  basellem2  27025  basellem3  27026  basellem4  27027  basellem5  27028  basellem8  27031  basellem9  27032  ppisval  27047  ppiprm  27094  ppinprm  27095  chtprm  27096  chtnprm  27097  chtdif  27101  ppidif  27106  ppi1  27107  cht1  27108  cht3  27116  ppieq0  27119  ppiublem1  27146  chpeq0  27152  chtub  27156  chpval2  27162  chpub  27164  mersenne  27171  perfect1  27172  perfectlem1  27173  perfectlem2  27174  bposlem1  27228  bposlem2  27229  bposlem3  27230  bposlem5  27232  bposlem6  27233  lgslem1  27241  lgsdir2lem2  27270  lgsdir2  27274  lgsqr  27295  gausslemma2dlem0i  27308  gausslemma2dlem1a  27309  gausslemma2dlem5a  27314  gausslemma2dlem5  27315  gausslemma2dlem6  27316  gausslemma2dlem7  27317  gausslemma2d  27318  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgsquadlem1  27324  lgsquadlem2  27325  lgsquad2lem1  27328  lgsquad2lem2  27329  lgsquad2  27330  lgsquad3  27331  m1lgs  27332  2lgslem1a1  27333  2lgslem1a2  27334  2lgslem1b  27336  2lgslem3b1  27345  2lgslem3c1  27346  2lgs2  27349  2lgs  27351  2lgsoddprmlem2  27353  2lgsoddprmlem3  27358  2lgsoddprm  27360  2sqblem  27375  2sqmod  27380  chebbnd1lem1  27413  chebbnd1lem3  27415  chebbnd1  27416  dchrisum0lem1a  27430  dchrvmasumiflem1  27445  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  dchrisum0lem3  27463  mulog2sumlem2  27479  pntlemd  27538  pntlema  27540  pntlemb  27541  pntlemh  27543  pntlemr  27546  pntlemf  27549  pntlemo  27551  istrkg2ld  28444  istrkg3ld  28445  axlowdimlem3  28929  axlowdimlem6  28932  axlowdimlem16  28942  axlowdimlem17  28943  axlowdim  28946  usgrexmpldifpr  29243  usgrexmplef  29244  cusgrsizeindb1  29436  pthdlem1  29751  clwlkclwwlklem2a1  29979  clwlkclwwlklem2fv1  29982  clwlkclwwlklem2fv2  29983  clwlkclwwlklem2a4  29984  clwlkclwwlklem2a  29985  clwwisshclwwslem  30001  eupth2lem3lem3  30217  konigsberglem5  30243  2clwwlk2  30335  numclwwlk2lem1  30363  numclwlk2lem2f  30364  frgrreggt1  30380  ex-fl  30434  ex-mod  30436  ex-hash  30440  ex-dvds  30443  ex-ind-dvds  30448  minvecolem3  30863  pjhthlem1  31378  wrdt2ind  32941  archirngz  33165  archiabllem2c  33171  evl1deg2  33547  rtelextdg2  33747  constrext2chnlem  33770  constrresqrtcl  33797  2sqr3minply  33800  cos9thpiminplylem2  33803  cos9thpiminplylem5  33806  lmat22det  33842  dya2ub  34290  dya2icoseg  34297  oddpwdc  34374  eulerpartlemd  34386  eulerpartlemt  34391  ballotlem2  34509  signslema  34582  prodfzo03  34623  hgt750leme  34678  tgoldbachgtde  34680  nn0prpwlem  36373  knoppndvlem2  36564  knoppndvlem8  36570  irrdifflemf  37376  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  logblebd  42075  lcm2un  42113  lcm3un  42114  lcmineqlem18  42145  lcmineqlem19  42146  lcmineqlem21  42148  lcmineqlem22  42149  3lexlogpow5ineq2  42154  3lexlogpow2ineq1  42157  aks4d1p1p3  42168  aks4d1p1p4  42170  aks4d1p1p6  42172  aks4d1p1p7  42173  aks4d1p1p5  42174  aks4d1p1  42175  aks4d1p3  42177  aks4d1p6  42180  aks4d1p7d1  42181  aks4d1p7  42182  aks4d1p8  42186  aks4d1p9  42187  posbezout  42199  5bc2eq10  42241  2np3bcnp1  42243  2ap1caineq  42244  aks6d1c6lem4  42272  aks6d1c7lem1  42279  aks6d1c7lem2  42280  flt4lem2  42746  flt4lem5  42749  flt4lem7  42758  nna4b4nsq  42759  acongrep  43078  acongeq  43081  jm2.18  43086  jm2.22  43093  jm2.23  43094  jm2.20nn  43095  jm2.26a  43098  jm2.26  43100  jm2.15nn0  43101  jm2.27a  43103  jm2.27c  43105  rmydioph  43112  jm3.1lem1  43115  jm3.1lem3  43117  expdiophlem1  43119  expdiophlem2  43120  hashnzfz2  44419  sumnnodd  45735  coskpi2  45969  cosknegpi  45972  dvdivbd  46026  stoweidlem26  46129  wallispilem4  46171  wallispi2lem1  46174  wallispi2lem2  46175  wallispi2  46176  stirlinglem1  46177  stirlinglem3  46179  stirlinglem7  46183  stirlinglem8  46184  stirlinglem10  46186  stirlinglem11  46187  stirlinglem15  46191  dirkertrigeqlem1  46201  dirkercncflem2  46207  fourierdlem54  46263  fourierdlem56  46265  fourierdlem57  46266  fourierdlem102  46311  fourierdlem114  46323  fourierswlem  46333  fouriersw  46334  smfmullem4  46897  nthrucw  46989  evenwodadd  46990  ceil5half3  47445  addmodne  47449  m1modnep2mod  47457  minusmodnep2tmod  47458  modmkpkne  47466  modmknepk  47467  modm2nep1  47471  modp2nep1  47472  modm1nep2  47473  modm1nem2  47474  fmtnorec1  47642  goldbachthlem2  47651  odz2prm2pw  47668  fmtnoprmfac1  47670  fmtnoprmfac2lem1  47671  fmtnoprmfac2  47672  fmtno4prmfac  47677  31prm  47702  sfprmdvdsmersenne  47708  lighneallem1  47710  lighneallem4a  47713  lighneallem4b  47714  lighneallem4  47715  proththdlem  47718  proththd  47719  3exp4mod41  47721  41prothprmlem2  47723  m1expevenALTV  47752  dfeven2  47754  m2even  47759  gcd2odd1  47773  oexpnegALTV  47782  oexpnegnz  47783  2evenALTV  47797  2noddALTV  47798  nn0o1gt2ALTV  47799  nnpw2evenALTV  47807  perfectALTVlem1  47826  perfectALTVlem2  47827  fppr2odd  47836  341fppr2  47839  9fppr8  47842  nfermltl2rev  47848  sbgoldbalt  47886  mogoldbb  47890  nnsum4primesodd  47901  nnsum4primesoddALTV  47902  wtgoldbnnsum4prm  47907  bgoldbnnsum3prm  47909  gpg5order  48165  gpg5nbgrvtx13starlem2  48177  gpg3nbgrvtx0ALT  48182  gpg3kgrtriexlem5  48192  gpg5gricstgr3  48195  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  pgnbgreunbgrlem2lem3  48221  gpg5edgnedg  48235  2even  48344  zlmodzxzequa  48602  zlmodzxznm  48603  zlmodzxzequap  48605  zlmodzxzldeplem1  48606  zlmodzxzldeplem3  48608  zlmodzxzldep  48610  ldepsnlinclem1  48611  ldepsnlinc  48614  pw2m1lepw2m1  48626  fldivexpfllog2  48671  nnlog2ge0lt1  48672  logbpw2m1  48673  fllog2  48674  blennnelnn  48682  blenpw2  48684  nnpw2blenfzo  48687  blennnt2  48695  nnolog2flm1  48696  dig2nn0ld  48710  dig2nn1st  48711  0dig2pr01  48716  0dig2nn0o  48719  ackval42  48802  itsclc0xyqsolr  48875