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

Definition df-dec 10383
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 21754. (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 10382 . 2  class ; A B
4 c10 10057 . . . 4  class  10
5 cmul 8995 . . . 4  class  x.
64, 1, 5co 6081 . . 3  class  ( 10  x.  A )
7 caddc 8993 . . 3  class  +
86, 2, 7co 6081 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1652 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10384  deceq1  10385  deceq2  10386  decnncl  10395  deccl  10396  dec0u  10397  dec0h  10398  decnncl2  10400  declt  10403  decltc  10404  decsuc  10405  declti  10407  decsucc  10409  dec10p  10411  decma  10420  decmac  10421  decma2c  10422  decadd  10423  decaddc  10424  decmul1c  10429  decmul2c  10430  5t5e25  10458  6t6e36  10463  8t6e48  10474  dec2dvds  13399  dec5dvds  13400  dec5nprm  13402  dec2nprm  13403  decsplit1  13418  decsplit  13419  bpoly4  26105  dpfrac1  28515
  Copyright terms: Public domain W3C validator