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

Definition df-dp2 27599
Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 10125. (Contributed by David A. Wheeler, 15-May-2015.)
Assertion
Ref Expression
df-dp2  |- _ A B  =  ( A  +  ( B  /  10 ) )

Detailed syntax breakdown of Definition df-dp2
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cdp2 27597 . 2  class _ A B
4 c10 9803 . . . 4  class  10
5 cdiv 9423 . . . 4  class  /
62, 4, 5co 5858 . . 3  class  ( B  /  10 )
7 caddc 8740 . . 3  class  +
81, 6, 7co 5858 . 2  class  ( A  +  ( B  /  10 ) )
93, 8wceq 1623 1  wff _ A B  =  ( A  +  ( B  /  10 ) )
Colors of variables: wff set class
This definition is referenced by:  dp2cl  27601  dpval  27602  dpfrac1  27604
  Copyright terms: Public domain W3C validator