Theorem nnnn0i 12534

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

Syntax hints:   ∈ wcel 2108  ℕcn 12266  ℕ₀cn0 12526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-n0 12527

This theorem is referenced by:  1nn0  12542  2nn0  12543  3nn0  12544  4nn0  12545  5nn0  12546  6nn0  12547  7nn0  12548  8nn0  12549  9nn0  12550  numlt  12758  declei  12769  numlti  12770  faclbnd4lem1  14332  divalglem6  16435  pockthi  16945  dec5dvds2  17103  modxp1i  17108  mod2xnegi  17109  43prm  17159  83prm  17160  317prm  17163  log2ublem2  26990  rpdp2cl2  32865  ballotlemfmpn  34497  ballotth  34540  circlevma  34657  12gcd5e1  42004  60gcd6e6  42005  60gcd7e1  42006  420lcm8e840  42012  lcmineqlem  42053  tgblthelfgott  47802  tgoldbach  47804