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

Theorem 3nn 10781
Description: 3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
Assertion
Ref Expression
3nn  |-  3  e.  NN

Proof of Theorem 3nn
StepHypRef Expression
1 df-3 10682 . 2  |-  3  =  ( 2  +  1 )
2 2nn 10780 . . 3  |-  2  e.  NN
3 peano2nn 10634 . . 3  |-  ( 2  e.  NN  ->  (
2  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 2  +  1 )  e.  NN
51, 4eqeltri 2508 1  |-  3  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1873  (class class class)co 6311   1c1 9553    + caddc 9555   NNcn 10622   2c2 10672   3c3 10673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-1cn 9610
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3087  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 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-tp 4009  df-op 4011  df-uni 4226  df-iun 4307  df-br 4430  df-opab 4489  df-mpt 4490  df-tr 4525  df-eprel 4770  df-id 4774  df-po 4780  df-so 4781  df-fr 4818  df-we 4820  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-pred 5405  df-ord 5451  df-on 5452  df-lim 5453  df-suc 5454  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-ov 6314  df-om 6713  df-wrecs 7045  df-recs 7107  df-rdg 7145  df-nn 10623  df-2 10681  df-3 10682
This theorem is referenced by:  4nn  10782  3nn0  10900  3z  10983  ige3m2fz  11836  f1oun2prg  13008  sqrlem7  13318  bpoly4  14117  fsumcube  14118  ef01bndlem  14243  sin01bnd  14244  egt2lt3  14263  rpnnen2lem2  14273  rpnnen2lem3  14274  rpnnen2lem4  14275  rpnnen2lem9  14280  rpnnen2lem11  14282  3lcm2e6woprm  14585  3lcm2e6  14686  prmo3  15004  5prm  15085  6nprm  15086  7prm  15087  9nprm  15089  11prm  15091  13prm  15092  17prm  15093  19prm  15094  23prm  15095  prmlem2  15096  37prm  15097  43prm  15098  83prm  15099  139prm  15100  163prm  15101  317prm  15102  631prm  15103  1259lem5  15111  2503lem1  15113  2503lem2  15114  2503lem3  15115  4001lem4  15120  4001prm  15121  mulrndx  15247  mulrid  15248  rngstr  15249  ressmulr  15255  unifndx  15307  unifid  15308  lt6abl  17534  sramulr  18408  opsrmulr  18709  cnfldstr  18977  zlmmulr  19095  znmul  19116  ressunif  21281  tuslem  21286  tngmulr  21656  vitalilem4  22573  tangtx  23464  1cubrlem  23771  1cubr  23772  dcubic1lem  23773  dcubic2  23774  dcubic  23776  mcubic  23777  cubic2  23778  cubic  23779  quartlem3  23789  quart  23791  log2cnv  23874  log2tlbnd  23875  log2ublem1  23876  log2ublem2  23877  log2ub  23879  ppiublem1  24134  ppiub  24136  chtub  24144  bposlem3  24218  bposlem4  24219  bposlem5  24220  bposlem6  24221  bposlem9  24224  lgsdir2lem5  24259  dchrvmasumlem2  24340  dchrvmasumlema  24342  pntibndlem1  24431  pntibndlem2  24433  pntlema  24438  pntlemb  24439  pntleml  24453  tgcgr4  24580  axlowdimlem16  24991  axlowdimlem17  24992  usgraexmpldifpr  25131  constr3trllem3  25384  ex-cnv  25891  ex-rn  25894  resvmulr  28612  fib4  29251  sinccvglem  30330  mblfinlem3  31949  itg2addnclem2  31964  itg2addnclem3  31965  itg2addnc  31966  hlhilsmul  35487  rmydioph  35845  rmxdioph  35847  expdiophlem2  35853  expdioph  35854  amgm3d  36627  lhe4.4ex1a  36654  wtgoldbnnsum4prm  38773  bgoldbnnsum3prm  38775  bgoldbtbndlem1  38776  tgoldbach  38787  41prothprm  38795
  Copyright terms: Public domain W3C validator