Metamath Proof Explorer


Theorem div2subd

Description: Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses div2subd.1
|- ( ph -> A e. CC )
div2subd.2
|- ( ph -> B e. CC )
div2subd.3
|- ( ph -> C e. CC )
div2subd.4
|- ( ph -> D e. CC )
div2subd.5
|- ( ph -> C =/= D )
Assertion div2subd
|- ( ph -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )

Proof

Step Hyp Ref Expression
1 div2subd.1
 |-  ( ph -> A e. CC )
2 div2subd.2
 |-  ( ph -> B e. CC )
3 div2subd.3
 |-  ( ph -> C e. CC )
4 div2subd.4
 |-  ( ph -> D e. CC )
5 div2subd.5
 |-  ( ph -> C =/= D )
6 div2sub
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
7 1 2 3 4 5 6 syl23anc
 |-  ( ph -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )