MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2z Structured version   Visualization version   GIF version

Theorem 2z 11447
Description: 2 is an integer. (Contributed by NM, 10-May-2004.)
Assertion
Ref Expression
2z 2 ∈ ℤ

Proof of Theorem 2z
StepHypRef Expression
1 2nn 11223 . 2 2 ∈ ℕ
21nnzi 11439 1 2 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  2c2 11108  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-z 11416
This theorem is referenced by:  nn0lt2  11478  nn0le2is012  11479  zadd2cl  11528  uzuzle23  11767  2eluzge1  11772  eluz2b1  11797  nn01to3  11819  nn0ge2m1nnALT  11820  ige2m1fz  12468  fz0to3un2pr  12480  fz0to4untppr  12481  fzctr  12490  fzo0to2pr  12593  fzo0to42pr  12595  2tnp1ge0ge0  12670  flhalf  12671  m1modge3gt1  12757  2txmodxeq0  12770  f13idfv  12840  sq1  12998  expnass  13010  sqrecd  13052  sqoddm1div8  13068  bcn2m1  13151  bcn2p1  13152  4bc2eq6  13156  hashtpg  13305  ccat2s1p2  13450  swrdtrcfv0  13488  swrdtrcfvl  13496  eqwrds3  13750  iseraltlem2  14457  iseraltlem3  14458  climcndslem1  14625  climcnds  14627  bpolydiflem  14829  efgt0  14877  tanval3  14908  cos01bnd  14960  cos01gt0  14965  odd2np1  15112  even2n  15113  oddm1even  15114  oddp1even  15115  oexpneg  15116  mod2eq1n2dvds  15118  2tp1odd  15123  2teven  15126  evend2  15128  oddp1d2  15129  ltoddhalfle  15132  opoe  15134  omoe  15135  opeo  15136  omeo  15137  m1expo  15139  m1exp1  15140  nn0o  15146  z0even  15150  n2dvds1  15151  z2even  15153  n2dvds3  15154  z4even  15155  4dvdseven  15156  sumeven  15157  flodddiv4  15184  bits0e  15198  bits0o  15199  bitsp1e  15201  bitsp1o  15202  bitsfzo  15204  bitsmod  15205  bitscmp  15207  bitsinv1lem  15210  bitsinv1  15211  6gcd4e2  15302  3lcm2e6woprm  15375  lcmf2a3a4e12  15407  isprm3  15443  dvdsnprmd  15450  2prm  15452  3prm  15453  oddprmge3  15459  isprm7  15467  divgcdodd  15469  oddprm  15562  pythagtriplem4  15571  pythagtriplem11  15577  pythagtriplem13  15579  iserodd  15587  prmgaplem3  15804  prmgaplem7  15808  dec2dvds  15814  prmlem0  15859  4001lem1  15895  psgnunilem4  17963  efgredleme  18202  lt6abl  18342  zringndrg  19886  znidomb  19958  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  minveclem2  23243  minveclem3  23246  pjthlem1  23254  dyaddisjlem  23409  mbfi1fseqlem5  23531  iblcnlem1  23599  dvrecg  23781  dvexp3  23786  aaliou3lem6  24148  tanregt0  24330  efif1olem4  24336  tanarg  24410  cubic2  24620  asinlem3  24643  atantayl2  24710  cxp2limlem  24747  lgamgulmlem3  24802  lgamgulmlem4  24803  basellem2  24853  basellem3  24854  basellem4  24855  basellem5  24856  basellem8  24859  basellem9  24860  ppisval  24875  ppiprm  24922  ppinprm  24923  chtprm  24924  chtnprm  24925  chtdif  24929  ppidif  24934  ppi1  24935  cht1  24936  cht3  24944  ppieq0  24947  ppiublem1  24972  ppiublem2  24973  chpeq0  24978  chtub  24982  chpval2  24988  chpub  24990  mersenne  24997  perfect1  24998  perfectlem1  24999  perfectlem2  25000  bposlem1  25054  bposlem2  25055  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgslem1  25067  lgsdir2lem2  25096  lgsdir2lem3  25097  lgsdir2  25100  lgsqr  25121  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  gausslemma2dlem5a  25140  gausslemma2dlem5  25141  gausslemma2dlem6  25142  gausslemma2dlem7  25143  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  lgsquad2lem2  25155  lgsquad2  25156  lgsquad3  25157  m1lgs  25158  2lgslem1a1  25159  2lgslem1a2  25160  2lgslem1b  25162  2lgslem2  25165  2lgslem3b1  25171  2lgslem3c1  25172  2lgs2  25175  2lgs  25177  2lgsoddprmlem2  25179  2lgsoddprmlem3  25184  2lgsoddprm  25186  2sqblem  25201  chebbnd1lem1  25203  chebbnd1lem3  25205  chebbnd1  25206  dchrisum0lem1a  25220  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  mulog2sumlem2  25269  pntlemd  25328  pntlema  25330  pntlemb  25331  pntlemh  25333  pntlemr  25336  pntlemf  25339  pntlemo  25341  istrkg2ld  25404  istrkg3ld  25405  axlowdimlem3  25869  axlowdimlem6  25872  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  usgrexmpldifpr  26195  usgrexmplef  26196  cusgrsizeindb1  26402  pthdlem1  26718  clwlkclwwlklem2a1  26958  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwwisshclwwslem  26971  eupth2lem3lem3  27208  eupth2lemb  27215  konigsberglem5  27234  2clwwlk2  27336  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  frgrreggt1  27380  ex-fl  27434  ex-mod  27436  ex-hash  27440  ex-dvds  27443  ex-ind-dvds  27448  minvecolem3  27860  pjhthlem1  28378  znsqcld  29640  2sqmod  29776  archirngz  29871  archiabllem2c  29877  lmat22det  30016  dya2ub  30460  dya2icoseg  30467  oddpwdc  30544  eulerpartlemd  30556  eulerpartlemt  30561  ballotlem2  30678  signslema  30767  prodfzo03  30809  hgt750leme  30864  tgoldbachgtde  30866  nn0prpwlem  32442  knoppndvlem2  32629  knoppndvlem8  32635  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  acongrep  37864  acongeq  37867  jm2.18  37872  jm2.22  37879  jm2.23  37880  jm2.20nn  37881  jm2.26a  37884  jm2.26  37886  jm2.15nn0  37887  jm2.27a  37889  jm2.27c  37891  rmydioph  37898  jm3.1lem1  37901  jm3.1lem3  37903  expdiophlem1  37905  expdiophlem2  37906  hashnzfz2  38837  sumnnodd  40180  coskpi2  40395  cosknegpi  40398  dvdivbd  40456  stoweidlem26  40561  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  stirlinglem15  40623  dirkertrigeqlem1  40633  dirkercncflem2  40639  fourierdlem54  40695  fourierdlem56  40697  fourierdlem57  40698  fourierdlem102  40743  fourierdlem114  40755  fourierswlem  40765  fouriersw  40766  smfmullem4  41322  pfxtrcfv0  41727  pfxtrcfvl  41730  fmtnorec1  41774  goldbachthlem2  41783  odz2prm2pw  41800  fmtnoprmfac1  41802  fmtnoprmfac2lem1  41803  fmtnoprmfac2  41804  fmtno4prmfac  41809  31prm  41837  sfprmdvdsmersenne  41845  lighneallem1  41847  lighneallem4a  41850  lighneallem4b  41851  lighneallem4  41852  proththdlem  41855  proththd  41856  3exp4mod41  41858  41prothprmlem2  41860  m1expevenALTV  41885  dfeven2  41887  oexpnegALTV  41913  oexpnegnz  41914  2evenALTV  41928  2noddALTV  41929  nn0o1gt2ALTV  41930  nnpw2evenALTV  41936  perfectALTVlem1  41955  perfectALTVlem2  41956  sbgoldbalt  41994  mogoldbb  41998  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  2even  42258  zlmodzxzequa  42610  zlmodzxznm  42611  zlmodzxzequap  42613  zlmodzxzldeplem1  42614  zlmodzxzldeplem3  42616  zlmodzxzldep  42618  ldepsnlinclem1  42619  ldepsnlinc  42622  pw2m1lepw2m1  42635  fldivexpfllog2  42684  nnlog2ge0lt1  42685  logbpw2m1  42686  fllog2  42687  blennnelnn  42695  blenpw2  42697  nnpw2blenfzo  42700  blennnt2  42708  nnolog2flm1  42709  dig2nn0ld  42723  dig2nn1st  42724  0dig2pr01  42729  0dig2nn0o  42732
  Copyright terms: Public domain W3C validator