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

Definition df-dec 11005
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, 1kp2ke3k 25167. (Contributed by Mario Carneiro, 17-Apr-2015.)
Assertion
Ref Expression
df-dec No typesetting for: |- ; A B = ( ( 10 x. A ) + B )

Detailed syntax breakdown of Definition df-dec
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cdc 11004 . 2 No typesetting for: class ; A B
4 c10 10618 . . . 4
5 cmul 9518 . . . 4
64, 1, 5co 6296 . . 3
7 caddc 9516 . . 3
86, 2, 7co 6296 . 2
93, 8wceq 1395 1 No typesetting for: wff ; A B = ( ( 10 x. A ) + B )
Colors of variables: wff setvar class
This definition is referenced by:  decex  11006  deceq1  11007  deceq2  11008  decnncl  11017  deccl  11018  dec0u  11019  dec0h  11020  decnncl2  11022  declt  11025  decltc  11026  decsuc  11027  declti  11029  decsucc  11031  dec10p  11033  decma  11042  decmac  11043  decma2c  11044  decadd  11045  decaddc  11046  decmul1c  11051  decmul2c  11052  5t5e25  11080  6t6e36  11085  8t6e48  11096  dec2dvds  14549  dec5dvds  14550  dec5nprm  14552  dec2nprm  14553  decsplit1  14568  decsplit  14569  bpoly4  29821  dpfrac1  33166
  Copyright terms: Public domain W3C validator