Theorem nnnn0i 12537

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℕcn 12258  ℕ₀cn0 12529

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-n0 12530

This theorem is used by:  1nn0  12545  2nn0  12546  3nn0  12547  4nn0  12548  5nn0  12549  6nn0  12550  7nn0  12551  8nn0  12552  9nn0  12553  numlt  12767  declei  12778  numlti  12779  faclbnd4lem1  14358  divalglem6  16489  pockthi  17000  dec5dvds2  17158  modxp1i  17163  mod2xnegi  17164  43prm  17215  317prm  17219  log2ublem2  27185  rpdp2cl2  33329  ballotlemfmpn  35007  ballotth  35050  circlevma  35151  12gcd5e1  42870  60gcd6e6  42871  60gcd7e1  42872  420lcm8e840  42878  lcmineqlem  42919  tgblthelfgott  48732  tgoldbach  48734