Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-10OLD | Structured version Visualization version Unicode version |
Description: Define the number 10. See remarks under df-2 11079. (Contributed by NM, 5-Feb-2007.) Obsolete as of 9-Sep-2021. (New usage is discouraged.) |
Ref | Expression |
---|---|
df-10OLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c10 11078 | . 2 | |
2 | c9 11077 | . . 3 | |
3 | c1 9937 | . . 3 | |
4 | caddc 9939 | . . 3 | |
5 | 2, 3, 4 | co 6650 | . 2 |
6 | 1, 5 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: 10reOLD 11109 10posOLD 11123 9p1e10OLD 11159 5p5e10OLD 11168 6p4e10OLD 11171 7p3e10OLD 11173 8p2e10OLD 11174 10nnOLD 11193 9lt10OLD 11230 decsuccOLD 11551 9p2e11OLD 11620 0.999...OLD 14613 3dvdsOLD 15053 3dvdsdecOLD 15055 3dvds2decOLD 15057 |
Copyright terms: Public domain | W3C validator |