Theorem nnnn0i 12621

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

This proof depends on syntax axioms:   ∈ wcel 2144  ℕcn 12342  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-n0 12614

This theorem is used by:  1nn0  12629  2nn0  12630  3nn0  12631  4nn0  12632  5nn0  12633  6nn0  12634  7nn0  12635  8nn0  12636  9nn0  12637  numlt  12851  declei  12862  numlti  12863  faclbnd4lem1  14444  divalglem6  16577  pockthi  17094  dec5dvds2  17252  modxp1i  17257  mod2xnegi  17258  43prm  17309  317prm  17313  log2ublem2  27284  rpdp2cl2  33499  ballotlemfmpn  35177  ballotth  35220  circlevma  35321  12gcd5e1  43190  60gcd6e6  43191  60gcd7e1  43192  420lcm8e840  43198  lcmineqlem  43239  tgblthelfgott  49049  tgoldbach  49051