Metamath Proof Explorer


Theorem subdi

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

Ref Expression
Assertion subdi ABCABC=ABAC

Proof

Step Hyp Ref Expression
1 simp1 ABCA
2 simp3 ABCC
3 subcl BCBC
4 3 3adant1 ABCBC
5 1 2 4 adddid ABCAC+B-C=AC+ABC
6 pncan3 CBC+B-C=B
7 6 ancoms BCC+B-C=B
8 7 3adant1 ABCC+B-C=B
9 8 oveq2d ABCAC+B-C=AB
10 5 9 eqtr3d ABCAC+ABC=AB
11 mulcl ABAB
12 11 3adant3 ABCAB
13 mulcl ACAC
14 13 3adant2 ABCAC
15 mulcl ABCABC
16 3 15 sylan2 ABCABC
17 16 3impb ABCABC
18 12 14 17 subaddd ABCABAC=ABCAC+ABC=AB
19 10 18 mpbird ABCABAC=ABC
20 19 eqcomd ABCABC=ABAC