Theorem 2z 12649

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

Syntax hints:   ∈ wcel 2108  2c2 12321  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-2 12329  df-z 12614

This theorem is referenced by:  nn0lt2  12681  nn0le2is012  12682  zadd2cl  12730  eluz4eluz2  12925  uzuzle23  12931  2eluzge1  12936  eluz2b1  12961  nn01to3  12983  nn0ge2m1nnALT  12984  ige2m1fz  13657  fz0to3un2pr  13669  fz0to4untppr  13670  fz0to5un2tp  13671  fzctr  13680  fzo0to2pr  13789  fzo0to42pr  13792  2tnp1ge0ge0  13869  flhalf  13870  m1modge3gt1  13959  2txmodxeq0  13972  f13idfv  14041  sqrecd  14190  znsqcld  14202  sq1  14234  expnass  14247  sqoddm1div8  14282  bcn2m1  14363  bcn2p1  14364  4bc2eq6  14368  hashtpg  14524  ccat2s1p2  14668  pfxtrcfv0  14732  pfxtrcfvl  14735  eqwrds3  15000  iseraltlem2  15719  iseraltlem3  15720  climcndslem1  15885  climcnds  15887  bpolydiflem  16090  efgt0  16139  tanval3  16170  cos01bnd  16222  cos01gt0  16227  odd2np1  16378  even2n  16379  oddm1even  16380  oddp1even  16381  oexpneg  16382  mod2eq1n2dvds  16384  2tp1odd  16389  2teven  16392  evend2  16394  oddp1d2  16395  ltoddhalfle  16398  opoe  16400  omoe  16401  opeo  16402  omeo  16403  z0even  16404  z2even  16407  z4even  16409  4dvdseven  16410  m1expo  16412  m1exp1  16413  nn0o  16420  sumeven  16424  flodddiv4  16452  bits0e  16466  bits0o  16467  bitsp1e  16469  bitsp1o  16470  bitsfzo  16472  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  bitsinv1  16479  6gcd4e2  16575  3lcm2e6woprm  16652  lcmf2a3a4e12  16684  isprm3  16720  dvdsnprmd  16727  2prm  16729  2mulprm  16730  oddprmge3  16737  ge2nprmge4  16738  isprm7  16745  divgcdodd  16747  oddprm  16848  pythagtriplem4  16857  pythagtriplem11  16863  pythagtriplem13  16865  iserodd  16873  prmgaplem3  17091  prmgaplem7  17095  dec2dvds  17101  prmlem0  17143  4001lem1  17178  psgnunilem4  19515  efgredleme  19761  lt6abl  19913  ablsimpgfindlem1  20127  ablsimpgfindlem2  20128  zringndrg  21479  znidomb  21580  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  minveclem2  25460  minveclem3  25463  pjthlem1  25471  dyaddisjlem  25630  mbfi1fseqlem5  25754  dvrecg  26011  dvexp3  26016  aaliou3lem6  26390  tanregt0  26581  efif1olem4  26587  tanarg  26661  cxpsqrtth  26772  2irrexpq  26773  2logb9irr  26838  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  cubic2  26891  asinlem3  26914  atantayl2  26981  cxp2limlem  27019  lgamgulmlem3  27074  lgamgulmlem4  27075  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  basellem8  27131  basellem9  27132  ppisval  27147  ppiprm  27194  ppinprm  27195  chtprm  27196  chtnprm  27197  chtdif  27201  ppidif  27206  ppi1  27207  cht1  27208  cht3  27216  ppieq0  27219  ppiublem1  27246  chpeq0  27252  chtub  27256  chpval2  27262  chpub  27264  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgslem1  27341  lgsdir2lem2  27370  lgsdir2  27374  lgsqr  27395  gausslemma2dlem0i  27408  gausslemma2dlem1a  27409  gausslemma2dlem5a  27414  gausslemma2dlem5  27415  gausslemma2dlem6  27416  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem1  27428  lgsquad2lem2  27429  lgsquad2  27430  lgsquad3  27431  m1lgs  27432  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1b  27436  2lgslem3b1  27445  2lgslem3c1  27446  2lgs2  27449  2lgs  27451  2lgsoddprmlem2  27453  2lgsoddprmlem3  27458  2lgsoddprm  27460  2sqblem  27475  2sqmod  27480  chebbnd1lem1  27513  chebbnd1lem3  27515  chebbnd1  27516  dchrisum0lem1a  27530  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  mulog2sumlem2  27579  pntlemd  27638  pntlema  27640  pntlemb  27641  pntlemh  27643  pntlemr  27646  pntlemf  27649  pntlemo  27651  istrkg2ld  28468  istrkg3ld  28469  axlowdimlem3  28959  axlowdimlem6  28962  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  usgrexmpldifpr  29275  usgrexmplef  29276  cusgrsizeindb1  29468  pthdlem1  29786  clwlkclwwlklem2a1  30011  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwwisshclwwslem  30033  eupth2lem3lem3  30249  konigsberglem5  30275  2clwwlk2  30367  numclwwlk2lem1  30395  numclwlk2lem2f  30396  frgrreggt1  30412  ex-fl  30466  ex-mod  30468  ex-hash  30472  ex-dvds  30475  ex-ind-dvds  30480  minvecolem3  30895  pjhthlem1  31410  wrdt2ind  32938  archirngz  33196  archiabllem2c  33202  evl1deg2  33602  rtelextdg2  33768  2sqr3minply  33791  lmat22det  33821  dya2ub  34272  dya2icoseg  34279  oddpwdc  34356  eulerpartlemd  34368  eulerpartlemt  34373  ballotlem2  34491  signslema  34577  prodfzo03  34618  hgt750leme  34673  tgoldbachgtde  34675  nn0prpwlem  36323  knoppndvlem2  36514  knoppndvlem8  36520  irrdifflemf  37326  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  logblebd  41977  lcm2un  42015  lcm3un  42016  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem21  42050  lcmineqlem22  42051  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  aks4d1p1p3  42070  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p3  42079  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  5bc2eq10  42143  2np3bcnp1  42145  2ap1caineq  42146  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7lem2  42182  flt4lem2  42657  flt4lem5  42660  flt4lem7  42669  nna4b4nsq  42670  acongrep  42992  acongeq  42995  jm2.18  43000  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.26a  43012  jm2.26  43014  jm2.15nn0  43015  jm2.27a  43017  jm2.27c  43019  rmydioph  43026  jm3.1lem1  43029  jm3.1lem3  43031  expdiophlem1  43033  expdiophlem2  43034  hashnzfz2  44340  sumnnodd  45645  coskpi2  45881  cosknegpi  45884  dvdivbd  45938  stoweidlem26  46041  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem15  46103  dirkertrigeqlem1  46113  dirkercncflem2  46119  fourierdlem54  46175  fourierdlem56  46177  fourierdlem57  46178  fourierdlem102  46223  fourierdlem114  46235  fourierswlem  46245  fouriersw  46246  smfmullem4  46809  evenwodadd  46903  ceil5half3  47342  addmodne  47346  m1modnep2mod  47354  minusmodnep2tmod  47355  fmtnorec1  47524  goldbachthlem2  47533  odz2prm2pw  47550  fmtnoprmfac1  47552  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  fmtno4prmfac  47559  31prm  47584  sfprmdvdsmersenne  47590  lighneallem1  47592  lighneallem4a  47595  lighneallem4b  47596  lighneallem4  47597  proththdlem  47600  proththd  47601  3exp4mod41  47603  41prothprmlem2  47605  m1expevenALTV  47634  dfeven2  47636  m2even  47641  gcd2odd1  47655  oexpnegALTV  47664  oexpnegnz  47665  2evenALTV  47679  2noddALTV  47680  nn0o1gt2ALTV  47681  nnpw2evenALTV  47689  perfectALTVlem1  47708  perfectALTVlem2  47709  fppr2odd  47718  341fppr2  47721  9fppr8  47724  nfermltl2rev  47730  sbgoldbalt  47768  mogoldbb  47772  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  gpg5order  48014  gpg3nbgrvtxlem  48023  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0ALT  48033  gpg3kgrtriexlem5  48043  gpg5gricstgr3  48046  2even  48155  zlmodzxzequa  48413  zlmodzxznm  48414  zlmodzxzequap  48416  zlmodzxzldeplem1  48417  zlmodzxzldeplem3  48419  zlmodzxzldep  48421  ldepsnlinclem1  48422  ldepsnlinc  48425  pw2m1lepw2m1  48437  fldivexpfllog2  48486  nnlog2ge0lt1  48487  logbpw2m1  48488  fllog2  48489  blennnelnn  48497  blenpw2  48499  nnpw2blenfzo  48502  blennnt2  48510  nnolog2flm1  48511  dig2nn0ld  48525  dig2nn1st  48526  0dig2pr01  48531  0dig2nn0o  48534  ackval42  48617  itsclc0xyqsolr  48690