Theorem nnnn0i 12409

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

Syntax hints:   ∈ wcel 2113  ℕcn 12145  ℕ₀cn0 12401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-n0 12402

This theorem is referenced by:  1nn0  12417  2nn0  12418  3nn0  12419  4nn0  12420  5nn0  12421  6nn0  12422  7nn0  12423  8nn0  12424  9nn0  12425  numlt  12632  declei  12643  numlti  12644  faclbnd4lem1  14216  divalglem6  16325  pockthi  16835  dec5dvds2  16993  modxp1i  16998  mod2xnegi  16999  43prm  17049  83prm  17050  317prm  17053  log2ublem2  26913  rpdp2cl2  32964  ballotlemfmpn  34652  ballotth  34695  circlevma  34799  12gcd5e1  42257  60gcd6e6  42258  60gcd7e1  42259  420lcm8e840  42265  lcmineqlem  42306  tgblthelfgott  48061  tgoldbach  48063