Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dec GIF version

Definition df-dec 8369
 Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000. (Contributed by Mario Carneiro, 17-Apr-2015.)
Assertion
Ref Expression
df-dec 𝐴𝐵 = ((10 · 𝐴) + 𝐵)

Detailed syntax breakdown of Definition df-dec
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cdc 8368 . 2 class 𝐴𝐵
4 c10 7972 . . . 4 class 10
5 cmul 6894 . . . 4 class ·
64, 1, 5co 5512 . . 3 class (10 · 𝐴)
7 caddc 6892 . . 3 class +
86, 2, 7co 5512 . 2 class ((10 · 𝐴) + 𝐵)
93, 8wceq 1243 1 wff 𝐴𝐵 = ((10 · 𝐴) + 𝐵)
 Colors of variables: wff set class This definition is referenced by:  deceq1  8370  deceq2  8371  decnncl  8380  deccl  8381  dec0u  8382  dec0h  8383  decnncl2  8385  declt  8388  decltc  8389  decsuc  8390  declti  8392  decsucc  8394  dec10p  8396  decma  8405  decmac  8406  decma2c  8407  decadd  8408  decaddc  8409  decmul1c  8414  decmul2c  8415  5t5e25  8443  6t6e36  8448  8t6e48  8459
 Copyright terms: Public domain W3C validator