Theorem nnnn0i 12436

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

Syntax hints:   ∈ wcel 2119  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-n0 12429

This theorem is referenced by:  1nn0  12444  2nn0  12445  3nn0  12446  4nn0  12447  5nn0  12448  6nn0  12449  7nn0  12450  8nn0  12451  9nn0  12452  numlt  12660  declei  12671  numlti  12672  faclbnd4lem1  14246  divalglem6  16358  pockthi  16869  dec5dvds2  17027  modxp1i  17032  mod2xnegi  17033  43prm  17083  83prm  17084  317prm  17087  log2ublem2  26929  rpdp2cl2  32961  ballotlemfmpn  34679  ballotth  34722  circlevma  34826  12gcd5e1  42488  60gcd6e6  42489  60gcd7e1  42490  420lcm8e840  42496  lcmineqlem  42537  tgblthelfgott  48306  tgoldbach  48308