Theorem nnnn0i 12241

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

Syntax hints:   ∈ wcel 2106  ℕcn 11973  ℕ₀cn0 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-n0 12234

This theorem is referenced by:  1nn0  12249  2nn0  12250  3nn0  12251  4nn0  12252  5nn0  12253  6nn0  12254  7nn0  12255  8nn0  12256  9nn0  12257  numlt  12462  declei  12473  numlti  12474  faclbnd4lem1  14007  divalglem6  16107  pockthi  16608  dec5dvds2  16766  modxp1i  16771  mod2xnegi  16772  43prm  16823  83prm  16824  317prm  16827  log2ublem2  26097  rpdp2cl2  31157  ballotlemfmpn  32461  ballotth  32504  circlevma  32622  12gcd5e1  40011  60gcd6e6  40012  60gcd7e1  40013  420lcm8e840  40019  lcmineqlem  40060  tgblthelfgott  45267  tgoldbach  45269