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

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

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 10089 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10042 . . 3  |-  1  e.  NN
3 peano2nn 10043 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2512 1  |-  2  e.  NN
Colors of variables: wff set class
Syntax hints:    e. wcel 1727  (class class class)co 6110   1c1 9022    + caddc 9024   NNcn 10031   2c2 10080
This theorem is referenced by:  3nn  10165  2nn0  10269  2z  10343  sqeq0  11477  expmulnbnd  11542  sqeq0d  11553  faclbnd5  11620  bcn2  11641  f1oun2prg  11895  climcndslem1  12660  climcndslem2  12661  climcnds  12662  harmonic  12669  geo2sum  12681  geo2lim  12683  efcllem  12711  ege2le3  12723  ef01bndlem  12816  egt2lt3  12836  nthruc  12881  bits0o  12973  bitsp1  12974  bitsfzolem  12977  bitsfzo  12978  bitsmod  12979  bitsfi  12980  bitscmp  12981  bitsinv1lem  12984  bitsinv1  12985  2ebits  12990  bitsinvp1  12992  sadcaddlem  13000  sadadd3  13004  sadaddlem  13009  sadasslem  13013  bitsres  13016  bitsuz  13017  bitsshft  13018  smumullem  13035  smumul  13036  sqgcd  13089  isprm3  13119  3prm  13127  pythagtriplem4  13224  iserodd  13240  prmreclem3  13317  prmreclem5  13319  prmreclem6  13320  4sqlem12  13355  vdwlem3  13382  vdwlem9  13388  vdwlem10  13389  dec2dvds  13430  dec5nprm  13433  dec2nprm  13434  2expltfac  13457  4nprm  13458  5prm  13462  6nprm  13463  7prm  13464  8nprm  13465  10nprm  13467  11prm  13468  17prm  13470  23prm  13472  37prm  13474  43prm  13475  83prm  13476  139prm  13477  163prm  13478  317prm  13479  631prm  13480  1259lem1  13481  1259lem2  13482  1259lem3  13483  1259lem4  13484  1259lem5  13485  1259prm  13486  2503lem1  13487  2503lem2  13488  2503lem3  13489  2503prm  13490  4001lem1  13491  4001lem2  13492  4001lem3  13493  4001lem4  13494  4001prm  13495  plusgndx  13594  plusgid  13595  grpstr  13599  grpbase  13600  grpplusg  13601  ressplusg  13602  rngstr  13607  lmodstr  13624  topgrpstr  13647  dsndx  13661  dsid  13662  odrngstr  13665  ressds  13672  imasvalstr  13706  lt6abl  15535  mgpds  15689  oppradd  15766  sraaddg  16282  srads  16288  opsrplusg  16571  cnfldstr  16736  zlmplusg  16831  znadd  16852  tmslem  18543  tngplusg  18714  ovollb2lem  19415  ovolunlem1a  19423  ovolunlem1  19424  ovoliunlem1  19429  ovoliunlem3  19431  dyadf  19514  dyadovol  19516  dyadss  19517  dyaddisjlem  19518  dyadmaxlem  19520  opnmbllem  19524  mbfi1fseqlem1  19636  mbfi1fseqlem3  19638  mbfi1fseqlem4  19639  mbfi1fseqlem5  19640  mbfi1fseqlem6  19641  dveflem  19894  aaliou3lem9  20298  dcubic1lem  20714  dcubic2  20715  mcubic  20718  quartlem1  20728  quartlem2  20729  basellem1  20894  basellem2  20895  basellem3  20896  basellem4  20897  basellem5  20898  basellem6  20899  basellem7  20900  basellem8  20901  basellem9  20902  ppiltx  20991  prmorcht  20992  1sgm2ppw  21015  ppiublem1  21017  ppiub  21019  chtlepsi  21021  chtublem  21026  chpub  21035  mersenne  21042  perfect1  21043  perfectlem1  21044  perfectlem2  21045  perfect  21046  pcbcctr  21091  bclbnd  21095  bposlem1  21099  bposlem2  21100  bposlem3  21101  bposlem4  21102  bposlem5  21103  bposlem6  21104  bposlem8  21106  lgsdir2lem2  21139  lgsqr  21161  lgseisenlem1  21164  lgseisenlem2  21165  lgseisenlem3  21166  lgseisenlem4  21167  lgsquadlem1  21169  lgsquadlem2  21170  lgsquad2lem2  21174  2sqlem3  21181  2sqlem8  21187  chebbnd1lem1  21194  chebbnd1lem3  21196  chtppilimlem1  21198  logdivsum  21258  log2sumbnd  21269  pntlemd  21319  pntlema  21321  pntlemb  21322  pntlemf  21330  pntlemo  21332  ostth2lem1  21343  usgraexmpl  21451  cusgrasizeindb0  21510  usgrcyclnl2  21659  eupath2lem3  21732  konigsberg  21740  ex-xp  21775  ex-cnv  21776  ex-rn  21779  ex-ima  21781  ballotlem2  24777  zetacvg  24830  lgamgulmlem4  24847  axlowdimlem5  25916  axlowdimlem6  25917  axlowdimlem16  25927  axlowdimlem17  25928  axlowdim  25931  opnmbllem0  26278  mblfinlem1  26279  dvreasin  26328  areacirclem1  26330  heiborlem3  26560  heiborlem5  26562  heiborlem6  26563  heiborlem7  26564  heiborlem8  26565  heibor  26568  rabren3dioph  26914  rmxypos  27050  ltrmynn0  27051  jm2.17a  27063  jm2.17b  27064  jm2.17c  27065  acongrep  27083  acongeq  27086  jm2.23  27105  jm2.27a  27114  jm2.27c  27116  rmydioph  27123  rmxdioph  27125  expdiophlem2  27131  expdioph  27132  frlmpwfi  27277  psgnunilem2  27433  lhe4.4ex1a  27561  wallispilem5  27832  wallispi2lem1  27834  wallispi2  27836  stirlinglem3  27839  stirlinglem8  27844  stirlinglem10  27846  stirlinglem15  27851  usgra2pthspth  28367  usgra2pthlem1  28372  hlhilsplus  32839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-1cn 9079
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-recs 6662  df-rdg 6697  df-nn 10032  df-2 10089
  Copyright terms: Public domain W3C validator