Theorem nnnn0i 12450

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

Syntax hints:   ∈ wcel 2109  ℕcn 12186  ℕ₀cn0 12442

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-n0 12443

This theorem is referenced by:  1nn0  12458  2nn0  12459  3nn0  12460  4nn0  12461  5nn0  12462  6nn0  12463  7nn0  12464  8nn0  12465  9nn0  12466  numlt  12674  declei  12685  numlti  12686  faclbnd4lem1  14258  divalglem6  16368  pockthi  16878  dec5dvds2  17036  modxp1i  17041  mod2xnegi  17042  43prm  17092  83prm  17093  317prm  17096  log2ublem2  26857  rpdp2cl2  32803  ballotlemfmpn  34486  ballotth  34529  circlevma  34633  12gcd5e1  41991  60gcd6e6  41992  60gcd7e1  41993  420lcm8e840  41999  lcmineqlem  42040  tgblthelfgott  47816  tgoldbach  47818