Metamath Proof Explorer

Theorem nnncan1

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
2 1 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C ∈ ℂ
3 sub32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A − C ∈ ℂ → A - B - A − C = A - A − C - B
4 2 3 syld3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B - A − C = A - A − C - B
5 nncan ⊢ A ∈ ℂ ∧ C ∈ ℂ → A − A − C = C
6 5 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − A − C = C
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - A − C - B = C − B
8 4 7 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B - A − C = C − B