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

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

Detailed syntax breakdown of Definition df-10
StepHypRef Expression
1 c10 10371 . 2
2 c9 10370 . . 3
3 c1 9275 . . 3
4 caddc 9277 . . 3
52, 3, 4co 6086 . 2
61, 5wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  10re  10402  10pos  10416  9p1e10  10445  5p5e10  10454  6p4e10  10457  7p3e10  10459  8p2e10  10460  10nn  10479  9lt10  10516  decsucc  10774  9p2e11  10809  0.999...  13333  3dvds  13588  bposlem4  22606  bposlem5  22607  rmydioph  29334
  Copyright terms: Public domain W3C validator