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

Theorem nnnn0i 10575
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 10574 . 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 1755   NNcn 10310   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-n0 10568
This theorem is referenced by:  1nn0  10583  2nn0  10584  3nn0  10585  4nn0  10586  5nn0  10587  6nn0  10588  7nn0  10589  8nn0  10590  9nn0  10591  10nn0  10592  numlt  10762  numlti  10767  faclbnd4lem1  12053  divalglem6  13585  pockthi  13951  dec5dvds2  14077  modxp1i  14082  mod2xnegi  14083  43prm  14132  83prm  14133  317prm  14136  strlemor2  14249  strlemor3  14250  log2ublem2  22227  ballotlemfmpn  26725  ballotth  26768
  Copyright terms: Public domain W3C validator