Theorem nnnn0i 12381

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 12380	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
3	1, 2	ax-mp 5	1 ⊢ 𝑁 ∈ ℕ0

Syntax hints:   ∈ wcel 2110  ℕcn 12117  ℕ₀cn0 12373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905  df-ss 3917  df-n0 12374

This theorem is referenced by:  1nn0  12389  2nn0  12390  3nn0  12391  4nn0  12392  5nn0  12393  6nn0  12394  7nn0  12395  8nn0  12396  9nn0  12397  numlt  12605  declei  12616  numlti  12617  faclbnd4lem1  14192  divalglem6  16301  pockthi  16811  dec5dvds2  16969  modxp1i  16974  mod2xnegi  16975  43prm  17025  83prm  17026  317prm  17029  log2ublem2  26877  rpdp2cl2  32853  ballotlemfmpn  34498  ballotth  34541  circlevma  34645  12gcd5e1  42015  60gcd6e6  42016  60gcd7e1  42017  420lcm8e840  42023  lcmineqlem  42064  tgblthelfgott  47825  tgoldbach  47827