Theorem nnnn0i 12426

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

Syntax hints:   ∈ wcel 2109  ℕcn 12162  ℕ₀cn0 12418

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-n0 12419

This theorem is referenced by:  1nn0  12434  2nn0  12435  3nn0  12436  4nn0  12437  5nn0  12438  6nn0  12439  7nn0  12440  8nn0  12441  9nn0  12442  numlt  12650  declei  12661  numlti  12662  faclbnd4lem1  14234  divalglem6  16344  pockthi  16854  dec5dvds2  17012  modxp1i  17017  mod2xnegi  17018  43prm  17068  83prm  17069  317prm  17072  log2ublem2  26890  rpdp2cl2  32853  ballotlemfmpn  34479  ballotth  34522  circlevma  34626  12gcd5e1  41984  60gcd6e6  41985  60gcd7e1  41986  420lcm8e840  41992  lcmineqlem  42033  tgblthelfgott  47809  tgoldbach  47811