Theorem nnnn0i 12439

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

Syntax hints:   ∈ wcel 2114  ℕcn 12168  ℕ₀cn0 12431

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-n0 12432

This theorem is referenced by:  1nn0  12447  2nn0  12448  3nn0  12449  4nn0  12450  5nn0  12451  6nn0  12452  7nn0  12453  8nn0  12454  9nn0  12455  numlt  12663  declei  12674  numlti  12675  faclbnd4lem1  14249  divalglem6  16361  pockthi  16872  dec5dvds2  17030  modxp1i  17035  mod2xnegi  17036  43prm  17086  83prm  17087  317prm  17090  log2ublem2  26927  rpdp2cl2  32960  ballotlemfmpn  34658  ballotth  34701  circlevma  34805  12gcd5e1  42459  60gcd6e6  42460  60gcd7e1  42461  420lcm8e840  42467  lcmineqlem  42508  tgblthelfgott  48306  tgoldbach  48308