Theorem nnnn0i 12507

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

Syntax hints:   ∈ wcel 2143  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-n0 12500

This theorem is referenced by:  1nn0  12515  2nn0  12516  3nn0  12517  4nn0  12518  5nn0  12519  6nn0  12520  7nn0  12521  8nn0  12522  9nn0  12523  numlt  12736  declei  12747  numlti  12748  faclbnd4lem1  14325  divalglem6  16451  pockthi  16962  dec5dvds2  17120  modxp1i  17125  mod2xnegi  17126  43prm  17177  317prm  17181  log2ublem2  27112  rpdp2cl2  33202  ballotlemfmpn  34885  ballotth  34928  circlevma  35029  12gcd5e1  42770  60gcd6e6  42771  60gcd7e1  42772  420lcm8e840  42778  lcmineqlem  42819  tgblthelfgott  48580  tgoldbach  48582