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 32577
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12700. (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 32576 . 2 class 𝐴𝐵
4 c1 11131 . . . . 5 class 1
5 cc0 11130 . . . . 5 class 0
64, 5cdc 12699 . . . 4 class 10
7 cdiv 11893 . . . 4 class /
82, 6, 7co 7414 . . 3 class (𝐵 / 10)
9 caddc 11133 . . 3 class +
101, 8, 9co 7414 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1534 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dp2eq1  32578  dp2eq2  32579  dp20u  32583  dp20h  32584  dp2cl  32585  dp2clq  32586  rpdp2cl  32587  dp2lt10  32589  dp2lt  32590  dp2ltsuc  32591  dp2ltc  32592  dpval  32595  dpfrac1  32597  dpval2  32598  dpval3  32599  dp3mul10  32603
  Copyright terms: Public domain W3C validator