Metamath Proof Explorer


Theorem subdir

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 30-Dec-2005)

Ref Expression
Assertion subdir ABCABC=ACBC

Proof

Step Hyp Ref Expression
1 subdi CABCAB=CACB
2 1 3coml ABCCAB=CACB
3 subcl ABAB
4 mulcom ABCABC=CAB
5 3 4 stoic3 ABCABC=CAB
6 mulcom ACAC=CA
7 6 3adant2 ABCAC=CA
8 mulcom BCBC=CB
9 8 3adant1 ABCBC=CB
10 7 9 oveq12d ABCACBC=CACB
11 2 5 10 3eqtr4d ABCABC=ACBC