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

Theorem nnnn0i 10155
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 10154 . 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 1717   NNcn 9926   NN0cn0 10147
This theorem is referenced by:  1nn0  10163  2nn0  10164  3nn0  10165  4nn0  10166  5nn0  10167  6nn0  10168  7nn0  10169  8nn0  10170  9nn0  10171  10nn0  10172  numlt  10327  numlti  10332  faclbnd4lem1  11505  divalglem6  12839  pockthi  13196  dec5dvds2  13322  modxp1i  13327  mod2xnegi  13328  43prm  13365  83prm  13366  317prm  13369  strlemor2  13478  strlemor3  13479  log2ublem2  20648  ballotlemfmpn  24525  ballotth  24568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895  df-un 3262  df-in 3264  df-ss 3271  df-n0 10148
  Copyright terms: Public domain W3C validator