Theorem nnnn0i 11753

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

Syntax hints:   ∈ wcel 2081  ℕcn 11486  ℕ₀cn0 11745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3864  df-in 3866  df-ss 3874  df-n0 11746

This theorem is referenced by:  1nn0  11761  2nn0  11762  3nn0  11763  4nn0  11764  5nn0  11765  6nn0  11766  7nn0  11767  8nn0  11768  9nn0  11769  numlt  11972  declei  11983  numlti  11984  faclbnd4lem1  13503  divalglem6  15582  pockthi  16072  dec5dvds2  16230  modxp1i  16235  mod2xnegi  16236  43prm  16284  83prm  16285  317prm  16288  log2ublem2  25207  rpdp2cl2  30243  ballotlemfmpn  31369  ballotth  31412  circlevma  31530  tgblthelfgott  43462  tgoldbach  43464