MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dec Unicode version

Definition df-dec 10125
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example,  (;;; 1 0 0 0  + ;;; 2 0 0 0 )  = ;;; 3 0 0 0 1kp2ke3k 20833. (Contributed by Mario Carneiro, 17-Apr-2015.)
Assertion
Ref Expression
df-dec  |- ; A B  =  ( ( 10  x.  A
)  +  B )

Detailed syntax breakdown of Definition df-dec
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cdc 10124 . 2  class ; A B
4 c10 9803 . . . 4  class  10
5 cmul 8742 . . . 4  class  x.
64, 1, 5co 5858 . . 3  class  ( 10  x.  A )
7 caddc 8740 . . 3  class  +
86, 2, 7co 5858 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1623 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10126  deceq1  10127  deceq2  10128  decnncl  10137  deccl  10138  dec0u  10139  dec0h  10140  decnncl2  10142  declt  10145  decltc  10146  decsuc  10147  declti  10149  decsucc  10151  dec10p  10153  decma  10162  decmac  10163  decma2c  10164  decadd  10165  decaddc  10166  decmul1c  10171  decmul2c  10172  5t5e25  10200  6t6e36  10205  8t6e48  10216  dec2dvds  13078  dec5dvds  13079  dec5nprm  13081  dec2nprm  13082  decsplit1  13097  decsplit  13098  bpoly4  24794  dpfrac1  28242
  Copyright terms: Public domain W3C validator