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 30541
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12091. (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 30540 . 2 class 𝐴𝐵
4 c1 10530 . . . . 5 class 1
5 cc0 10529 . . . . 5 class 0
64, 5cdc 12090 . . . 4 class 10
7 cdiv 11289 . . . 4 class /
82, 6, 7co 7148 . . 3 class (𝐵 / 10)
9 caddc 10532 . . 3 class +
101, 8, 9co 7148 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1530 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dp2eq1  30542  dp2eq2  30543  dp20u  30547  dp20h  30548  dp2cl  30549  dp2clq  30550  rpdp2cl  30551  dp2lt10  30553  dp2lt  30554  dp2ltsuc  30555  dp2ltc  30556  dpval  30559  dpfrac1  30561  dpval2  30562  dpval3  30563  dp3mul10  30567
  Copyright terms: Public domain W3C validator