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

Definition df-dec 10141
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 20849. (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 10140 . 2  class ; A B
4 c10 9819 . . . 4  class  10
5 cmul 8758 . . . 4  class  x.
64, 1, 5co 5874 . . 3  class  ( 10  x.  A )
7 caddc 8756 . . 3  class  +
86, 2, 7co 5874 . 2  class  ( ( 10  x.  A )  +  B )
93, 8wceq 1632 1  wff ; A B  =  ( ( 10  x.  A
)  +  B )
Colors of variables: wff set class
This definition is referenced by:  decex  10142  deceq1  10143  deceq2  10144  decnncl  10153  deccl  10154  dec0u  10155  dec0h  10156  decnncl2  10158  declt  10161  decltc  10162  decsuc  10163  declti  10165  decsucc  10167  dec10p  10169  decma  10178  decmac  10179  decma2c  10180  decadd  10181  decaddc  10182  decmul1c  10187  decmul2c  10188  5t5e25  10216  6t6e36  10221  8t6e48  10232  dec2dvds  13094  dec5dvds  13095  dec5nprm  13097  dec2nprm  13098  decsplit1  13113  decsplit  13114  bpoly4  24865  dpfrac1  28495
  Copyright terms: Public domain W3C validator