Theorem nnnn0i 12561

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

Syntax hints:   ∈ wcel 2108  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-n0 12554

This theorem is referenced by:  1nn0  12569  2nn0  12570  3nn0  12571  4nn0  12572  5nn0  12573  6nn0  12574  7nn0  12575  8nn0  12576  9nn0  12577  numlt  12783  declei  12794  numlti  12795  faclbnd4lem1  14342  divalglem6  16446  pockthi  16954  dec5dvds2  17112  modxp1i  17117  mod2xnegi  17118  43prm  17169  83prm  17170  317prm  17173  log2ublem2  27008  rpdp2cl2  32847  ballotlemfmpn  34459  ballotth  34502  circlevma  34619  12gcd5e1  41960  60gcd6e6  41961  60gcd7e1  41962  420lcm8e840  41968  lcmineqlem  42009  tgblthelfgott  47689  tgoldbach  47691