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 30475
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12087. (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 30474 . 2 class 𝐴𝐵
4 c1 10526 . . . . 5 class 1
5 cc0 10525 . . . . 5 class 0
64, 5cdc 12086 . . . 4 class 10
7 cdiv 11285 . . . 4 class /
82, 6, 7co 7145 . . 3 class (𝐵 / 10)
9 caddc 10528 . . 3 class +
101, 8, 9co 7145 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1528 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dp2eq1  30476  dp2eq2  30477  dp20u  30481  dp20h  30482  dp2cl  30483  dp2clq  30484  rpdp2cl  30485  dp2lt10  30487  dp2lt  30488  dp2ltsuc  30489  dp2ltc  30490  dpval  30493  dpfrac1  30495  dpval2  30496  dpval3  30497  dp3mul10  30501
  Copyright terms: Public domain W3C validator