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 30124
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11821. (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 30123 . 2 class 𝐴𝐵
4 c1 10252 . . . . 5 class 1
5 cc0 10251 . . . . 5 class 0
64, 5cdc 11820 . . . 4 class 10
7 cdiv 11008 . . . 4 class /
82, 6, 7co 6904 . . 3 class (𝐵 / 10)
9 caddc 10254 . . 3 class +
101, 8, 9co 6904 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1658 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dp2eq1  30125  dp2eq2  30126  dp20u  30130  dp20h  30131  dp2cl  30132  dp2clq  30133  rpdp2cl  30134  dp2lt10  30136  dp2lt  30137  dp2ltsuc  30138  dp2ltc  30139  dpval  30142  dpfrac1  30144  dpval2  30145  dpval3  30146  dp3mul10  30150
  Copyright terms: Public domain W3C validator