| 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 12734. (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 32853 | . 2 class _𝐴𝐵 |
| 4 | c1 11156 | . . . . 5 class 1 | |
| 5 | cc0 11155 | . . . . 5 class 0 | |
| 6 | 4, 5 | cdc 12733 | . . . 4 class ;10 |
| 7 | cdiv 11920 | . . . 4 class / | |
| 8 | 2, 6, 7 | co 7431 | . . 3 class (𝐵 / ;10) |
| 9 | caddc 11158 | . . 3 class + | |
| 10 | 1, 8, 9 | co 7431 | . 2 class (𝐴 + (𝐵 / ;10)) |
| 11 | 3, 10 | wceq 1540 | 1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dp2eq1 32855 dp2eq2 32856 dp20u 32860 dp20h 32861 dp2cl 32862 dp2clq 32863 rpdp2cl 32864 dp2lt10 32866 dp2lt 32867 dp2ltsuc 32868 dp2ltc 32869 dpval 32872 dpfrac1 32874 dpval2 32875 dpval3 32876 dp3mul10 32880 |
| Copyright terms: Public domain | W3C validator |