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 29918
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11696. (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 29917 . 2 class 𝐴𝐵
4 c1 10139 . . . . 5 class 1
5 cc0 10138 . . . . 5 class 0
64, 5cdc 11695 . . . 4 class 10
7 cdiv 10886 . . . 4 class /
82, 6, 7co 6793 . . 3 class (𝐵 / 10)
9 caddc 10141 . . 3 class +
101, 8, 9co 6793 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1631 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dfdp2OLD  29919  dp2eq1  29920  dp2eq2  29921  dp20u  29925  dp20h  29926  dp2cl  29927  dp2clq  29928  rpdp2cl  29929  dp2lt10  29931  dp2lt  29932  dp2ltsuc  29933  dp2ltc  29934  dpval  29937  dpfrac1  29939  dpval2  29941  dpval3  29942  dp3mul10  29946
  Copyright terms: Public domain W3C validator