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

Theorem nnnn0i 10690
Description: A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.)
Hypothesis
Ref Expression
nnnn0.1  |-  N  e.  NN
Assertion
Ref Expression
nnnn0i  |-  N  e. 
NN0

Proof of Theorem nnnn0i
StepHypRef Expression
1 nnnn0.1 . 2  |-  N  e.  NN
2 nnnn0 10689 . 2  |-  ( N  e.  NN  ->  N  e.  NN0 )
31, 2ax-mp 5 1  |-  N  e. 
NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   NNcn 10425   NN0cn0 10682
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-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-un 3433  df-in 3435  df-ss 3442  df-n0 10683
This theorem is referenced by:  1nn0  10698  2nn0  10699  3nn0  10700  4nn0  10701  5nn0  10702  6nn0  10703  7nn0  10704  8nn0  10705  9nn0  10706  10nn0  10707  numlt  10877  numlti  10882  faclbnd4lem1  12172  divalglem6  13706  pockthi  14072  dec5dvds2  14198  modxp1i  14203  mod2xnegi  14204  43prm  14253  83prm  14254  317prm  14257  strlemor2  14370  strlemor3  14371  log2ublem2  22460  ballotlemfmpn  27013  ballotth  27056
  Copyright terms: Public domain W3C validator