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 ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + C - A = C − B

Proof

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