Metamath Proof Explorer


Theorem divsubdir

Description: Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005)

Ref Expression
Assertion divsubdir A B C C 0 A B C = A C B C

Proof

Step Hyp Ref Expression
1 negcl B B
2 divdir A B C C 0 A + B C = A C + B C
3 1 2 syl3an2 A B C C 0 A + B C = A C + B C
4 negsub A B A + B = A B
5 4 oveq1d A B A + B C = A B C
6 5 3adant3 A B C C 0 A + B C = A B C
7 3 6 eqtr3d A B C C 0 A C + B C = A B C
8 divneg B C C 0 B C = B C
9 8 3expb B C C 0 B C = B C
10 9 3adant1 A B C C 0 B C = B C
11 10 oveq2d A B C C 0 A C + B C = A C + B C
12 divcl A C C 0 A C
13 12 3expb A C C 0 A C
14 13 3adant2 A B C C 0 A C
15 divcl B C C 0 B C
16 15 3expb B C C 0 B C
17 16 3adant1 A B C C 0 B C
18 14 17 negsubd A B C C 0 A C + B C = A C B C
19 11 18 eqtr3d A B C C 0 A C + B C = A C B C
20 7 19 eqtr3d A B C C 0 A B C = A C B C