Metamath Proof Explorer

Theorem nnpcan

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

Ref Expression
Assertion nnpcan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B - C + B = A − C

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 1 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B ∈ ℂ
3 addsub ⊢ A − B ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − B - C + B
4 3 eqcomd ⊢ A − B ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B - C + B = A − B + B - C
5 2 4 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B - C + B = A − B + B - C
6 npcan ⊢ A ∈ ℂ ∧ B ∈ ℂ → A - B + B = A
7 6 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B + B = A
8 7 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B + B - C = A − C
9 5 8 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B - C + B = A − C