Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dp2 Structured version   Visualization version   GIF version

Definition df-dp2 32854
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.)
Assertion
Ref Expression
df-dp2 𝐴𝐵 = (𝐴 + (𝐵 / 10))

Detailed syntax breakdown of Definition df-dp2
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cdp2 32853 . 2 class 𝐴𝐵
4 c1 11156 . . . . 5 class 1
5 cc0 11155 . . . . 5 class 0
64, 5cdc 12733 . . . 4 class 10
7 cdiv 11920 . . . 4 class /
82, 6, 7co 7431 . . 3 class (𝐵 / 10)
9 caddc 11158 . . 3 class +
101, 8, 9co 7431 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 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