This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addsubass

Description: Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion addsubass ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐶 ) = ( 𝐴 + ( 𝐵 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
2 subcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
3 2 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
4 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
5 1 3 4 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) + 𝐶 ) = ( 𝐴 + ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) )
6 npcan ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + 𝐶 ) = 𝐵 )
7 6 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) + 𝐶 ) = 𝐵 )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( ( 𝐵 − 𝐶 ) + 𝐶 ) ) = ( 𝐴 + 𝐵 ) )
9 5 8 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) + 𝐶 ) = ( 𝐴 + 𝐵 ) )
10 9 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) + 𝐶 ) − 𝐶 ) = ( ( 𝐴 + 𝐵 ) − 𝐶 ) )
11 1 3 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( 𝐵 − 𝐶 ) ) ∈ ℂ )
12 pncan ⊢ ( ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) + 𝐶 ) − 𝐶 ) = ( 𝐴 + ( 𝐵 − 𝐶 ) ) )
13 11 4 12 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + ( 𝐵 − 𝐶 ) ) + 𝐶 ) − 𝐶 ) = ( 𝐴 + ( 𝐵 − 𝐶 ) ) )
14 10 13 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐶 ) = ( 𝐴 + ( 𝐵 − 𝐶 ) ) )