Metamath Proof Explorer


Theorem mulsubaddmulsub

Description: A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

Ref Expression
Assertion mulsubaddmulsub A B C D B C A + B C D = A D + B D - A C

Proof

Step Hyp Ref Expression
1 simplr A B C D B
2 simprl A B C D C
3 1 2 mulcld A B C D B C
4 subaddmulsub A B C D B C B C A + B C D = B C - A C - B C + A D + B D
5 3 4 mpd3an3 A B C D B C A + B C D = B C - A C - B C + A D + B D
6 simpll A B C D A
7 6 2 mulcld A B C D A C
8 3 7 3 sub32d A B C D B C - A C - B C = B C - B C - A C
9 3 subidd A B C D B C B C = 0
10 9 oveq1d A B C D B C - B C - A C = 0 A C
11 8 10 eqtrd A B C D B C - A C - B C = 0 A C
12 df-neg A C = 0 A C
13 11 12 eqtr4di A B C D B C - A C - B C = A C
14 13 oveq1d A B C D B C - A C - B C + A D + B D = A C + A D + B D
15 7 negcld A B C D A C
16 simprr A B C D D
17 6 16 mulcld A B C D A D
18 1 16 mulcld A B C D B D
19 17 18 addcld A B C D A D + B D
20 15 19 addcomd A B C D A C + A D + B D = A D + B D + A C
21 19 7 negsubd A B C D A D + B D + A C = A D + B D - A C
22 20 21 eqtrd A B C D A C + A D + B D = A D + B D - A C
23 14 22 eqtrd A B C D B C - A C - B C + A D + B D = A D + B D - A C
24 5 23 eqtrd A B C D B C A + B C D = A D + B D - A C