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 ) ) )