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

Metamath Proof Explorer

Theorem addsubeq4

Description: Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion addsubeq4 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ↔ ( 𝐶 − 𝐴 ) = ( 𝐵 − 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 eqcom ⊢ ( ( 𝐶 − 𝐴 ) = ( 𝐵 − 𝐷 ) ↔ ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) )
2 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
3 2 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
4 subadd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
5 4 3expa ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
6 5 ancoms ⊢ ( ( ( 𝐶 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
7 3 6 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
8 7 an4s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐴 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
9 1 8 bitrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 − 𝐴 ) = ( 𝐵 − 𝐷 ) ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
10 addcom ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
12 11 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 + 𝐷 ) − 𝐴 ) = ( ( 𝐷 + 𝐶 ) − 𝐴 ) )
13 addsubass ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐷 + 𝐶 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
14 13 3com12 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐷 + 𝐶 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
15 14 3expa ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐷 + 𝐶 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
16 15 ancoms ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐷 + 𝐶 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
17 12 16 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 + 𝐷 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
18 17 adantlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐶 + 𝐷 ) − 𝐴 ) = ( 𝐷 + ( 𝐶 − 𝐴 ) ) )
19 18 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐶 + 𝐷 ) − 𝐴 ) = 𝐵 ↔ ( 𝐷 + ( 𝐶 − 𝐴 ) ) = 𝐵 ) )
20 addcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 + 𝐷 ) ∈ ℂ )
21 subadd ⊢ ( ( ( 𝐶 + 𝐷 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐶 + 𝐷 ) − 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) )
22 21 3expb ⊢ ( ( ( 𝐶 + 𝐷 ) ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( ( 𝐶 + 𝐷 ) − 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) )
23 22 ancoms ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 + 𝐷 ) ∈ ℂ ) → ( ( ( 𝐶 + 𝐷 ) − 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) )
24 20 23 sylan2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐶 + 𝐷 ) − 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) )
25 9 19 24 3bitr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ↔ ( 𝐶 − 𝐴 ) = ( 𝐵 − 𝐷 ) ) )