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