Mathbox for David A. Wheeler |
< 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 11370. (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 42304 | . 2 class _𝐴𝐵 |
4 | c1 9816 | . . . . 5 class 1 | |
5 | cc0 9815 | . . . . 5 class 0 | |
6 | 4, 5 | cdc 11369 | . . . 4 class ;10 |
7 | cdiv 10563 | . . . 4 class / | |
8 | 2, 6, 7 | co 6549 | . . 3 class (𝐵 / ;10) |
9 | caddc 9818 | . . 3 class + | |
10 | 1, 8, 9 | co 6549 | . 2 class (𝐴 + (𝐵 / ;10)) |
11 | 3, 10 | wceq 1475 | 1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfdp2OLD 42307 dp2cl 42309 dpval 42310 dpfrac1 42312 |
Copyright terms: Public domain | W3C validator |