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

Step	Hyp	Ref	Expression
1		nnnn0i.1	. 2 ⊢ 𝑁 ∈ ℕ
2		nnnn0 12420	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
3	1, 2	ax-mp 5	1 ⊢ 𝑁 ∈ ℕ0

Syntax hints:   ∈ wcel 2114  ℕcn 12157  ℕ₀cn0 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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  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  12644  declei  12655  numlti  12656  faclbnd4lem1  14228  divalglem6  16337  pockthi  16847  dec5dvds2  17005  modxp1i  17010  mod2xnegi  17011  43prm  17061  83prm  17062  317prm  17065  log2ublem2  26925  rpdp2cl2  32975  ballotlemfmpn  34673  ballotth  34716  circlevma  34820  12gcd5e1  42373  60gcd6e6  42374  60gcd7e1  42375  420lcm8e840  42381  lcmineqlem  42422  tgblthelfgott  48175  tgoldbach  48177