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

Theorem nnnn0i 9989
Description: A natural number 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 9988 . 2  |-  ( N  e.  NN  ->  N  e.  NN0 )
31, 2ax-mp 8 1  |-  N  e. 
NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   NNcn 9762   NN0cn0 9981
This theorem is referenced by:  1nn0  9997  2nn0  9998  3nn0  9999  4nn0  10000  5nn0  10001  6nn0  10002  7nn0  10003  8nn0  10004  9nn0  10005  10nn0  10006  numlt  10159  numlti  10164  faclbnd4lem1  11322  divalglem6  12613  pockthi  12970  dec5dvds2  13096  modxp1i  13101  mod2xnegi  13102  43prm  13139  83prm  13140  317prm  13143  strlemor2  13252  strlemor3  13253  log2ublem2  20259  ballotlemfmpn  23069  ballotth  23112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-n0 9982
  Copyright terms: Public domain W3C validator