Metamath Proof Explorer

Theorem addsubeq4

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

Ref Expression
Assertion addsubeq4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B = C + D ↔ C − A = B − D

Proof

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