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

Definition df-dec 8367
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 8366 . 2 class 𝐴𝐵
4 c10 7970 . . . 4 class 10
5 cmul 6892 . . . 4 class ·
64, 1, 5co 5512 . . 3 class (10 · 𝐴)
7 caddc 6890 . . 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  8368  deceq2  8369  decnncl  8378  deccl  8379  dec0u  8380  dec0h  8381  decnncl2  8383  declt  8386  decltc  8387  decsuc  8388  declti  8390  decsucc  8392  dec10p  8394  decma  8403  decmac  8404  decma2c  8405  decadd  8406  decaddc  8407  decmul1c  8412  decmul2c  8413  5t5e25  8441  6t6e36  8446  8t6e48  8457
  Copyright terms: Public domain W3C validator