Theorem nnnn0i 12527

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

This proof depends on syntax axioms:   ∈ wcel 2146  ℕcn 12248  ℕ₀cn0 12519

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-n0 12520

This theorem is used by:  1nn0  12535  2nn0  12536  3nn0  12537  4nn0  12538  5nn0  12539  6nn0  12540  7nn0  12541  8nn0  12542  9nn0  12543  numlt  12757  declei  12768  numlti  12769  faclbnd4lem1  14347  divalglem6  16478  pockthi  16989  dec5dvds2  17147  modxp1i  17152  mod2xnegi  17153  43prm  17204  317prm  17208  log2ublem2  27163  rpdp2cl2  33272  ballotlemfmpn  34950  ballotth  34993  circlevma  35094  12gcd5e1  42828  60gcd6e6  42829  60gcd7e1  42830  420lcm8e840  42836  lcmineqlem  42877  tgblthelfgott  48638  tgoldbach  48640