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

Theorem nnnn0i 11911
 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 11910 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
31, 2ax-mp 5 1 𝑁 ∈ ℕ0
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111  ℕcn 11643  ℕ0cn0 11903 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-un 3888  df-in 3890  df-ss 3900  df-n0 11904 This theorem is referenced by:  1nn0  11919  2nn0  11920  3nn0  11921  4nn0  11922  5nn0  11923  6nn0  11924  7nn0  11925  8nn0  11926  9nn0  11927  numlt  12131  declei  12142  numlti  12143  faclbnd4lem1  13669  divalglem6  15759  pockthi  16253  dec5dvds2  16411  modxp1i  16416  mod2xnegi  16417  43prm  16467  83prm  16468  317prm  16471  log2ublem2  25577  rpdp2cl2  30629  ballotlemfmpn  31928  ballotth  31971  circlevma  32089  12gcd5e1  39442  60gcd6e6  39443  60gcd7e1  39444  420lcm8e840  39450  lcmineqlem  39491  tgblthelfgott  44501  tgoldbach  44503
 Copyright terms: Public domain W3C validator