Theorem nnnn0i 11300

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

Syntax hints:   ∈ wcel 1990  ℕcn 11020  ℕ₀cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-n0 11293

This theorem is referenced by:  1nn0  11308  2nn0  11309  3nn0  11310  4nn0  11311  5nn0  11312  6nn0  11313  7nn0  11314  8nn0  11315  9nn0  11316  10nn0OLD  11317  numlt  11527  declei  11542  numlti  11545  faclbnd4lem1  13080  divalglem6  15121  pockthi  15611  dec5dvds2  15769  modxp1i  15774  mod2xnegi  15775  43prm  15829  83prm  15830  317prm  15833  strlemor2OLD  15970  strlemor3OLD  15971  log2ublem2  24674  rpdp2cl2  29590  ballotlemfmpn  30556  ballotth  30599  circlevma  30720  tgblthelfgott  41703  tgoldbach  41705  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  tgoldbachOLD  41712