Theorem nnnn0i 12480

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

Syntax hints:   ∈ wcel 2107  ℕcn 12212  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-n0 12473

This theorem is referenced by:  1nn0  12488  2nn0  12489  3nn0  12490  4nn0  12491  5nn0  12492  6nn0  12493  7nn0  12494  8nn0  12495  9nn0  12496  numlt  12702  declei  12713  numlti  12714  faclbnd4lem1  14253  divalglem6  16341  pockthi  16840  dec5dvds2  16998  modxp1i  17003  mod2xnegi  17004  43prm  17055  83prm  17056  317prm  17059  log2ublem2  26452  rpdp2cl2  32080  ballotlemfmpn  33524  ballotth  33567  circlevma  33685  12gcd5e1  40916  60gcd6e6  40917  60gcd7e1  40918  420lcm8e840  40924  lcmineqlem  40965  tgblthelfgott  46531  tgoldbach  46533