MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnnn0i Unicode version

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
StepHypRef Expression
1 nnnn0.1 . 2
2 nnnn0 10724 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator