Theorem nnnn0i 12511

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

Syntax hints:   ∈ wcel 2149  ℕcn 12232  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-n0 12504

This theorem is referenced by:  1nn0  12519  2nn0  12520  3nn0  12521  4nn0  12522  5nn0  12523  6nn0  12524  7nn0  12525  8nn0  12526  9nn0  12527  numlt  12740  declei  12751  numlti  12752  faclbnd4lem1  14328  divalglem6  16455  pockthi  16966  dec5dvds2  17124  modxp1i  17129  mod2xnegi  17130  43prm  17181  83prm  17182  317prm  17185  log2ublem2  27077  rpdp2cl2  33142  ballotlemfmpn  34829  ballotth  34872  circlevma  34973  12gcd5e1  42659  60gcd6e6  42660  60gcd7e1  42661  420lcm8e840  42667  lcmineqlem  42708  tgblthelfgott  48468  tgoldbach  48470