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

Theorem 2nn 10500
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 10401 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10354 . . 3  |-  1  e.  NN
3 peano2nn 10355 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2513 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756  (class class class)co 6112   1c1 9304    + caddc 9306   NNcn 10343   2c2 10392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-1cn 9361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-om 6498  df-recs 6853  df-rdg 6887  df-nn 10344  df-2 10401
This theorem is referenced by:  3nn  10501  2nn0  10617  2z  10699  ige2m1fz1  11494  sqeq0  11951  expmulnbnd  12017  sqeq0d  12028  faclbnd5  12095  bcn2  12116  f1oun2prg  12548  climcndslem1  13333  climcndslem2  13334  climcnds  13335  harmonic  13342  geo2sum  13354  geo2lim  13356  ege2le3  13396  ef01bndlem  13489  egt2lt3  13509  nthruc  13554  bits0o  13647  bitsp1  13648  bitsfzolem  13651  bitsfzo  13652  bitsmod  13653  bitsfi  13654  bitscmp  13655  bitsinv1lem  13658  bitsinv1  13659  2ebits  13664  bitsinvp1  13666  sadcaddlem  13674  sadadd3  13678  sadaddlem  13683  sadasslem  13687  bitsres  13690  bitsuz  13691  bitsshft  13692  smumullem  13709  smumul  13710  sqgcd  13763  isprm3  13793  3prm  13801  pythagtriplem4  13907  iserodd  13923  prmreclem3  14000  prmreclem5  14002  prmreclem6  14003  4sqlem12  14038  vdwlem3  14065  vdwlem9  14071  vdwlem10  14072  dec2dvds  14113  dec5nprm  14116  dec2nprm  14117  2expltfac  14140  4nprm  14153  5prm  14157  6nprm  14158  7prm  14159  8nprm  14160  10nprm  14162  11prm  14163  17prm  14165  23prm  14167  37prm  14169  43prm  14170  83prm  14171  139prm  14172  163prm  14173  317prm  14174  631prm  14175  1259lem1  14176  1259lem2  14177  1259lem3  14178  1259lem4  14179  1259lem5  14180  1259prm  14181  2503lem1  14182  2503lem2  14183  2503lem3  14184  2503prm  14185  4001lem1  14186  4001lem2  14187  4001lem3  14188  4001lem4  14189  4001prm  14190  plusgndx  14293  plusgid  14294  grpstr  14298  grpbase  14299  grpplusg  14300  ressplusg  14301  rngstr  14306  lmodstr  14323  topgrpstr  14348  dsndx  14362  dsid  14363  odrngstr  14366  ressds  14373  imasvalstr  14411  pmtrprfval  16014  pmtrprfvalrn  16015  psgnunilem2  16022  psgnprfval  16046  psgnprfval1  16047  lt6abl  16392  mgpds  16623  oppradd  16744  sraaddg  17282  srads  17289  opsrplusg  17583  cnfldstr  17842  zlmplusg  17972  znadd  17995  m2detleiblem1  18452  m2detleiblem5  18453  m2detleiblem6  18454  m2detleiblem3  18457  m2detleiblem4  18458  m2detleib  18459  tmslem  20079  tngplusg  20250  ovollb2lem  20993  ovolunlem1a  21001  ovolunlem1  21002  ovoliunlem1  21007  ovoliunlem3  21009  dyadf  21093  dyadovol  21095  dyadss  21096  dyaddisjlem  21097  dyadmaxlem  21099  opnmbllem  21103  mbfi1fseqlem1  21215  mbfi1fseqlem3  21217  mbfi1fseqlem4  21218  mbfi1fseqlem5  21219  mbfi1fseqlem6  21220  dveflem  21473  aaliou3lem9  21838  dcubic1lem  22260  dcubic2  22261  mcubic  22264  quartlem1  22274  quartlem2  22275  basellem1  22440  basellem2  22441  basellem3  22442  basellem4  22443  basellem5  22444  basellem6  22445  basellem7  22446  basellem8  22447  basellem9  22448  ppiltx  22537  prmorcht  22538  1sgm2ppw  22561  ppiublem1  22563  ppiub  22565  chtlepsi  22567  chtublem  22572  chpub  22581  mersenne  22588  perfect1  22589  perfectlem1  22590  perfectlem2  22591  perfect  22592  pcbcctr  22637  bclbnd  22641  bposlem1  22645  bposlem2  22646  bposlem3  22647  bposlem4  22648  bposlem5  22649  bposlem6  22650  bposlem8  22652  lgsdir2lem2  22685  lgsqr  22707  lgseisenlem1  22710  lgseisenlem2  22711  lgseisenlem3  22712  lgseisenlem4  22713  lgsquadlem1  22715  lgsquadlem2  22716  lgsquad2lem2  22720  2sqlem3  22727  2sqlem8  22733  chebbnd1lem1  22740  chebbnd1lem3  22742  chtppilimlem1  22744  logdivsum  22804  log2sumbnd  22815  pntlemd  22865  pntlema  22867  pntlemb  22868  pntlemf  22876  pntlemo  22878  ostth2lem1  22889  trkgstr  22927  ttgplusg  23146  ttgds  23149  axlowdimlem5  23214  axlowdimlem6  23215  axlowdimlem16  23225  axlowdimlem17  23226  axlowdim  23229  eengstr  23248  usgraexmpl  23341  cusgrasizeindb0  23400  usgrcyclnl2  23549  eupath2lem3  23622  konigsberg  23630  ex-xp  23665  ex-cnv  23666  ex-rn  23669  resvplusg  26323  oddpwdc  26759  eulerpartlemt  26776  eulerpartlemgh  26783  fib0  26804  fib1  26805  fib3  26808  signswbase  26977  signswplusg  26978  zetacvg  27023  lgamgulmlem4  27040  problem5  27324  opnmbllem0  28453  mblfinlem1  28454  dvasin  28506  areacirclem1  28510  heiborlem3  28738  heiborlem5  28740  heiborlem6  28741  heiborlem7  28742  heiborlem8  28743  heibor  28746  rmxypos  29316  ltrmynn0  29317  jm2.17a  29329  jm2.17b  29330  jm2.17c  29331  acongrep  29349  acongeq  29352  jm2.27a  29380  jm2.27c  29382  rmydioph  29389  rmxdioph  29391  expdiophlem2  29397  expdioph  29398  frlmpwfi  29479  lhe4.4ex1a  29629  wallispilem5  29890  wallispi2lem1  29892  wallispi2  29894  stirlinglem3  29897  stirlinglem8  29902  stirlinglem10  29904  stirlinglem15  29909  uz3m2nn  30221  wwlktovf  30277  usgra2pthspth  30321  usgra2pthlem1  30326  hlhilsplus  35684
  Copyright terms: Public domain W3C validator