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