Metamath Proof Explorer

Theorem div2sub

Description: Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion div2sub 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 subcl 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C - D ) e. CC )
3 2 3adant3 
 |-  ( ( C e. CC /\ D e. CC /\ C =/= D ) -> ( C - D ) e. CC )
4 subeq0 
 |-  ( ( C e. CC /\ D e. CC ) -> ( ( C - D ) = 0 <-> C = D ) )
5 4 necon3bid 
 |-  ( ( C e. CC /\ D e. CC ) -> ( ( C - D ) =/= 0 <-> C =/= D ) )
6 5 biimp3ar 
 |-  ( ( C e. CC /\ D e. CC /\ C =/= D ) -> ( C - D ) =/= 0 )
7 3 6 jca 
 |-  ( ( C e. CC /\ D e. CC /\ C =/= D ) -> ( ( C - D ) e. CC /\ ( C - D ) =/= 0 ) )
8 div2neg 
 |-  ( ( ( A - B ) e. CC /\ ( C - D ) e. CC /\ ( C - D ) =/= 0 ) -> ( -u ( A - B ) / -u ( C - D ) ) = ( ( A - B ) / ( C - D ) ) )
9 8 3expb 
 |-  ( ( ( A - B ) e. CC /\ ( ( C - D ) e. CC /\ ( C - D ) =/= 0 ) ) -> ( -u ( A - B ) / -u ( C - D ) ) = ( ( A - B ) / ( C - D ) ) )
10 1 7 9 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( -u ( A - B ) / -u ( C - D ) ) = ( ( A - B ) / ( C - D ) ) )
11 negsubdi2 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
12 negsubdi2 
 |-  ( ( C e. CC /\ D e. CC ) -> -u ( C - D ) = ( D - C ) )
13 12 3adant3 
 |-  ( ( C e. CC /\ D e. CC /\ C =/= D ) -> -u ( C - D ) = ( D - C ) )
14 11 13 oveqan12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( -u ( A - B ) / -u ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
15 10 14 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )