Theorem nnnn0i 12507

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

Syntax hints:   ∈ wcel 2108  ℕcn 12238  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-n0 12500

This theorem is referenced by:  1nn0  12515  2nn0  12516  3nn0  12517  4nn0  12518  5nn0  12519  6nn0  12520  7nn0  12521  8nn0  12522  9nn0  12523  numlt  12731  declei  12742  numlti  12743  faclbnd4lem1  14309  divalglem6  16415  pockthi  16925  dec5dvds2  17083  modxp1i  17088  mod2xnegi  17089  43prm  17139  83prm  17140  317prm  17143  log2ublem2  26907  rpdp2cl2  32803  ballotlemfmpn  34473  ballotth  34516  circlevma  34620  12gcd5e1  41962  60gcd6e6  41963  60gcd7e1  41964  420lcm8e840  41970  lcmineqlem  42011  tgblthelfgott  47777  tgoldbach  47779