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

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

Proof of Theorem 2z
StepHypRef Expression
1 2nn 11035 . 2 2 ∈ ℕ
21nnzi 11237 1 2 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  2c2 10920  cz 11213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-2 10929  df-z 11214
This theorem is referenced by:  nn0lt2  11276  zadd2cl  11325  uzuzle23  11564  2eluzge1  11569  eluz2b1  11594  nn01to3  11616  nn0ge2m1nnALT  11617  ige2m1fz  12257  fz0to3un2pr  12268  fz0to4untppr  12269  fzctr  12278  fzo0to2pr  12378  fzo0to42pr  12380  2tnp1ge0ge0  12450  flhalf  12451  m1modge3gt1  12537  2txmodxeq0  12550  f13idfv  12620  sq1  12778  expnass  12790  sqrecd  12832  sqoddm1div8  12848  bcn2m1  12931  bcn2p1  12932  4bc2eq6  12936  hashtpg  13074  ccat2s1p2  13207  swrdtrcfv0  13243  swrdtrcfvl  13251  eqwrds3  13501  iseraltlem2  14210  iseraltlem3  14211  climcndslem1  14369  climcnds  14371  bpolydiflem  14573  efgt0  14621  tanval3  14652  cos01bnd  14704  cos01gt0  14709  odd2np1  14852  even2n  14853  oddm1even  14854  oddp1even  14855  oexpneg  14856  mod2eq1n2dvds  14858  2tp1odd  14863  2teven  14866  evend2  14868  oddp1d2  14869  ltoddhalfle  14872  opoe  14874  omoe  14875  opeo  14876  omeo  14877  m1expo  14879  m1exp1  14880  nn0o  14886  z0even  14890  n2dvds1  14891  z2even  14893  n2dvds3  14894  z4even  14895  4dvdseven  14896  sumeven  14897  flodddiv4  14924  bits0e  14938  bits0o  14939  bitsp1e  14941  bitsp1o  14942  bitsfzo  14944  bitsmod  14945  bitscmp  14947  bitsinv1lem  14950  bitsinv1  14951  6gcd4e2  15042  3lcm2e6woprm  15115  lcmf2a3a4e12  15147  isprm3  15183  dvdsnprmd  15190  2prm  15192  3prm  15193  oddprmge3  15199  isprm7  15207  divgcdodd  15209  oddprm  15302  pythagtriplem4  15311  pythagtriplem11  15317  pythagtriplem13  15319  iserodd  15327  prmgaplem3  15544  prmgaplem7  15548  dec2dvds  15554  prmlem0  15599  4001lem1  15635  psgnunilem4  17689  efgredleme  17928  lt6abl  18068  znidomb  19677  chfacfscmulfsupp  20431  chfacfpmmulfsupp  20435  minveclem2  22950  minveclem3  22953  pjthlem1  22961  dyaddisjlem  23114  mbfi1fseqlem5  23237  iblcnlem1  23305  dvexp3  23490  aaliou3lem6  23852  tanregt0  24034  efif1olem4  24040  tanarg  24114  cubic2  24320  asinlem3  24343  atantayl2  24410  cxp2limlem  24447  lgamgulmlem3  24502  lgamgulmlem4  24503  basellem2  24553  basellem3  24554  basellem4  24555  basellem5  24556  basellem8  24559  basellem9  24560  ppisval  24575  ppiprm  24622  ppinprm  24623  chtprm  24624  chtnprm  24625  chtdif  24629  ppidif  24634  ppi1  24635  cht1  24636  cht3  24644  ppieq0  24647  ppiublem1  24672  ppiublem2  24673  chpeq0  24678  chtub  24682  chpval2  24688  chpub  24690  mersenne  24697  perfect1  24698  perfectlem1  24699  perfectlem2  24700  bposlem1  24754  bposlem2  24755  bposlem3  24756  bposlem5  24758  bposlem6  24759  lgslem1  24767  lgsdir2lem2  24796  lgsdir2lem3  24797  lgsdir2  24800  lgsqr  24821  gausslemma2dlem0i  24834  gausslemma2dlem1a  24835  gausslemma2dlem5a  24840  gausslemma2dlem5  24841  gausslemma2dlem6  24842  gausslemma2dlem7  24843  gausslemma2d  24844  lgseisenlem1  24845  lgseisenlem2  24846  lgseisenlem3  24847  lgseisenlem4  24848  lgsquadlem1  24850  lgsquadlem2  24851  lgsquad2lem1  24854  lgsquad2lem2  24855  lgsquad2  24856  lgsquad3  24857  m1lgs  24858  2lgslem1a1  24859  2lgslem1a2  24860  2lgslem1b  24862  2lgslem2  24865  2lgslem3b1  24871  2lgslem3c1  24872  2lgs2  24875  2lgs  24877  2lgsoddprmlem2  24879  2lgsoddprmlem3  24884  2lgsoddprm  24886  2sqblem  24901  chebbnd1lem1  24903  chebbnd1lem3  24905  chebbnd1  24906  dchrisum0lem1a  24920  dchrvmasumiflem1  24935  dchrisum0flblem1  24942  dchrisum0flblem2  24943  dchrisum0lem1b  24949  dchrisum0lem1  24950  dchrisum0lem2a  24951  dchrisum0lem2  24952  dchrisum0lem3  24953  mulog2sumlem2  24969  pntlemd  25028  pntlema  25030  pntlemb  25031  pntlemh  25033  pntlemr  25036  pntlemf  25039  pntlemo  25041  istrkg2ld  25104  istrkg3ld  25105  axlowdimlem3  25570  axlowdimlem6  25573  axlowdimlem16  25583  axlowdimlem17  25584  axlowdim  25587  usgraexmpldifpr  25722  usgraexmplef  25723  cusgrasizeindb1  25794  2wlklemC  25880  2trllemD  25881  2trllemG  25882  wlkntrllem2  25884  constr2spthlem1  25918  2pthon  25926  usgra2adedgwlkonALT  25938  usgra2wlkspthlem2  25942  3v3e3cycl1  25966  constr3lem4  25969  constr3trllem2  25973  constr3trllem3  25974  constr3trllem5  25976  constr3pthlem1  25977  constr3pthlem2  25978  4cycl4v4e  25988  4cycl4dv4e  25990  clwlkisclwwlklem2a1  26101  clwlkisclwwlklem2fv1  26104  clwlkisclwwlklem2fv2  26105  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  clwwisshclwwlem  26128  eupath2lem3  26300  eupath2  26301  frgrawopreglem2  26366  extwwlkfablem2  26399  numclwwlkovf2ex  26407  numclwwlk2lem1  26423  numclwlk2lem2f  26424  frgrareggt1  26437  ex-fl  26490  ex-mod  26492  ex-hash  26496  ex-dvds  26499  ex-ind-dvds  26504  minvecolem3  26950  pjhthlem1  27468  znsqcld  28734  2sqmod  28813  archirngz  28908  archiabllem2c  28914  lmat22det  29050  dya2ub  29493  dya2icoseg  29500  oddpwdc  29577  eulerpartlemd  29589  eulerpartlemt  29594  ballotlem2  29711  signslema  29799  nn0prpwlem  31321  knoppndvlem2  31508  knoppndvlem8  31514  poimirlem25  32428  poimirlem26  32429  poimirlem27  32430  poimirlem28  32431  acongrep  36389  acongeq  36392  jm2.18  36397  jm2.22  36404  jm2.23  36405  jm2.20nn  36406  jm2.26a  36409  jm2.26  36411  jm2.15nn0  36412  jm2.27a  36414  jm2.27c  36416  rmydioph  36423  jm3.1lem1  36426  jm3.1lem3  36428  expdiophlem1  36430  expdiophlem2  36431  hashnzfz2  37366  sumnnodd  38521  coskpi2  38573  cosknegpi  38576  dvrecg  38624  dvdivbd  38637  stoweidlem26  38743  wallispilem4  38785  wallispi2lem1  38788  wallispi2lem2  38789  wallispi2  38790  stirlinglem1  38791  stirlinglem3  38793  stirlinglem7  38797  stirlinglem8  38798  stirlinglem10  38800  stirlinglem11  38801  stirlinglem15  38805  dirkertrigeqlem1  38815  dirkercncflem2  38821  fourierdlem54  38877  fourierdlem56  38879  fourierdlem57  38880  fourierdlem102  38925  fourierdlem114  38937  fourierswlem  38947  fouriersw  38948  smfmullem4  39503  fmtnorec1  39812  goldbachthlem2  39821  odz2prm2pw  39838  fmtnoprmfac1  39840  fmtnoprmfac2lem1  39841  fmtnoprmfac2  39842  fmtno4prmfac  39847  31prm  39875  sfprmdvdsmersenne  39883  lighneallem1  39885  lighneallem4a  39888  lighneallem4b  39889  lighneallem4  39890  proththdlem  39893  proththd  39894  3exp4mod41  39896  41prothprmlem2  39898  m1expevenALTV  39923  dfeven2  39925  oexpnegALTV  39951  oexpnegnz  39952  2evenALTV  39966  2noddALTV  39967  nn0o1gt2ALTV  39968  nnpw2evenALTV  39974  perfectALTVlem1  39989  perfectALTVlem2  39990  sgoldbalt  40028  nnsum4primesodd  40037  nnsum4primesoddALTV  40038  wtgoldbnnsum4prm  40043  bgoldbnnsum3prm  40045  pfxtrcfv0  40090  pfxtrcfvl  40093  cusgrsizeindb1  40688  pthdlem1  40994  clwlkclwwlklem2a1  41223  clwlkclwwlklem2fv1  41226  clwlkclwwlklem2fv2  41227  clwlkclwwlklem2a4  41228  clwlkclwwlklem2a  41229  clwwisshclwwslem  41256  eupth2lem3lem3  41420  eupth2lemb  41427  konigsberglem5  41448  av-extwwlkfablem2  41532  av-numclwwlkovf2ex  41539  av-numclwwlk2lem1  41554  av-numclwlk2lem2f  41555  av-frgrareggt1  41569  2even  41745  nn0le2is012  41960  zlmodzxzequa  42101  zlmodzxznm  42102  zlmodzxzequap  42104  zlmodzxzldeplem1  42105  zlmodzxzldeplem3  42107  zlmodzxzldep  42109  ldepsnlinclem1  42110  ldepsnlinc  42113  pw2m1lepw2m1  42126  fldivexpfllog2  42179  nnlog2ge0lt1  42180  logbpw2m1  42181  fllog2  42182  blennnelnn  42190  blenpw2  42192  nnpw2blenfzo  42195  blennnt2  42203  nnolog2flm1  42204  dig2nn0ld  42218  dig2nn1st  42219  0dig2pr01  42224  0dig2nn0o  42227
  Copyright terms: Public domain W3C validator