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

Definition df-dec 10214
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 20939. (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 10213 . 2  class ; A B
4 c10 9890 . . . 4  class  10
5 cmul 8829 . . . 4  class  x.
64, 1, 5co 5942 . . 3  class  ( 10  x.  A )
7 caddc 8827 . . 3  class  +
86, 2, 7co 5942 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1642 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10215  deceq1  10216  deceq2  10217  decnncl  10226  deccl  10227  dec0u  10228  dec0h  10229  decnncl2  10231  declt  10234  decltc  10235  decsuc  10236  declti  10238  decsucc  10240  dec10p  10242  decma  10251  decmac  10252  decma2c  10253  decadd  10254  decaddc  10255  decmul1c  10260  decmul2c  10261  5t5e25  10289  6t6e36  10294  8t6e48  10305  dec2dvds  13169  dec5dvds  13170  dec5nprm  13172  dec2nprm  13173  decsplit1  13188  decsplit  13189  bpoly4  25353  dpfrac1  27925
  Copyright terms: Public domain W3C validator