Theorem nnnn0i 12098

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

Syntax hints:   ∈ wcel 2110  ℕcn 11830  ℕ₀cn0 12090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-in 3873  df-ss 3883  df-n0 12091

This theorem is referenced by:  1nn0  12106  2nn0  12107  3nn0  12108  4nn0  12109  5nn0  12110  6nn0  12111  7nn0  12112  8nn0  12113  9nn0  12114  numlt  12318  declei  12329  numlti  12330  faclbnd4lem1  13859  divalglem6  15959  pockthi  16460  dec5dvds2  16618  modxp1i  16623  mod2xnegi  16624  43prm  16675  83prm  16676  317prm  16679  log2ublem2  25830  rpdp2cl2  30877  ballotlemfmpn  32173  ballotth  32216  circlevma  32334  12gcd5e1  39745  60gcd6e6  39746  60gcd7e1  39747  420lcm8e840  39753  lcmineqlem  39794  tgblthelfgott  44940  tgoldbach  44942