Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dp2 Structured version   Visualization version   GIF version

Definition df-dp2 42306
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11370. (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 42304 . 2 class 𝐴𝐵
4 c1 9816 . . . . 5 class 1
5 cc0 9815 . . . . 5 class 0
64, 5cdc 11369 . . . 4 class 10
7 cdiv 10563 . . . 4 class /
82, 6, 7co 6549 . . 3 class (𝐵 / 10)
9 caddc 9818 . . 3 class +
101, 8, 9co 6549 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1475 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dfdp2OLD  42307  dp2cl  42309  dpval  42310  dpfrac1  42312
  Copyright terms: Public domain W3C validator