Theorem nnnn0i 12512

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

Syntax hints:   ∈ wcel 2149  ℕcn 12233  ℕ₀cn0 12504

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 12505

This theorem is referenced by:  1nn0  12520  2nn0  12521  3nn0  12522  4nn0  12523  5nn0  12524  6nn0  12525  7nn0  12526  8nn0  12527  9nn0  12528  numlt  12741  declei  12752  numlti  12753  faclbnd4lem1  14329  divalglem6  16456  pockthi  16967  dec5dvds2  17125  modxp1i  17130  mod2xnegi  17131  43prm  17182  83prm  17183  317prm  17186  log2ublem2  27078  rpdp2cl2  33143  ballotlemfmpn  34830  ballotth  34873  circlevma  34974  12gcd5e1  42660  60gcd6e6  42661  60gcd7e1  42662  420lcm8e840  42668  lcmineqlem  42709  tgblthelfgott  48469  tgoldbach  48471