![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-dp2 | Structured version Visualization version GIF version |
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11821. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
Ref | Expression |
---|---|
df-dp2 | ⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cdp2 30123 | . 2 class _𝐴𝐵 |
4 | c1 10252 | . . . . 5 class 1 | |
5 | cc0 10251 | . . . . 5 class 0 | |
6 | 4, 5 | cdc 11820 | . . . 4 class ;10 |
7 | cdiv 11008 | . . . 4 class / | |
8 | 2, 6, 7 | co 6904 | . . 3 class (𝐵 / ;10) |
9 | caddc 10254 | . . 3 class + | |
10 | 1, 8, 9 | co 6904 | . 2 class (𝐴 + (𝐵 / ;10)) |
11 | 3, 10 | wceq 1658 | 1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
Colors of variables: wff setvar class |
This definition is referenced by: dp2eq1 30125 dp2eq2 30126 dp20u 30130 dp20h 30131 dp2cl 30132 dp2clq 30133 rpdp2cl 30134 dp2lt10 30136 dp2lt 30137 dp2ltsuc 30138 dp2ltc 30139 dpval 30142 dpfrac1 30144 dpval2 30145 dpval3 30146 dp3mul10 30150 |
Copyright terms: Public domain | W3C validator |