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 42265
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 11322. (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 42263 . 2 class 𝐴𝐵
4 c1 9789 . . . . 5 class 1
5 cc0 9788 . . . . 5 class 0
64, 5cdc 11321 . . . 4 class 10
7 cdiv 10529 . . . 4 class /
82, 6, 7co 6523 . . 3 class (𝐵 / 10)
9 caddc 9791 . . 3 class +
101, 8, 9co 6523 . 2 class (𝐴 + (𝐵 / 10))
113, 10wceq 1474 1 wff 𝐴𝐵 = (𝐴 + (𝐵 / 10))
Colors of variables: wff setvar class
This definition is referenced by:  dfdp2OLD  42266  dp2cl  42268  dpval  42269  dpfrac1  42271
  Copyright terms: Public domain W3C validator