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

Definition df-dec 10339
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 21707. (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 10338 . 2  class ; A B
4 c10 10013 . . . 4  class  10
5 cmul 8951 . . . 4  class  x.
64, 1, 5co 6040 . . 3  class  ( 10  x.  A )
7 caddc 8949 . . 3  class  +
86, 2, 7co 6040 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1649 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10340  deceq1  10341  deceq2  10342  decnncl  10351  deccl  10352  dec0u  10353  dec0h  10354  decnncl2  10356  declt  10359  decltc  10360  decsuc  10361  declti  10363  decsucc  10365  dec10p  10367  decma  10376  decmac  10377  decma2c  10378  decadd  10379  decaddc  10380  decmul1c  10385  decmul2c  10386  5t5e25  10414  6t6e36  10419  8t6e48  10430  dec2dvds  13354  dec5dvds  13355  dec5nprm  13357  dec2nprm  13358  decsplit1  13373  decsplit  13374  bpoly4  26009  dpfrac1  28229
  Copyright terms: Public domain W3C validator