Theorem nnnn0i 12171

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

Syntax hints:   ∈ wcel 2108  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-n0 12164

This theorem is referenced by:  1nn0  12179  2nn0  12180  3nn0  12181  4nn0  12182  5nn0  12183  6nn0  12184  7nn0  12185  8nn0  12186  9nn0  12187  numlt  12391  declei  12402  numlti  12403  faclbnd4lem1  13935  divalglem6  16035  pockthi  16536  dec5dvds2  16694  modxp1i  16699  mod2xnegi  16700  43prm  16751  83prm  16752  317prm  16755  log2ublem2  26002  rpdp2cl2  31059  ballotlemfmpn  32361  ballotth  32404  circlevma  32522  12gcd5e1  39939  60gcd6e6  39940  60gcd7e1  39941  420lcm8e840  39947  lcmineqlem  39988  tgblthelfgott  45155  tgoldbach  45157