Metamath Proof Explorer


Definition df-dp2

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec . (Contributed by David A. Wheeler, 15-May-2015) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion df-dp2 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cB 𝐵
2 0 1 cdp2 𝐴 𝐵
3 caddc +
4 cdiv /
5 c1 1
6 cc0 0
7 5 6 cdc 1 0
8 1 7 4 co ( 𝐵 / 1 0 )
9 0 8 3 co ( 𝐴 + ( 𝐵 / 1 0 ) )
10 2 9 wceq 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )