![]() |
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 12700. (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 32576 | . 2 class _𝐴𝐵 |
4 | c1 11131 | . . . . 5 class 1 | |
5 | cc0 11130 | . . . . 5 class 0 | |
6 | 4, 5 | cdc 12699 | . . . 4 class ;10 |
7 | cdiv 11893 | . . . 4 class / | |
8 | 2, 6, 7 | co 7414 | . . 3 class (𝐵 / ;10) |
9 | caddc 11133 | . . 3 class + | |
10 | 1, 8, 9 | co 7414 | . 2 class (𝐴 + (𝐵 / ;10)) |
11 | 3, 10 | wceq 1534 | 1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
Colors of variables: wff setvar class |
This definition is referenced by: dp2eq1 32578 dp2eq2 32579 dp20u 32583 dp20h 32584 dp2cl 32585 dp2clq 32586 rpdp2cl 32587 dp2lt10 32589 dp2lt 32590 dp2ltsuc 32591 dp2ltc 32592 dpval 32595 dpfrac1 32597 dpval2 32598 dpval3 32599 dp3mul10 32603 |
Copyright terms: Public domain | W3C validator |