Theorem nnnn0i 12445

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

Syntax hints:   ∈ wcel 2114  ℕcn 12174  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-n0 12438

This theorem is referenced by:  1nn0  12453  2nn0  12454  3nn0  12455  4nn0  12456  5nn0  12457  6nn0  12458  7nn0  12459  8nn0  12460  9nn0  12461  numlt  12669  declei  12680  numlti  12681  faclbnd4lem1  14255  divalglem6  16367  pockthi  16878  dec5dvds2  17036  modxp1i  17041  mod2xnegi  17042  43prm  17092  83prm  17093  317prm  17096  log2ublem2  26911  rpdp2cl2  32942  ballotlemfmpn  34639  ballotth  34682  circlevma  34786  12gcd5e1  42442  60gcd6e6  42443  60gcd7e1  42444  420lcm8e840  42450  lcmineqlem  42491  tgblthelfgott  48291  tgoldbach  48293