Metamath Proof Explorer

Theorem addsubeq4

Description: Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( ( C - A ) = ( B - D ) <-> ( B - D ) = ( C - A ) )
2 subcl 
 |-  ( ( C e. CC /\ A e. CC ) -> ( C - A ) e. CC )
3 2 ancoms 
 |-  ( ( A e. CC /\ C e. CC ) -> ( C - A ) e. CC )
4 subadd 
 |-  ( ( B e. CC /\ D e. CC /\ ( C - A ) e. CC ) -> ( ( B - D ) = ( C - A ) <-> ( D + ( C - A ) ) = B ) )
5 4 3expa 
 |-  ( ( ( B e. CC /\ D e. CC ) /\ ( C - A ) e. CC ) -> ( ( B - D ) = ( C - A ) <-> ( D + ( C - A ) ) = B ) )
6 5 ancoms 
 |-  ( ( ( C - A ) e. CC /\ ( B e. CC /\ D e. CC ) ) -> ( ( B - D ) = ( C - A ) <-> ( D + ( C - A ) ) = B ) )
7 3 6 sylan 
 |-  ( ( ( A e. CC /\ C e. CC ) /\ ( B e. CC /\ D e. CC ) ) -> ( ( B - D ) = ( C - A ) <-> ( D + ( C - A ) ) = B ) )
8 7 an4s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( B - D ) = ( C - A ) <-> ( D + ( C - A ) ) = B ) )
9 1 8 syl5bb 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( C - A ) = ( B - D ) <-> ( D + ( C - A ) ) = B ) )
10 addcom 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C + D ) = ( D + C ) )
11 10 adantl 
 |-  ( ( A e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( C + D ) = ( D + C ) )
12 11 oveq1d 
 |-  ( ( A e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( C + D ) - A ) = ( ( D + C ) - A ) )
13 addsubass 
 |-  ( ( D e. CC /\ C e. CC /\ A e. CC ) -> ( ( D + C ) - A ) = ( D + ( C - A ) ) )
14 13 3com12 
 |-  ( ( C e. CC /\ D e. CC /\ A e. CC ) -> ( ( D + C ) - A ) = ( D + ( C - A ) ) )
15 14 3expa 
 |-  ( ( ( C e. CC /\ D e. CC ) /\ A e. CC ) -> ( ( D + C ) - A ) = ( D + ( C - A ) ) )
16 15 ancoms 
 |-  ( ( A e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( D + C ) - A ) = ( D + ( C - A ) ) )
17 12 16 eqtrd 
 |-  ( ( A e. CC /\ ( C e. CC /\ D e. CC ) ) -> ( ( C + D ) - A ) = ( D + ( C - A ) ) )
18 17 adantlr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( C + D ) - A ) = ( D + ( C - A ) ) )
19 18 eqeq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( C + D ) - A ) = B <-> ( D + ( C - A ) ) = B ) )
20 addcl 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C + D ) e. CC )
21 subadd 
 |-  ( ( ( C + D ) e. CC /\ A e. CC /\ B e. CC ) -> ( ( ( C + D ) - A ) = B <-> ( A + B ) = ( C + D ) ) )
22 21 3expb 
 |-  ( ( ( C + D ) e. CC /\ ( A e. CC /\ B e. CC ) ) -> ( ( ( C + D ) - A ) = B <-> ( A + B ) = ( C + D ) ) )
23 22 ancoms 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C + D ) e. CC ) -> ( ( ( C + D ) - A ) = B <-> ( A + B ) = ( C + D ) ) )
24 20 23 sylan2 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( C + D ) - A ) = B <-> ( A + B ) = ( C + D ) ) )
25 9 19 24 3bitr2rd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) = ( C + D ) <-> ( C - A ) = ( B - D ) ) )