Theorem nnnn0i 10725

Description: A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.)

Hypothesis

Ref	Expression
nnnn0.1

Assertion

Ref	Expression
nnnn0i

Proof of Theorem nnnn0i

Step	Hyp	Ref	Expression
1		nnnn0.1	. 2
2		nnnn0 10724	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1758  cn 10460  cn0 10717

This theorem is referenced by:  1nn0  10733  2nn0  10734  3nn0  10735  4nn0  10736  5nn0  10737  6nn0  10738  7nn0  10739  8nn0  10740  9nn0  10741  10nn0  10742  numlt  10913  numlti  10918  faclbnd4lem1  12226  divalglem6  13760  pockthi  14126  dec5dvds2  14252  modxp1i  14257  mod2xnegi  14258  43prm  14307  83prm  14308  317prm  14311  strlemor2  14425  strlemor3  14426  log2ublem2  22742  ballotlemfmpn  27333  ballotth  27376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-un 3447  df-in 3449  df-ss 3456  df-n0 10718