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

Theorem nnnn0i 12355
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 12354 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
31, 2ax-mp 5 1 𝑁 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cn 12087  0cn0 12347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-in 3916  df-ss 3926  df-n0 12348
This theorem is referenced by:  1nn0  12363  2nn0  12364  3nn0  12365  4nn0  12366  5nn0  12367  6nn0  12368  7nn0  12369  8nn0  12370  9nn0  12371  numlt  12576  declei  12587  numlti  12588  faclbnd4lem1  14121  divalglem6  16215  pockthi  16714  dec5dvds2  16872  modxp1i  16877  mod2xnegi  16878  43prm  16929  83prm  16930  317prm  16933  log2ublem2  26219  rpdp2cl2  31521  ballotlemfmpn  32855  ballotth  32898  circlevma  33016  12gcd5e1  40346  60gcd6e6  40347  60gcd7e1  40348  420lcm8e840  40354  lcmineqlem  40395  tgblthelfgott  45725  tgoldbach  45727
  Copyright terms: Public domain W3C validator