Theorem nnnn0i 12457

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

Syntax hints:   ∈ wcel 2109  ℕcn 12193  ℕ₀cn0 12449

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-n0 12450

This theorem is referenced by:  1nn0  12465  2nn0  12466  3nn0  12467  4nn0  12468  5nn0  12469  6nn0  12470  7nn0  12471  8nn0  12472  9nn0  12473  numlt  12681  declei  12692  numlti  12693  faclbnd4lem1  14265  divalglem6  16375  pockthi  16885  dec5dvds2  17043  modxp1i  17048  mod2xnegi  17049  43prm  17099  83prm  17100  317prm  17103  log2ublem2  26864  rpdp2cl2  32810  ballotlemfmpn  34493  ballotth  34536  circlevma  34640  12gcd5e1  41998  60gcd6e6  41999  60gcd7e1  42000  420lcm8e840  42006  lcmineqlem  42047  tgblthelfgott  47820  tgoldbach  47822