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

Theorem 5nn 10592
Description: 5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
Assertion
Ref Expression
5nn  |-  5  e.  NN

Proof of Theorem 5nn
StepHypRef Expression
1 df-5 10493 . 2  |-  5  =  ( 4  +  1 )
2 4nn 10591 . . 3  |-  4  e.  NN
3 peano2nn 10444 . . 3  |-  ( 4  e.  NN  ->  (
4  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 4  +  1 )  e.  NN
51, 4eqeltri 2538 1  |-  5  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758  (class class class)co 6199   1c1 9393    + caddc 9395   NNcn 10432   4c4 10483   5c5 10484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-1cn 9450
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-om 6586  df-recs 6941  df-rdg 6975  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-5 10493
This theorem is referenced by:  6nn  10593  5nn0  10709  dec5dvds  14210  dec5nprm  14212  dec2nprm  14213  5prm  14253  10nprm  14258  23prm  14263  prmlem2  14264  43prm  14266  83prm  14267  317prm  14270  scandx  14416  scaid  14417  lmodstr  14420  ipsstr  14427  resssca  14434  ccondx  14473  ccoid  14474  ressco  14476  prdsvalstr  14509  oppchomfval  14771  oppcbas  14775  rescco  14863  catstr  14985  lt6abl  16491  mgpsca  16719  psrvalstr  17552  opsrsca  17687  tngsca  20362  log2ublem1  22473  log2ublem2  22474  log2ub  22476  birthday  22480  ppiublem1  22673  ppiublem2  22674  ppiub  22675  bclbnd  22751  bposlem3  22757  bposlem4  22758  bposlem5  22759  bposlem6  22760  bposlem8  22762  bposlem9  22763  lgsdir2lem3  22796  ex-eprel  23791  ex-xp  23794  fib6  26932  rmydioph  29510  expdiophlem2  29518  algstr  29681
  Copyright terms: Public domain W3C validator