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

Theorem 2nn 10767
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 10668 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10620 . . 3  |-  1  e.  NN
3 peano2nn 10621 . . 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 1870  (class class class)co 6305   1c1 9539    + caddc 9541   NNcn 10609   2c2 10659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-1cn 9596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-nn 10610  df-2 10668
This theorem is referenced by:  3nn  10768  2nn0  10886  2z  10969  uz3m2nn  11201  ige2m1fz1  11881  sqeq0  12336  expmulnbnd  12401  sqeq0d  12412  faclbnd5  12480  bcn2  12501  f1oun2prg  12981  wwlktovf  13010  climcndslem1  13885  climcndslem2  13886  climcnds  13887  harmonic  13895  geo2sum  13907  geo2lim  13909  ege2le3  14122  ef01bndlem  14216  egt2lt3  14236  nthruc  14281  bits0o  14378  bitsp1  14379  bitsfzolem  14382  bitsfzo  14383  bitsmod  14384  bitsfi  14385  bitscmp  14386  bitsinv1lem  14389  bitsinv1  14390  2ebits  14395  bitsinvp1  14397  sadcaddlem  14405  sadadd3  14409  sadaddlem  14414  sadasslem  14418  bitsres  14421  bitsuz  14422  bitsshft  14423  smumullem  14440  smumul  14441  sqgcd  14497  3lcm2e6woprm  14551  3prm  14612  3lcm2e6  14652  pythagtriplem4  14732  iserodd  14748  prmreclem3  14825  prmreclem5  14827  prmreclem6  14828  4sqlem12  14863  vdwlem3  14896  vdwlem9  14902  vdwlem10  14903  prmo2  14961  dec2dvds  14998  dec5nprm  15001  dec2nprm  15002  2expltfac  15026  4nprm  15039  5prm  15043  6nprm  15044  7prm  15045  8nprm  15046  10nprm  15048  11prm  15049  17prm  15051  23prm  15053  37prm  15055  43prm  15056  83prm  15057  139prm  15058  163prm  15059  317prm  15060  631prm  15061  1259lem1  15065  1259lem2  15066  1259lem3  15067  1259lem4  15068  1259lem5  15069  1259prm  15070  2503lem1  15071  2503lem2  15072  2503lem3  15073  2503prm  15074  4001lem1  15075  4001lem2  15076  4001lem3  15077  4001lem4  15078  4001prm  15079  plusgndx  15186  plusgid  15187  grpstr  15195  grpbase  15196  grpplusg  15197  ressplusg  15198  rngstr  15203  lmodstr  15220  topgrpstr  15245  dsndx  15259  dsid  15260  odrngstr  15263  ressds  15270  imasvalstr  15309  pmtrprfvalrn  17080  psgnunilem2  17087  psgnprfval  17113  psgnprfval1  17114  mgpds  17668  oppradd  17793  sraaddg  18337  srads  18344  opsrplusg  18638  cnfldstr  18907  zlmplusg  19021  znadd  19042  m2detleiblem1  19580  m2detleiblem5  19581  m2detleiblem6  19582  m2detleiblem3  19585  m2detleiblem4  19586  m2detleib  19587  tmslem  21428  tngplusg  21581  ovollb2lem  22319  ovolunlem1a  22327  ovolunlem1  22328  ovoliunlem1  22333  ovoliunlem3  22335  dyadf  22426  dyadovol  22428  dyadss  22429  dyaddisjlem  22430  dyadmaxlem  22432  opnmbllem  22436  mbfi1fseqlem1  22550  mbfi1fseqlem3  22552  mbfi1fseqlem4  22553  mbfi1fseqlem5  22554  mbfi1fseqlem6  22555  dveflem  22808  aaliou3lem9  23171  dcubic1lem  23634  dcubic2  23635  mcubic  23638  quartlem1  23648  quartlem2  23649  zetacvg  23805  lgamgulmlem4  23822  basellem1  23870  basellem2  23871  basellem3  23872  basellem4  23873  basellem5  23874  basellem6  23875  basellem7  23876  basellem8  23877  basellem9  23878  1sgm2ppw  23991  ppiublem1  23993  chtublem  24002  mersenne  24018  perfect1  24019  perfectlem1  24020  perfectlem2  24021  perfect  24022  pcbcctr  24067  bclbnd  24071  bposlem1  24075  bposlem2  24076  bposlem3  24077  bposlem4  24078  bposlem5  24079  bposlem6  24080  bposlem8  24082  lgsdir2lem2  24115  lgsqr  24137  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgseisenlem4  24143  lgsquadlem1  24145  lgsquadlem2  24146  lgsquad2lem2  24150  2sqlem3  24157  2sqlem8  24163  chebbnd1lem1  24170  chebbnd1lem3  24172  logdivsum  24234  log2sumbnd  24245  pntlemd  24295  pntlema  24297  pntlemb  24298  pntlemf  24306  pntlemo  24308  ostth2lem1  24319  trkgstr  24355  ttgplusg  24754  ttgds  24757  axlowdimlem6  24823  eengstr  24856  usgraexmpl  24974  cusgrasizeindb0  25043  usgrcyclnl2  25214  eupath2lem3  25552  konigsberg  25560  ex-xp  25731  ex-cnv  25732  ex-rn  25735  resvplusg  28435  lmat22e11  28483  lmat22e12  28484  lmat22e21  28485  lmat22e22  28486  lmat22det  28487  oddpwdc  29013  eulerpartlemt  29030  eulerpartlemgh  29037  fib0  29058  fib1  29059  fib3  29062  problem5  30089  bcprod  30161  opnmbllem0  31679  mblfinlem1  31680  dvasin  31731  areacirclem1  31735  heiborlem3  31848  heiborlem5  31850  heiborlem6  31851  heiborlem7  31852  heiborlem8  31853  heibor  31856  hlhilsplus  35219  jm2.17a  35515  jm2.17b  35516  jm2.17c  35517  acongrep  35535  acongeq  35538  jm2.27a  35565  jm2.27c  35567  rmydioph  35574  rmxdioph  35576  expdiophlem2  35582  expdioph  35583  frlmpwfi  35661  amgm2d  36286  hashnzfz2  36306  lhe4.4ex1a  36314  wallispilem5  37499  wallispi2lem1  37501  wallispi2  37503  stirlinglem3  37506  stirlinglem8  37511  stirlinglem10  37513  stirlinglem15  37518  dirkertrigeqlem3  37530  fouriersw  37662  elmod2  38113  iseven5  38183  oddprmALTV  38205  perfectALTVlem1  38232  perfectALTVlem2  38233  perfectALTV  38234  nnsum3primes4  38272  nnsum3primesgbe  38276  nnsum4primesevenALTV  38285  bgoldbtbndlem1  38289  tgblthelfgott  38297  proththdlem  38302  proththd  38303  pfx2  38342  usgra2pthspth  38420  usgra2pthlem1  38422  pw2m1lepw2m1  39078  nnpw2even  39096  logbpw2m1  39138  blenpw2  39149  nnpw2pmod  39154  blen2  39156  nnpw2p  39157  nnpw2pb  39158  blennnt2  39160  nnolog2flm1  39161  dig2nn1st  39176  0dig2pr01  39181  dig2nn0  39182  0dig2nn0e  39183  0dig2nn0o  39184  dig2bits  39185  dignn0flhalflem1  39186  dignn0ehalf  39188  dignn0flhalf  39189  nn0sumshdiglemA  39190  nn0sumshdiglemB  39191  nn0sumshdiglem1  39192  nn0sumshdiglem2  39193  nn0mullong  39196
  Copyright terms: Public domain W3C validator