Theorem nnnn0i 11899

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

Syntax hints:   ∈ wcel 2110  ℕcn 11632  ℕ₀cn0 11891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941  df-in 3943  df-ss 3952  df-n0 11892

This theorem is referenced by:  1nn0  11907  2nn0  11908  3nn0  11909  4nn0  11910  5nn0  11911  6nn0  11912  7nn0  11913  8nn0  11914  9nn0  11915  numlt  12117  declei  12128  numlti  12129  faclbnd4lem1  13647  divalglem6  15743  pockthi  16237  dec5dvds2  16395  modxp1i  16400  mod2xnegi  16401  43prm  16449  83prm  16450  317prm  16453  log2ublem2  25519  rpdp2cl2  30554  ballotlemfmpn  31747  ballotth  31790  circlevma  31908  tgblthelfgott  43973  tgoldbach  43975