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

Theorem nnnn0i 12421
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 12420 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
31, 2ax-mp 5 1 𝑁 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  cn 12153  0cn0 12413
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 2707
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 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-un 3915  df-in 3917  df-ss 3927  df-n0 12414
This theorem is referenced by:  1nn0  12429  2nn0  12430  3nn0  12431  4nn0  12432  5nn0  12433  6nn0  12434  7nn0  12435  8nn0  12436  9nn0  12437  numlt  12643  declei  12654  numlti  12655  faclbnd4lem1  14193  divalglem6  16280  pockthi  16779  dec5dvds2  16937  modxp1i  16942  mod2xnegi  16943  43prm  16994  83prm  16995  317prm  16998  log2ublem2  26297  rpdp2cl2  31739  ballotlemfmpn  33094  ballotth  33137  circlevma  33255  12gcd5e1  40460  60gcd6e6  40461  60gcd7e1  40462  420lcm8e840  40468  lcmineqlem  40509  tgblthelfgott  45997  tgoldbach  45999
  Copyright terms: Public domain W3C validator