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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( 𝐶 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
3		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
4		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
5	2 3 4	addsubd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( ( ( 𝐴 − 𝐵 ) − 𝐴 ) + 𝐶 ) )
6		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
7		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
8	6 7 6	3jca	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
9	8	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
10		sub32	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − 𝐴 ) = ( ( 𝐴 − 𝐴 ) − 𝐵 ) )
11	9 10	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − 𝐴 ) = ( ( 𝐴 − 𝐴 ) − 𝐵 ) )
12	11	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) − 𝐴 ) + 𝐶 ) = ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) )
13		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 − 𝐴 ) ∈ ℂ )
14	13	anidms	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) ∈ ℂ )
15	14	3ad2ant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐴 ) ∈ ℂ )
16		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
17	15 16 3	subadd23d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) = ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) )
18		subid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
19	18	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) = ( 0 + ( 𝐶 − 𝐵 ) ) )
20	19	3ad2ant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐴 ) + ( 𝐶 − 𝐵 ) ) = ( 0 + ( 𝐶 − 𝐵 ) ) )
21		subcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
22	21	ancoms	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
23	22	addid2d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 + ( 𝐶 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
24	23	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 + ( 𝐶 − 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
25	17 20 24	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐴 ) − 𝐵 ) + 𝐶 ) = ( 𝐶 − 𝐵 ) )
26	5 12 25	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 − 𝐵 ) + 𝐶 ) − 𝐴 ) = ( 𝐶 − 𝐵 ) )