Theorem nnnn0i 12614

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℕcn 12335  ℕ₀cn0 12606

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-n0 12607

This theorem is used by:  1nn0  12622  2nn0  12623  3nn0  12624  4nn0  12625  5nn0  12626  6nn0  12627  7nn0  12628  8nn0  12629  9nn0  12630  numlt  12844  declei  12855  numlti  12856  faclbnd4lem1  14437  divalglem6  16568  pockthi  17085  dec5dvds2  17243  modxp1i  17248  mod2xnegi  17249  43prm  17300  317prm  17304  log2ublem2  27275  rpdp2cl2  33449  ballotlemfmpn  35127  ballotth  35170  circlevma  35271  12gcd5e1  43053  60gcd6e6  43054  60gcd7e1  43055  420lcm8e840  43061  lcmineqlem  43102  tgblthelfgott  48912  tgoldbach  48914