This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subeqrev

Description: Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013)

Ref Expression
Assertion subeqrev 
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( 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 neg11 
 |-  ( ( ( A - B ) e. CC /\ ( C - D ) e. CC ) -> ( -u ( A - B ) = -u ( C - D ) <-> ( A - B ) = ( C - D ) ) )
4 1 2 3 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A - B ) = -u ( C - D ) <-> ( A - B ) = ( C - D ) ) )
5 negsubdi2 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A - B ) = ( B - A ) )
6 negsubdi2 
 |-  ( ( C e. CC /\ D e. CC ) -> -u ( C - D ) = ( D - C ) )
7 5 6 eqeqan12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( -u ( A - B ) = -u ( C - D ) <-> ( B - A ) = ( D - C ) ) )
8 4 7 bitr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) = ( C - D ) <-> ( B - A ) = ( D - C ) ) )