Theorem nnnn0i 12407

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

Syntax hints:   ∈ wcel 2113  ℕcn 12143  ℕ₀cn0 12399

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-n0 12400

This theorem is referenced by:  1nn0  12415  2nn0  12416  3nn0  12417  4nn0  12418  5nn0  12419  6nn0  12420  7nn0  12421  8nn0  12422  9nn0  12423  numlt  12630  declei  12641  numlti  12642  faclbnd4lem1  14214  divalglem6  16323  pockthi  16833  dec5dvds2  16991  modxp1i  16996  mod2xnegi  16997  43prm  17047  83prm  17048  317prm  17051  log2ublem2  26911  rpdp2cl2  32913  ballotlemfmpn  34601  ballotth  34644  circlevma  34748  12gcd5e1  42196  60gcd6e6  42197  60gcd7e1  42198  420lcm8e840  42204  lcmineqlem  42245  tgblthelfgott  48003  tgoldbach  48005