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

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

Proof of Theorem 2z
StepHypRef Expression
1 2nn 11062 . 2 2 ∈ ℕ
21nnzi 11278 1 2 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  2c2 10947  cz 11254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-z 11255
This theorem is referenced by:  nn0lt2  11317  zadd2cl  11366  uzuzle23  11605  2eluzge1  11610  eluz2b1  11635  nn01to3  11657  nn0ge2m1nnALT  11658  ige2m1fz  12299  fz0to3un2pr  12310  fz0to4untppr  12311  fzctr  12320  fzo0to2pr  12420  fzo0to42pr  12422  2tnp1ge0ge0  12492  flhalf  12493  m1modge3gt1  12579  2txmodxeq0  12592  f13idfv  12662  sq1  12820  expnass  12832  sqrecd  12874  sqoddm1div8  12890  bcn2m1  12973  bcn2p1  12974  4bc2eq6  12978  hashtpg  13121  ccat2s1p2  13258  swrdtrcfv0  13294  swrdtrcfvl  13302  eqwrds3  13552  iseraltlem2  14261  iseraltlem3  14262  climcndslem1  14420  climcnds  14422  bpolydiflem  14624  efgt0  14672  tanval3  14703  cos01bnd  14755  cos01gt0  14760  odd2np1  14903  even2n  14904  oddm1even  14905  oddp1even  14906  oexpneg  14907  mod2eq1n2dvds  14909  2tp1odd  14914  2teven  14917  evend2  14919  oddp1d2  14920  ltoddhalfle  14923  opoe  14925  omoe  14926  opeo  14927  omeo  14928  m1expo  14930  m1exp1  14931  nn0o  14937  z0even  14941  n2dvds1  14942  z2even  14944  n2dvds3  14945  z4even  14946  4dvdseven  14947  sumeven  14948  flodddiv4  14975  bits0e  14989  bits0o  14990  bitsp1e  14992  bitsp1o  14993  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  bitsinv1  15002  6gcd4e2  15093  3lcm2e6woprm  15166  lcmf2a3a4e12  15198  isprm3  15234  dvdsnprmd  15241  2prm  15243  3prm  15244  oddprmge3  15250  isprm7  15258  divgcdodd  15260  oddprm  15353  pythagtriplem4  15362  pythagtriplem11  15368  pythagtriplem13  15370  iserodd  15378  prmgaplem3  15595  prmgaplem7  15599  dec2dvds  15605  prmlem0  15650  4001lem1  15686  psgnunilem4  17740  efgredleme  17979  lt6abl  18119  zringndrg  19657  znidomb  19729  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  minveclem2  23005  minveclem3  23008  pjthlem1  23016  dyaddisjlem  23169  mbfi1fseqlem5  23292  iblcnlem1  23360  dvexp3  23545  aaliou3lem6  23907  tanregt0  24089  efif1olem4  24095  tanarg  24169  cubic2  24375  asinlem3  24398  atantayl2  24465  cxp2limlem  24502  lgamgulmlem3  24557  lgamgulmlem4  24558  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem8  24614  basellem9  24615  ppisval  24630  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  chtdif  24684  ppidif  24689  ppi1  24690  cht1  24691  cht3  24699  ppieq0  24702  ppiublem1  24727  ppiublem2  24728  chpeq0  24733  chtub  24737  chpval2  24743  chpub  24745  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgslem1  24822  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsdir2  24855  lgsqr  24876  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  gausslemma2dlem5a  24895  gausslemma2dlem5  24896  gausslemma2dlem6  24897  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem1  24909  lgsquad2lem2  24910  lgsquad2  24911  lgsquad3  24912  m1lgs  24913  2lgslem1a1  24914  2lgslem1a2  24915  2lgslem1b  24917  2lgslem2  24920  2lgslem3b1  24926  2lgslem3c1  24927  2lgs2  24930  2lgs  24932  2lgsoddprmlem2  24934  2lgsoddprmlem3  24939  2lgsoddprm  24941  2sqblem  24956  chebbnd1lem1  24958  chebbnd1lem3  24960  chebbnd1  24961  dchrisum0lem1a  24975  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  mulog2sumlem2  25024  pntlemd  25083  pntlema  25085  pntlemb  25086  pntlemh  25088  pntlemr  25091  pntlemf  25094  pntlemo  25096  istrkg2ld  25159  istrkg3ld  25160  axlowdimlem3  25624  axlowdimlem6  25627  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  usgraexmpldifpr  25928  usgraexmplef  25929  cusgrasizeindb1  26000  2wlklemC  26086  2trllemD  26087  2trllemG  26088  wlkntrllem2  26090  constr2spthlem1  26124  2pthon  26132  usgra2adedgwlkonALT  26144  usgra2wlkspthlem2  26148  3v3e3cycl1  26172  constr3lem4  26175  constr3trllem2  26179  constr3trllem3  26180  constr3trllem5  26182  constr3pthlem1  26183  constr3pthlem2  26184  4cycl4v4e  26194  4cycl4dv4e  26196  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwisshclwwlem  26334  eupath2lem3  26506  eupath2  26507  frgrawopreglem2  26572  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlk2lem1  26629  numclwlk2lem2f  26630  frgrareggt1  26643  ex-fl  26696  ex-mod  26698  ex-hash  26702  ex-dvds  26705  ex-ind-dvds  26710  minvecolem3  27116  pjhthlem1  27634  znsqcld  28900  2sqmod  28979  archirngz  29074  archiabllem2c  29080  lmat22det  29216  dya2ub  29659  dya2icoseg  29666  oddpwdc  29743  eulerpartlemd  29755  eulerpartlemt  29760  ballotlem2  29877  signslema  29965  nn0prpwlem  31487  knoppndvlem2  31674  knoppndvlem8  31680  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  acongrep  36565  acongeq  36568  jm2.18  36573  jm2.22  36580  jm2.23  36581  jm2.20nn  36582  jm2.26a  36585  jm2.26  36587  jm2.15nn0  36588  jm2.27a  36590  jm2.27c  36592  rmydioph  36599  jm3.1lem1  36602  jm3.1lem3  36604  expdiophlem1  36606  expdiophlem2  36607  hashnzfz2  37542  sumnnodd  38697  coskpi2  38749  cosknegpi  38752  dvrecg  38800  dvdivbd  38813  stoweidlem26  38919  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem15  38981  dirkertrigeqlem1  38991  dirkercncflem2  38997  fourierdlem54  39053  fourierdlem56  39055  fourierdlem57  39056  fourierdlem102  39101  fourierdlem114  39113  fourierswlem  39123  fouriersw  39124  smfmullem4  39679  fmtnorec1  39987  goldbachthlem2  39996  odz2prm2pw  40013  fmtnoprmfac1  40015  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  fmtno4prmfac  40022  31prm  40050  sfprmdvdsmersenne  40058  lighneallem1  40060  lighneallem4a  40063  lighneallem4b  40064  lighneallem4  40065  proththdlem  40068  proththd  40069  3exp4mod41  40071  41prothprmlem2  40073  m1expevenALTV  40098  dfeven2  40100  oexpnegALTV  40126  oexpnegnz  40127  2evenALTV  40141  2noddALTV  40142  nn0o1gt2ALTV  40143  nnpw2evenALTV  40149  perfectALTVlem1  40164  perfectALTVlem2  40165  sgoldbalt  40203  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  pfxtrcfv0  40265  pfxtrcfvl  40268  cusgrsizeindb1  40666  pthdlem1  40972  clwlkclwwlklem2a1  41201  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwisshclwwslem  41234  eupth2lem3lem3  41398  eupth2lemb  41405  konigsberglem5  41426  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-frgrareggt1  41547  2even  41723  nn0le2is012  41938  zlmodzxzequa  42079  zlmodzxznm  42080  zlmodzxzequap  42082  zlmodzxzldeplem1  42083  zlmodzxzldeplem3  42085  zlmodzxzldep  42087  ldepsnlinclem1  42088  ldepsnlinc  42091  pw2m1lepw2m1  42104  fldivexpfllog2  42157  nnlog2ge0lt1  42158  logbpw2m1  42159  fllog2  42160  blennnelnn  42168  blenpw2  42170  nnpw2blenfzo  42173  blennnt2  42181  nnolog2flm1  42182  dig2nn0ld  42196  dig2nn1st  42197  0dig2pr01  42202  0dig2nn0o  42205
  Copyright terms: Public domain W3C validator