Metamath Proof Explorer

Theorem cnambpcma

Description: ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - B ) e. CC )
3 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
4 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
5 2 3 4 addsubd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) - A ) = ( ( ( A - B ) - A ) + C ) )
6 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
7 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
8 6 7 6 3jca 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A e. CC /\ B e. CC /\ A e. CC ) )
9 8 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A e. CC /\ B e. CC /\ A e. CC ) )
10 sub32 
 |-  ( ( A e. CC /\ B e. CC /\ A e. CC ) -> ( ( A - B ) - A ) = ( ( A - A ) - B ) )
11 9 10 syl 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) - A ) = ( ( A - A ) - B ) )
12 11 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) - A ) + C ) = ( ( ( A - A ) - B ) + C ) )
13 subcl 
 |-  ( ( A e. CC /\ A e. CC ) -> ( A - A ) e. CC )
14 13 anidms 
 |-  ( A e. CC -> ( A - A ) e. CC )
15 14 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - A ) e. CC )
16 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
17 15 16 3 subadd23d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - A ) - B ) + C ) = ( ( A - A ) + ( C - B ) ) )
18 subid 
 |-  ( A e. CC -> ( A - A ) = 0 )
19 18 oveq1d 
 |-  ( A e. CC -> ( ( A - A ) + ( C - B ) ) = ( 0 + ( C - B ) ) )
20 19 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - A ) + ( C - B ) ) = ( 0 + ( C - B ) ) )
21 subcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C - B ) e. CC )
22 21 ancoms 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C - B ) e. CC )
23 22 addlidd 
 |-  ( ( B e. CC /\ C e. CC ) -> ( 0 + ( C - B ) ) = ( C - B ) )
24 23 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( 0 + ( C - B ) ) = ( C - B ) )
25 17 20 24 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - A ) - B ) + C ) = ( C - B ) )
26 5 12 25 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A - B ) + C ) - A ) = ( C - B ) )