Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsubass Structured version   Visualization version   GIF version

 Description: Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
addsubass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵𝐶)))

StepHypRef Expression
1 simp1 1081 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐴 ∈ ℂ)
2 subcl 10318 . . . . . 6 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵𝐶) ∈ ℂ)
323adant1 1099 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵𝐶) ∈ ℂ)
4 simp3 1083 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐶 ∈ ℂ)
51, 3, 4addassd 10100 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + (𝐵𝐶)) + 𝐶) = (𝐴 + ((𝐵𝐶) + 𝐶)))
6 npcan 10328 . . . . . 6 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵𝐶) + 𝐶) = 𝐵)
763adant1 1099 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵𝐶) + 𝐶) = 𝐵)
87oveq2d 6706 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + ((𝐵𝐶) + 𝐶)) = (𝐴 + 𝐵))
95, 8eqtrd 2685 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + (𝐵𝐶)) + 𝐶) = (𝐴 + 𝐵))
109oveq1d 6705 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 + (𝐵𝐶)) + 𝐶) − 𝐶) = ((𝐴 + 𝐵) − 𝐶))
111, 3addcld 10097 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵𝐶)) ∈ ℂ)
12 pncan 10325 . . 3 (((𝐴 + (𝐵𝐶)) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 + (𝐵𝐶)) + 𝐶) − 𝐶) = (𝐴 + (𝐵𝐶)))
1311, 4, 12syl2anc 694 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 + (𝐵𝐶)) + 𝐶) − 𝐶) = (𝐴 + (𝐵𝐶)))
1410, 13eqtr3d 2687 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵𝐶)))