MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2nn Structured version   Unicode version

Theorem 2nn 10718
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
Assertion
Ref Expression
2nn  |-  2  e.  NN

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 10619 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10571 . . 3  |-  1  e.  NN
3 peano2nn 10572 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2502 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872  (class class class)co 6249   1c1 9491    + caddc 9493   NNcn 10560   2c2 10610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-1cn 9548
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-om 6651  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-nn 10561  df-2 10619
This theorem is referenced by:  3nn  10719  2nn0  10837  2z  10920  uz3m2nn  11152  ige2m1fz1  11834  sqeq0  12289  expmulnbnd  12354  sqeq0d  12365  faclbnd5  12433  bcn2  12454  f1oun2prg  12946  wwlktovf  12975  climcndslem1  13850  climcndslem2  13851  climcnds  13852  harmonic  13860  geo2sum  13872  geo2lim  13874  ege2le3  14087  ef01bndlem  14181  egt2lt3  14201  nthruc  14246  bits0o  14346  bitsp1  14347  bitsfzolem  14350  bitsfzolemOLD  14351  bitsfzo  14352  bitsmod  14353  bitsfi  14354  bitscmp  14355  bitsinv1lem  14358  bitsinv1  14359  2ebits  14364  bitsinvp1  14366  sadcaddlem  14374  sadadd3  14378  sadaddlem  14383  sadasslem  14387  bitsres  14390  bitsuz  14391  bitsshft  14392  smumullem  14409  smumul  14410  sqgcd  14469  3lcm2e6woprm  14523  3prm  14584  3lcm2e6  14624  pythagtriplem4  14712  iserodd  14728  prmreclem3  14805  prmreclem5  14807  prmreclem6  14808  4sqlem12  14843  vdwlem3  14876  vdwlem9  14882  vdwlem10  14883  prmo2  14941  dec2dvds  14978  dec5nprm  14981  dec2nprm  14982  2expltfac  15006  4nprm  15019  5prm  15023  6nprm  15024  7prm  15025  8nprm  15026  10nprm  15028  11prm  15029  17prm  15031  23prm  15033  37prm  15035  43prm  15036  83prm  15037  139prm  15038  163prm  15039  317prm  15040  631prm  15041  1259lem1  15045  1259lem2  15046  1259lem3  15047  1259lem4  15048  1259lem5  15049  1259prm  15050  2503lem1  15051  2503lem2  15052  2503lem3  15053  2503prm  15054  4001lem1  15055  4001lem2  15056  4001lem3  15057  4001lem4  15058  4001prm  15059  plusgndx  15167  plusgid  15168  grpstr  15179  grpbase  15180  grpplusg  15181  ressplusg  15182  rngstr  15187  lmodstr  15204  topgrpstr  15229  dsndx  15243  dsid  15244  odrngstr  15247  ressds  15254  imasvalstr  15293  pmtrprfvalrn  17072  psgnunilem2  17079  psgnprfval  17105  psgnprfval1  17106  mgpds  17676  oppradd  17801  sraaddg  18345  srads  18352  opsrplusg  18646  cnfldstr  18915  zlmplusg  19032  znadd  19053  m2detleiblem1  19591  m2detleiblem5  19592  m2detleiblem6  19593  m2detleiblem3  19596  m2detleiblem4  19597  m2detleib  19598  tmslem  21439  tngplusg  21592  ovollb2lem  22383  ovolunlem1a  22391  ovolunlem1  22392  ovoliunlem1  22397  ovoliunlem3  22399  dyadf  22491  dyadovol  22493  dyadss  22494  dyaddisjlem  22495  dyadmaxlem  22497  opnmbllem  22501  mbfi1fseqlem1  22615  mbfi1fseqlem3  22617  mbfi1fseqlem4  22618  mbfi1fseqlem5  22619  mbfi1fseqlem6  22620  dveflem  22873  aaliou3lem9  23248  dcubic1lem  23711  dcubic2  23712  mcubic  23715  quartlem1  23725  quartlem2  23726  zetacvg  23882  lgamgulmlem4  23899  basellem1  23949  basellem2  23950  basellem3  23951  basellem4  23952  basellem5  23953  basellem6  23954  basellem7  23955  basellem8  23956  basellem9  23957  1sgm2ppw  24070  ppiublem1  24072  chtublem  24081  mersenne  24097  perfect1  24098  perfectlem1  24099  perfectlem2  24100  perfect  24101  pcbcctr  24146  bclbnd  24150  bposlem1  24154  bposlem2  24155  bposlem3  24156  bposlem4  24157  bposlem5  24158  bposlem6  24159  bposlem8  24161  lgsdir2lem2  24194  lgsqr  24216  lgseisenlem1  24219  lgseisenlem2  24220  lgseisenlem3  24221  lgseisenlem4  24222  lgsquadlem1  24224  lgsquadlem2  24225  lgsquad2lem2  24229  2sqlem3  24236  2sqlem8  24242  chebbnd1lem1  24249  chebbnd1lem3  24251  logdivsum  24313  log2sumbnd  24324  pntlemd  24374  pntlema  24376  pntlemb  24377  pntlemf  24385  pntlemo  24387  ostth2lem1  24398  trkgstr  24434  ttgplusg  24850  ttgds  24853  axlowdimlem6  24919  eengstr  24952  usgraexmplef  25070  cusgrasizeindb0  25140  usgrcyclnl2  25311  eupath2lem3  25649  konigsberg  25657  ex-xp  25828  ex-cnv  25829  ex-rn  25832  resvplusg  28548  lmat22e11  28596  lmat22e12  28597  lmat22e21  28598  lmat22e22  28599  lmat22det  28600  oddpwdc  29139  eulerpartlemt  29156  eulerpartlemgh  29163  fib0  29184  fib1  29185  fib3  29188  problem5  30253  bcprod  30325  opnmbllem0  31883  mblfinlem1  31884  dvasin  31935  areacirclem1  31939  heiborlem3  32052  heiborlem5  32054  heiborlem6  32055  heiborlem7  32056  heiborlem8  32057  heibor  32060  hlhilsplus  35423  jm2.17a  35723  jm2.17b  35724  jm2.17c  35725  acongrep  35743  acongeq  35746  jm2.27a  35773  jm2.27c  35775  rmydioph  35782  rmxdioph  35784  expdiophlem2  35790  expdioph  35791  frlmpwfi  35869  amgm2d  36563  hashnzfz2  36583  lhe4.4ex1a  36591  wallispilem5  37814  wallispi2lem1  37816  wallispi2  37818  stirlinglem3  37821  stirlinglem8  37826  stirlinglem10  37828  stirlinglem15  37833  dirkertrigeqlem3  37845  fouriersw  37978  hoicvrrex  38225  ovnsubaddlem1  38239  ovnsubaddlem2  38240  elmod2  38537  iseven5  38607  oddprmALTV  38629  perfectALTVlem1  38656  perfectALTVlem2  38657  perfectALTV  38658  nnsum3primes4  38696  nnsum3primesgbe  38700  nnsum4primesevenALTV  38709  bgoldbtbndlem1  38713  tgblthelfgott  38721  proththdlem  38726  proththd  38727  pfx2  38766  cusgrsizeindb0  39248  usgra2pthspth  39266  usgra2pthlem1  39268  pw2m1lepw2m1  39921  nnpw2even  39939  logbpw2m1  39981  blenpw2  39992  nnpw2pmod  39997  blen2  39999  nnpw2p  40000  nnpw2pb  40001  blennnt2  40003  nnolog2flm1  40004  dig2nn1st  40019  0dig2pr01  40024  dig2nn0  40025  0dig2nn0e  40026  0dig2nn0o  40027  dig2bits  40028  dignn0flhalflem1  40029  dignn0ehalf  40031  dignn0flhalf  40032  nn0sumshdiglemA  40033  nn0sumshdiglemB  40034  nn0sumshdiglem1  40035  nn0sumshdiglem2  40036  nn0mullong  40039
  Copyright terms: Public domain W3C validator