Theorem nnnn0i 12654

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

This proof depends on syntax axioms:   ∈ wcel 2147  ℕcn 12375  ℕ₀cn0 12646

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-n0 12647

This theorem is used by:  1nn0  12662  2nn0  12663  3nn0  12664  4nn0  12665  5nn0  12666  6nn0  12667  7nn0  12668  8nn0  12669  9nn0  12670  numlt  12884  declei  12895  numlti  12896  faclbnd4lem1  14478  divalglem6  16612  pockthi  17129  dec5dvds2  17287  modxp1i  17292  mod2xnegi  17293  43prm  17344  317prm  17348  cnfldstr  21731  log2ublem2  27332  rpdp2cl2  33545  ballotlemfmpn  35238  ballotth  35281  circlevma  35382  12gcd5e1  43319  60gcd6e6  43320  60gcd7e1  43321  420lcm8e840  43327  lcmineqlem  43368  tgblthelfgott  49186  tgoldbach  49188