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

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

Proof of Theorem nnnn0i
StepHypRef Expression
1 nnnn0i.1 . 2  |-  N  e.  NN
2 nnnn0 10808 . 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 1804   NNcn 10542   NN0cn0 10801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-n0 10802
This theorem is referenced by:  1nn0  10817  2nn0  10818  3nn0  10819  4nn0  10820  5nn0  10821  6nn0  10822  7nn0  10823  8nn0  10824  9nn0  10825  10nn0  10826  numlt  11003  numlti  11008  faclbnd4lem1  12350  divalglem6  13933  pockthi  14302  dec5dvds2  14428  modxp1i  14433  mod2xnegi  14434  43prm  14484  83prm  14485  317prm  14488  strlemor2  14602  strlemor3  14603  log2ublem2  23150  ballotlemfmpn  28306  ballotth  28349
  Copyright terms: Public domain W3C validator