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