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

Definition df-dec 10121
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 20809. (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 10120 . 2  class ; A B
4 c10 9799 . . . 4  class  10
5 cmul 8738 . . . 4  class  x.
64, 1, 5co 5820 . . 3  class  ( 10  x.  A )
7 caddc 8736 . . 3  class  +
86, 2, 7co 5820 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1624 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10122  deceq1  10123  deceq2  10124  decnncl  10133  deccl  10134  dec0u  10135  dec0h  10136  decnncl2  10138  declt  10141  decltc  10142  decsuc  10143  declti  10145  decsucc  10147  dec10p  10149  decma  10158  decmac  10159  decma2c  10160  decadd  10161  decaddc  10162  decmul1c  10167  decmul2c  10168  5t5e25  10196  6t6e36  10201  8t6e48  10212  dec2dvds  13073  dec5dvds  13074  dec5nprm  13076  dec2nprm  13077  decsplit1  13092  decsplit  13093  bpoly4  24202  dpfrac1  27503
  Copyright terms: Public domain W3C validator