Metamath Proof Explorer

Theorem addsub4

Description: Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC )
2 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
3 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
4 addsub 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )
5 1 2 3 4 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )
6 5 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) - D ) = ( ( ( A - C ) + B ) - D ) )
7 1 2 addcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A + B ) e. CC )
8 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC )
9 subsub4 
 |-  ( ( ( A + B ) e. CC /\ C e. CC /\ D e. CC ) -> ( ( ( A + B ) - C ) - D ) = ( ( A + B ) - ( C + D ) ) )
10 7 3 8 9 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) - D ) = ( ( A + B ) - ( C + D ) ) )
11 subcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC )
12 11 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A - C ) e. CC )
13 addsubass 
 |-  ( ( ( A - C ) e. CC /\ B e. CC /\ D e. CC ) -> ( ( ( A - C ) + B ) - D ) = ( ( A - C ) + ( B - D ) ) )
14 12 2 8 13 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A - C ) + B ) - D ) = ( ( A - C ) + ( B - D ) ) )
15 6 10 14 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) ) )