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

Theorem nnnn0i 12354
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 12353 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
31, 2ax-mp 5 1 𝑁 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  cn 12086  0cn0 12346
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3913  df-in 3915  df-ss 3925  df-n0 12347
This theorem is referenced by:  1nn0  12362  2nn0  12363  3nn0  12364  4nn0  12365  5nn0  12366  6nn0  12367  7nn0  12368  8nn0  12369  9nn0  12370  numlt  12575  declei  12586  numlti  12587  faclbnd4lem1  14120  divalglem6  16214  pockthi  16713  dec5dvds2  16871  modxp1i  16876  mod2xnegi  16877  43prm  16928  83prm  16929  317prm  16932  log2ublem2  26219  rpdp2cl2  31533  ballotlemfmpn  32867  ballotth  32910  circlevma  33028  12gcd5e1  40355  60gcd6e6  40356  60gcd7e1  40357  420lcm8e840  40363  lcmineqlem  40404  tgblthelfgott  45756  tgoldbach  45758
  Copyright terms: Public domain W3C validator