Theorem nnnn0i 12489

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

Syntax hints:   ∈ wcel 2142  ℕcn 12210  ℕ₀cn0 12481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-n0 12482

This theorem is referenced by:  1nn0  12497  2nn0  12498  3nn0  12499  4nn0  12500  5nn0  12501  6nn0  12502  7nn0  12503  8nn0  12504  9nn0  12505  numlt  12718  declei  12729  numlti  12730  faclbnd4lem1  14306  divalglem6  16432  pockthi  16943  dec5dvds2  17101  modxp1i  17106  mod2xnegi  17107  43prm  17158  83prm  17159  317prm  17162  log2ublem2  27012  rpdp2cl2  33060  ballotlemfmpn  34792  ballotth  34835  circlevma  34936  12gcd5e1  42620  60gcd6e6  42621  60gcd7e1  42622  420lcm8e840  42628  lcmineqlem  42669  tgblthelfgott  48437  tgoldbach  48439