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

Definition df-dec 10308
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 21595. (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 10307 . 2  class ; A B
4 c10 9982 . . . 4  class  10
5 cmul 8921 . . . 4  class  x.
64, 1, 5co 6013 . . 3  class  ( 10  x.  A )
7 caddc 8919 . . 3  class  +
86, 2, 7co 6013 . 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  10309  deceq1  10310  deceq2  10311  decnncl  10320  deccl  10321  dec0u  10322  dec0h  10323  decnncl2  10325  declt  10328  decltc  10329  decsuc  10330  declti  10332  decsucc  10334  dec10p  10336  decma  10345  decmac  10346  decma2c  10347  decadd  10348  decaddc  10349  decmul1c  10354  decmul2c  10355  5t5e25  10383  6t6e36  10388  8t6e48  10399  dec2dvds  13319  dec5dvds  13320  dec5nprm  13322  dec2nprm  13323  decsplit1  13338  decsplit  13339  bpoly4  25812  dpfrac1  27854
  Copyright terms: Public domain W3C validator