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

Theorem 2nn 10122
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 10047 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10000 . . 3  |-  1  e.  NN
3 peano2nn 10001 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 8 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2505 1  |-  2  e.  NN
Colors of variables: wff set class
Syntax hints:    e. wcel 1725  (class class class)co 6072   1c1 8980    + caddc 8982   NNcn 9989   2c2 10038
This theorem is referenced by:  3nn  10123  2nn0  10227  2z  10301  sqeq0  11434  expmulnbnd  11499  sqeq0d  11510  faclbnd5  11577  bcn2  11598  f1oun2prg  11852  climcndslem1  12617  climcndslem2  12618  climcnds  12619  harmonic  12626  geo2sum  12638  geo2lim  12640  efcllem  12668  ege2le3  12680  ef01bndlem  12773  egt2lt3  12793  nthruc  12838  bits0o  12930  bitsp1  12931  bitsfzolem  12934  bitsfzo  12935  bitsmod  12936  bitsfi  12937  bitscmp  12938  bitsinv1lem  12941  bitsinv1  12942  2ebits  12947  bitsinvp1  12949  sadcaddlem  12957  sadadd3  12961  sadaddlem  12966  sadasslem  12970  bitsres  12973  bitsuz  12974  bitsshft  12975  smumullem  12992  smumul  12993  sqgcd  13046  isprm3  13076  3prm  13084  pythagtriplem4  13181  iserodd  13197  prmreclem3  13274  prmreclem5  13276  prmreclem6  13277  4sqlem12  13312  vdwlem3  13339  vdwlem9  13345  vdwlem10  13346  dec2dvds  13387  dec5nprm  13390  dec2nprm  13391  2expltfac  13414  4nprm  13415  5prm  13419  6nprm  13420  7prm  13421  8nprm  13422  10nprm  13424  11prm  13425  17prm  13427  23prm  13429  37prm  13431  43prm  13432  83prm  13433  139prm  13434  163prm  13435  317prm  13436  631prm  13437  1259lem1  13438  1259lem2  13439  1259lem3  13440  1259lem4  13441  1259lem5  13442  1259prm  13443  2503lem1  13444  2503lem2  13445  2503lem3  13446  2503prm  13447  4001lem1  13448  4001lem2  13449  4001lem3  13450  4001lem4  13451  4001prm  13452  plusgndx  13551  plusgid  13552  grpstr  13556  grpbase  13557  grpplusg  13558  ressplusg  13559  rngstr  13564  lmodstr  13581  topgrpstr  13604  dsndx  13618  dsid  13619  odrngstr  13622  ressds  13629  imasvalstr  13663  lt6abl  15492  mgpds  15646  oppradd  15723  sraaddg  16239  srads  16245  opsrplusg  16528  cnfldstr  16693  zlmplusg  16788  znadd  16809  tmslem  18500  tngplusg  18671  ovollb2lem  19372  ovolunlem1a  19380  ovolunlem1  19381  ovoliunlem1  19386  ovoliunlem3  19388  dyadf  19471  dyadovol  19473  dyadss  19474  dyaddisjlem  19475  dyadmaxlem  19477  opnmbllem  19481  mbfi1fseqlem1  19595  mbfi1fseqlem3  19597  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1fseqlem6  19600  dveflem  19851  aaliou3lem9  20255  dcubic1lem  20671  dcubic2  20672  mcubic  20675  quartlem1  20685  quartlem2  20686  basellem1  20851  basellem2  20852  basellem3  20853  basellem4  20854  basellem5  20855  basellem6  20856  basellem7  20857  basellem8  20858  basellem9  20859  ppiltx  20948  prmorcht  20949  1sgm2ppw  20972  ppiublem1  20974  ppiub  20976  chtlepsi  20978  chtublem  20983  chpub  20992  mersenne  20999  perfect1  21000  perfectlem1  21001  perfectlem2  21002  perfect  21003  pcbcctr  21048  bclbnd  21052  bposlem1  21056  bposlem2  21057  bposlem3  21058  bposlem4  21059  bposlem5  21060  bposlem6  21061  bposlem8  21063  lgsdir2lem2  21096  lgsqr  21118  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgseisenlem4  21124  lgsquadlem1  21126  lgsquadlem2  21127  lgsquad2lem2  21131  2sqlem3  21138  2sqlem8  21144  chebbnd1lem1  21151  chebbnd1lem3  21153  chtppilimlem1  21155  logdivsum  21215  log2sumbnd  21226  pntlemd  21276  pntlema  21278  pntlemb  21279  pntlemf  21287  pntlemo  21289  ostth2lem1  21300  usgraexmpl  21408  cusgrasizeindb0  21467  usgrcyclnl2  21616  eupath2lem3  21689  konigsberg  21697  ex-xp  21732  ex-cnv  21733  ex-rn  21736  ex-ima  21738  ballotlem2  24734  zetacvg  24787  lgamgulmlem4  24804  axlowdimlem5  25833  axlowdimlem6  25834  axlowdimlem16  25844  axlowdimlem17  25845  axlowdim  25848  mblfinlem  26190  dvreasin  26226  areacirclem2  26228  areacirclem3  26229  heiborlem3  26459  heiborlem5  26461  heiborlem6  26462  heiborlem7  26463  heiborlem8  26464  heibor  26467  rabren3dioph  26813  rmxypos  26949  ltrmynn0  26950  jm2.17a  26962  jm2.17b  26963  jm2.17c  26964  acongrep  26982  acongeq  26985  jm2.23  27004  jm2.27a  27013  jm2.27c  27015  rmydioph  27022  rmxdioph  27024  expdiophlem2  27030  expdioph  27031  frlmpwfi  27177  psgnunilem2  27333  lhe4.4ex1a  27461  wallispilem5  27732  wallispi2lem1  27734  wallispi2  27736  stirlinglem3  27739  stirlinglem8  27744  stirlinglem10  27746  stirlinglem15  27751  usgra2pthspth  28179  usgra2pthlem1  28184  hlhilsplus  32580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-1cn 9037
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-recs 6624  df-rdg 6659  df-nn 9990  df-2 10047
  Copyright terms: Public domain W3C validator