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

Theorem 2nn 10466
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 10367 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10320 . . 3  |-  1  e.  NN
3 peano2nn 10321 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2503 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755  (class class class)co 6080   1c1 9270    + caddc 9272   NNcn 10309   2c2 10358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-1cn 9327
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10310  df-2 10367
This theorem is referenced by:  3nn  10467  2nn0  10583  2z  10665  ige2m1fz1  11459  sqeq0  11913  expmulnbnd  11979  sqeq0d  11990  faclbnd5  12057  bcn2  12078  f1oun2prg  12510  climcndslem1  13294  climcndslem2  13295  climcnds  13296  harmonic  13303  geo2sum  13315  geo2lim  13317  ege2le3  13357  ef01bndlem  13450  egt2lt3  13470  nthruc  13515  bits0o  13608  bitsp1  13609  bitsfzolem  13612  bitsfzo  13613  bitsmod  13614  bitsfi  13615  bitscmp  13616  bitsinv1lem  13619  bitsinv1  13620  2ebits  13625  bitsinvp1  13627  sadcaddlem  13635  sadadd3  13639  sadaddlem  13644  sadasslem  13648  bitsres  13651  bitsuz  13652  bitsshft  13653  smumullem  13670  smumul  13671  sqgcd  13724  isprm3  13754  3prm  13762  pythagtriplem4  13868  iserodd  13884  prmreclem3  13961  prmreclem5  13963  prmreclem6  13964  4sqlem12  13999  vdwlem3  14026  vdwlem9  14032  vdwlem10  14033  dec2dvds  14074  dec5nprm  14077  dec2nprm  14078  2expltfac  14101  4nprm  14114  5prm  14118  6nprm  14119  7prm  14120  8nprm  14121  10nprm  14123  11prm  14124  17prm  14126  23prm  14128  37prm  14130  43prm  14131  83prm  14132  139prm  14133  163prm  14134  317prm  14135  631prm  14136  1259lem1  14137  1259lem2  14138  1259lem3  14139  1259lem4  14140  1259lem5  14141  1259prm  14142  2503lem1  14143  2503lem2  14144  2503lem3  14145  2503prm  14146  4001lem1  14147  4001lem2  14148  4001lem3  14149  4001lem4  14150  4001prm  14151  plusgndx  14254  plusgid  14255  grpstr  14259  grpbase  14260  grpplusg  14261  ressplusg  14262  rngstr  14267  lmodstr  14284  topgrpstr  14309  dsndx  14323  dsid  14324  odrngstr  14327  ressds  14334  imasvalstr  14372  pmtrprfval  15972  pmtrprfvalrn  15973  psgnunilem2  15980  psgnprfval  16004  psgnprfval1  16005  lt6abl  16350  mgpds  16574  oppradd  16655  sraaddg  17181  srads  17188  opsrplusg  17492  cnfldstr  17663  zlmplusg  17791  znadd  17814  m2detleiblem1  18271  m2detleiblem5  18272  m2detleiblem6  18273  m2detleiblem3  18276  m2detleiblem4  18277  m2detleib  18278  tmslem  19898  tngplusg  20069  ovollb2lem  20812  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliunlem3  20828  dyadf  20912  dyadovol  20914  dyadss  20915  dyaddisjlem  20916  dyadmaxlem  20918  opnmbllem  20922  mbfi1fseqlem1  21034  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1fseqlem6  21039  dveflem  21292  aaliou3lem9  21700  dcubic1lem  22122  dcubic2  22123  mcubic  22126  quartlem1  22136  quartlem2  22137  basellem1  22302  basellem2  22303  basellem3  22304  basellem4  22305  basellem5  22306  basellem6  22307  basellem7  22308  basellem8  22309  basellem9  22310  ppiltx  22399  prmorcht  22400  1sgm2ppw  22423  ppiublem1  22425  ppiub  22427  chtlepsi  22429  chtublem  22434  chpub  22443  mersenne  22450  perfect1  22451  perfectlem1  22452  perfectlem2  22453  perfect  22454  pcbcctr  22499  bclbnd  22503  bposlem1  22507  bposlem2  22508  bposlem3  22509  bposlem4  22510  bposlem5  22511  bposlem6  22512  bposlem8  22514  lgsdir2lem2  22547  lgsqr  22569  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem3  22574  lgseisenlem4  22575  lgsquadlem1  22577  lgsquadlem2  22578  lgsquad2lem2  22582  2sqlem3  22589  2sqlem8  22595  chebbnd1lem1  22602  chebbnd1lem3  22604  chtppilimlem1  22606  logdivsum  22666  log2sumbnd  22677  pntlemd  22727  pntlema  22729  pntlemb  22730  pntlemf  22738  pntlemo  22740  ostth2lem1  22751  trkgstr  22789  ttgplusg  22946  ttgds  22949  axlowdimlem5  23014  axlowdimlem6  23015  axlowdimlem16  23025  axlowdimlem17  23026  axlowdim  23029  eengstr  23048  usgraexmpl  23141  cusgrasizeindb0  23200  usgrcyclnl2  23349  eupath2lem3  23422  konigsberg  23430  ex-xp  23465  ex-cnv  23466  ex-rn  23469  resvplusg  26154  oddpwdc  26584  eulerpartlemt  26601  eulerpartlemgh  26608  fib0  26629  fib1  26630  fib3  26633  signswbase  26802  signswplusg  26803  zetacvg  26848  lgamgulmlem4  26865  problem5  27149  opnmbllem0  28268  mblfinlem1  28269  dvasin  28321  areacirclem1  28325  heiborlem3  28553  heiborlem5  28555  heiborlem6  28556  heiborlem7  28557  heiborlem8  28558  heibor  28561  rmxypos  29132  ltrmynn0  29133  jm2.17a  29145  jm2.17b  29146  jm2.17c  29147  acongrep  29165  acongeq  29168  jm2.27a  29196  jm2.27c  29198  rmydioph  29205  rmxdioph  29207  expdiophlem2  29213  expdioph  29214  frlmpwfi  29295  lhe4.4ex1a  29445  wallispilem5  29707  wallispi2lem1  29709  wallispi2  29711  stirlinglem3  29714  stirlinglem8  29719  stirlinglem10  29721  stirlinglem15  29726  uz3m2nn  30038  wwlktovf  30094  usgra2pthspth  30138  usgra2pthlem1  30143  hlhilsplus  35158
  Copyright terms: Public domain W3C validator