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

Theorem nnnn0i 11507
Description: A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.)
Hypothesis
Ref Expression
nnnn0i.1 𝑁 ∈ ℕ
Assertion
Ref Expression
nnnn0i 𝑁 ∈ ℕ0

Proof of Theorem nnnn0i
StepHypRef Expression
1 nnnn0i.1 . 2 𝑁 ∈ ℕ
2 nnnn0 11506 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
31, 2ax-mp 5 1 𝑁 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  cn 11226  0cn0 11499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-n0 11500
This theorem is referenced by:  1nn0  11515  2nn0  11516  3nn0  11517  4nn0  11518  5nn0  11519  6nn0  11520  7nn0  11521  8nn0  11522  9nn0  11523  10nn0OLD  11524  numlt  11734  declei  11749  numlti  11752  faclbnd4lem1  13284  divalglem6  15329  pockthi  15818  dec5dvds2  15976  modxp1i  15981  mod2xnegi  15982  43prm  16036  83prm  16037  317prm  16040  strlemor2OLD  16178  strlemor3OLD  16179  log2ublem2  24895  rpdp2cl2  29930  ballotlemfmpn  30896  ballotth  30939  circlevma  31060  tgblthelfgott  42228  tgoldbach  42230  bgoldbachltOLD  42232  tgblthelfgottOLD  42234  tgoldbachOLD  42237
  Copyright terms: Public domain W3C validator