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

Definition df-10 10627
Description: Define the number 10. See remarks under df-2 10619. (Contributed by NM, 5-Feb-2007.)
Assertion
Ref Expression
df-10

Detailed syntax breakdown of Definition df-10
StepHypRef Expression
1 c10 10618 . 2
2 c9 10617 . . 3
3 c1 9514 . . 3
4 caddc 9516 . . 3
52, 3, 4co 6296 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  10re  10649  10pos  10663  9p1e10  10692  5p5e10  10701  6p4e10  10704  7p3e10  10706  8p2e10  10707  10nn  10726  9lt10  10763  decsucc  11031  9p2e11  11066  0.999...  13690  3dvds  14050  bposlem4  23562  bposlem5  23563  rmydioph  30956
  Copyright terms: Public domain W3C validator