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 12087. (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 30474 | . 2 class _𝐴𝐵 |
4 | c1 10526 | . . . . 5 class 1 | |
5 | cc0 10525 | . . . . 5 class 0 | |
6 | 4, 5 | cdc 12086 | . . . 4 class ;10 |
7 | cdiv 11285 | . . . 4 class / | |
8 | 2, 6, 7 | co 7145 | . . 3 class (𝐵 / ;10) |
9 | caddc 10528 | . . 3 class + | |
10 | 1, 8, 9 | co 7145 | . 2 class (𝐴 + (𝐵 / ;10)) |
11 | 3, 10 | wceq 1528 | 1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
Colors of variables: wff setvar class |
This definition is referenced by: dp2eq1 30476 dp2eq2 30477 dp20u 30481 dp20h 30482 dp2cl 30483 dp2clq 30484 rpdp2cl 30485 dp2lt10 30487 dp2lt 30488 dp2ltsuc 30489 dp2ltc 30490 dpval 30493 dpfrac1 30495 dpval2 30496 dpval3 30497 dp3mul10 30501 |
Copyright terms: Public domain | W3C validator |