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

Theorem 2nn 10089
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 10014 . 2  |-  2  =  ( 1  +  1 )
2 1nn 9967 . . 3  |-  1  e.  NN
3 peano2nn 9968 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 8 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2474 1  |-  2  e.  NN
Colors of variables: wff set class
Syntax hints:    e. wcel 1721  (class class class)co 6040   1c1 8947    + caddc 8949   NNcn 9956   2c2 10005
This theorem is referenced by:  3nn  10090  2nn0  10194  2z  10268  sqeq0  11401  expmulnbnd  11466  sqeq0d  11477  faclbnd5  11544  bcn2  11565  f1oun2prg  11819  climcndslem1  12584  climcndslem2  12585  climcnds  12586  harmonic  12593  geo2sum  12605  geo2lim  12607  efcllem  12635  ege2le3  12647  ef01bndlem  12740  egt2lt3  12760  nthruc  12805  bits0o  12897  bitsp1  12898  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitsfi  12904  bitscmp  12905  bitsinv1lem  12908  bitsinv1  12909  2ebits  12914  bitsinvp1  12916  sadcaddlem  12924  sadadd3  12928  sadaddlem  12933  sadasslem  12937  bitsres  12940  bitsuz  12941  bitsshft  12942  smumullem  12959  smumul  12960  sqgcd  13013  isprm3  13043  3prm  13051  pythagtriplem4  13148  iserodd  13164  prmreclem3  13241  prmreclem5  13243  prmreclem6  13244  4sqlem12  13279  vdwlem3  13306  vdwlem9  13312  vdwlem10  13313  dec2dvds  13354  dec5nprm  13357  dec2nprm  13358  2expltfac  13381  4nprm  13382  5prm  13386  6nprm  13387  7prm  13388  8nprm  13389  10nprm  13391  11prm  13392  17prm  13394  23prm  13396  37prm  13398  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  plusgndx  13518  plusgid  13519  grpstr  13523  grpbase  13524  grpplusg  13525  ressplusg  13526  rngstr  13531  lmodstr  13548  topgrpstr  13571  dsndx  13585  dsid  13586  odrngstr  13589  ressds  13596  imasvalstr  13630  lt6abl  15459  mgpds  15613  oppradd  15690  sraaddg  16206  srads  16212  opsrplusg  16495  cnfldstr  16660  zlmplusg  16755  znadd  16776  tmslem  18465  tngplusg  18636  ovollb2lem  19337  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem3  19353  dyadf  19436  dyadovol  19438  dyadss  19439  dyaddisjlem  19440  dyadmaxlem  19442  opnmbllem  19446  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  dveflem  19816  aaliou3lem9  20220  dcubic1lem  20636  dcubic2  20637  mcubic  20640  quartlem1  20650  quartlem2  20651  basellem1  20816  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  ppiltx  20913  prmorcht  20914  1sgm2ppw  20937  ppiublem1  20939  ppiub  20941  chtlepsi  20943  chtublem  20948  chpub  20957  mersenne  20964  perfect1  20965  perfectlem1  20966  perfectlem2  20967  perfect  20968  pcbcctr  21013  bclbnd  21017  bposlem1  21021  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem8  21028  lgsdir2lem2  21061  lgsqr  21083  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem2  21096  2sqlem3  21103  2sqlem8  21109  chebbnd1lem1  21116  chebbnd1lem3  21118  chtppilimlem1  21120  logdivsum  21180  log2sumbnd  21191  pntlemd  21241  pntlema  21243  pntlemb  21244  pntlemf  21252  pntlemo  21254  ostth2lem1  21265  usgraexmpl  21373  cusgrasizeindb0  21432  usgrcyclnl2  21581  eupath2lem3  21654  konigsberg  21662  ex-xp  21697  ex-cnv  21698  ex-rn  21701  ex-ima  21703  ballotlem2  24699  zetacvg  24752  lgamgulmlem4  24769  axlowdimlem5  25789  axlowdimlem6  25790  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  mblfinlem  26143  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  heiborlem3  26412  heiborlem5  26414  heiborlem6  26415  heiborlem7  26416  heiborlem8  26417  heibor  26420  rabren3dioph  26766  rmxypos  26902  ltrmynn0  26903  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  acongrep  26935  acongeq  26938  jm2.23  26957  jm2.27a  26966  jm2.27c  26968  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  frlmpwfi  27130  psgnunilem2  27286  lhe4.4ex1a  27414  wallispilem5  27685  wallispi2lem1  27687  wallispi2  27689  stirlinglem3  27692  stirlinglem8  27697  stirlinglem10  27699  stirlinglem15  27704  usgra2pthspth  28035  usgra2pthlem1  28040  hlhilsplus  32426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-1cn 9004
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-recs 6592  df-rdg 6627  df-nn 9957  df-2 10014
  Copyright terms: Public domain W3C validator