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

Theorem 2nn 10693
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 10594 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10547 . . 3  |-  1  e.  NN
3 peano2nn 10548 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2551 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767  (class class class)co 6284   1c1 9493    + caddc 9495   NNcn 10536   2c2 10585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-1cn 9550
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537  df-2 10594
This theorem is referenced by:  3nn  10694  2nn0  10812  2z  10896  uz3m2nn  11124  ige2m1fz1  11766  sqeq0  12200  expmulnbnd  12266  sqeq0d  12277  faclbnd5  12344  bcn2  12365  f1oun2prg  12828  wwlktovf  12857  climcndslem1  13624  climcndslem2  13625  climcnds  13626  harmonic  13633  geo2sum  13645  geo2lim  13647  ege2le3  13687  ef01bndlem  13780  egt2lt3  13800  nthruc  13845  bits0o  13939  bitsp1  13940  bitsfzolem  13943  bitsfzo  13944  bitsmod  13945  bitsfi  13946  bitscmp  13947  bitsinv1lem  13950  bitsinv1  13951  2ebits  13956  bitsinvp1  13958  sadcaddlem  13966  sadadd3  13970  sadaddlem  13975  sadasslem  13979  bitsres  13982  bitsuz  13983  bitsshft  13984  smumullem  14001  smumul  14002  sqgcd  14055  isprm3  14085  3prm  14093  pythagtriplem4  14202  iserodd  14218  prmreclem3  14295  prmreclem5  14297  prmreclem6  14298  4sqlem12  14333  vdwlem3  14360  vdwlem9  14366  vdwlem10  14367  dec2dvds  14408  dec5nprm  14411  dec2nprm  14412  2expltfac  14435  4nprm  14448  5prm  14452  6nprm  14453  7prm  14454  8nprm  14455  10nprm  14457  11prm  14458  17prm  14460  23prm  14462  37prm  14464  43prm  14465  83prm  14466  139prm  14467  163prm  14468  317prm  14469  631prm  14470  1259lem1  14471  1259lem2  14472  1259lem3  14473  1259lem4  14474  1259lem5  14475  1259prm  14476  2503lem1  14477  2503lem2  14478  2503lem3  14479  2503prm  14480  4001lem1  14481  4001lem2  14482  4001lem3  14483  4001lem4  14484  4001prm  14485  plusgndx  14589  plusgid  14590  grpstr  14594  grpbase  14595  grpplusg  14596  ressplusg  14597  rngstr  14602  lmodstr  14619  topgrpstr  14644  dsndx  14658  dsid  14659  odrngstr  14662  ressds  14669  imasvalstr  14707  pmtrprfval  16318  pmtrprfvalrn  16319  psgnunilem2  16326  psgnprfval  16352  psgnprfval1  16353  lt6abl  16700  mgpds  16953  oppradd  17080  sraaddg  17625  srads  17632  opsrplusg  17943  cnfldstr  18221  zlmplusg  18351  znadd  18374  m2detleiblem1  18921  m2detleiblem5  18922  m2detleiblem6  18923  m2detleiblem3  18926  m2detleiblem4  18927  m2detleib  18928  tmslem  20748  tngplusg  20919  ovollb2lem  21662  ovolunlem1a  21670  ovolunlem1  21671  ovoliunlem1  21676  ovoliunlem3  21678  dyadf  21763  dyadovol  21765  dyadss  21766  dyaddisjlem  21767  dyadmaxlem  21769  opnmbllem  21773  mbfi1fseqlem1  21885  mbfi1fseqlem3  21887  mbfi1fseqlem4  21888  mbfi1fseqlem5  21889  mbfi1fseqlem6  21890  dveflem  22143  aaliou3lem9  22508  dcubic1lem  22930  dcubic2  22931  mcubic  22934  quartlem1  22944  quartlem2  22945  basellem1  23110  basellem2  23111  basellem3  23112  basellem4  23113  basellem5  23114  basellem6  23115  basellem7  23116  basellem8  23117  basellem9  23118  ppiltx  23207  prmorcht  23208  1sgm2ppw  23231  ppiublem1  23233  ppiub  23235  chtlepsi  23237  chtublem  23242  chpub  23251  mersenne  23258  perfect1  23259  perfectlem1  23260  perfectlem2  23261  perfect  23262  pcbcctr  23307  bclbnd  23311  bposlem1  23315  bposlem2  23316  bposlem3  23317  bposlem4  23318  bposlem5  23319  bposlem6  23320  bposlem8  23322  lgsdir2lem2  23355  lgsqr  23377  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem3  23382  lgseisenlem4  23383  lgsquadlem1  23385  lgsquadlem2  23386  lgsquad2lem2  23390  2sqlem3  23397  2sqlem8  23403  chebbnd1lem1  23410  chebbnd1lem3  23412  chtppilimlem1  23414  logdivsum  23474  log2sumbnd  23485  pntlemd  23535  pntlema  23537  pntlemb  23538  pntlemf  23546  pntlemo  23548  ostth2lem1  23559  trkgstr  23596  ttgplusg  23885  ttgds  23888  axlowdimlem5  23953  axlowdimlem6  23954  axlowdimlem16  23964  axlowdimlem17  23965  axlowdim  23968  eengstr  23987  usgraexmpl  24105  cusgrasizeindb0  24174  usgrcyclnl2  24345  eupath2lem3  24683  konigsberg  24691  ex-xp  24862  ex-cnv  24863  ex-rn  24866  resvplusg  27514  oddpwdc  27961  eulerpartlemt  27978  eulerpartlemgh  27985  fib0  28006  fib1  28007  fib3  28010  signswbase  28179  signswplusg  28180  zetacvg  28225  lgamgulmlem4  28242  problem5  28526  opnmbllem0  29655  mblfinlem1  29656  dvasin  29708  areacirclem1  29712  heiborlem3  29940  heiborlem5  29942  heiborlem6  29943  heiborlem7  29944  heiborlem8  29945  heibor  29948  rmxypos  30517  ltrmynn0  30518  jm2.17a  30530  jm2.17b  30531  jm2.17c  30532  acongrep  30550  acongeq  30553  jm2.27a  30579  jm2.27c  30581  rmydioph  30588  rmxdioph  30590  expdiophlem2  30596  expdioph  30597  frlmpwfi  30678  hashnzfz2  30854  lhe4.4ex1a  30862  wallispilem5  31397  wallispi2lem1  31399  wallispi2  31401  stirlinglem3  31404  stirlinglem8  31409  stirlinglem10  31411  stirlinglem15  31416  dirkertrigeqlem3  31428  fouriersw  31560  usgra2pthspth  31846  usgra2pthlem1  31848  hlhilsplus  36758
  Copyright terms: Public domain W3C validator