Metamath Proof Explorer

Theorem halfaddsub

Description: Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007)

Ref Expression
Assertion halfaddsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A ∧ A + B 2 − A − B 2 = B

Proof

Step Hyp Ref Expression
1 ppncan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A ∈ ℂ → A + B + A − B = A + A
2 1 3anidm13 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A − B = A + A
3 2times ⊢ A ∈ ℂ → 2 ⁢ A = A + A
4 3 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ A = A + A
5 2 4 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A − B = 2 ⁢ A
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A − B 2 = 2 ⁢ A 2
7 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
8 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
9 2cnne0 ⊢ 2 ∈ ℂ ∧ 2 ≠ 0
10 divdir ⊢ A + B ∈ ℂ ∧ A − B ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → A + B + A − B 2 = A + B 2 + A − B 2
11 9 10 mp3an3 ⊢ A + B ∈ ℂ ∧ A − B ∈ ℂ → A + B + A − B 2 = A + B 2 + A − B 2
12 7 8 11 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A − B 2 = A + B 2 + A − B 2
13 2cn ⊢ 2 ∈ ℂ
14 2ne0 ⊢ 2 ≠ 0
15 divcan3 ⊢ A ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → 2 ⁢ A 2 = A
16 13 14 15 mp3an23 ⊢ A ∈ ℂ → 2 ⁢ A 2 = A
17 16 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ A 2 = A
18 6 12 17 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A
19 pnncan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ∈ ℂ → A + B - A − B = B + B
20 19 3anidm23 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A − B = B + B
21 2times ⊢ B ∈ ℂ → 2 ⁢ B = B + B
22 21 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ B = B + B
23 20 22 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A − B = 2 ⁢ B
24 23 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A − B 2 = 2 ⁢ B 2
25 divsubdir ⊢ A + B ∈ ℂ ∧ A − B ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → A + B - A − B 2 = A + B 2 − A − B 2
26 9 25 mp3an3 ⊢ A + B ∈ ℂ ∧ A − B ∈ ℂ → A + B - A − B 2 = A + B 2 − A − B 2
27 7 8 26 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A − B 2 = A + B 2 − A − B 2
28 divcan3 ⊢ B ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → 2 ⁢ B 2 = B
29 13 14 28 mp3an23 ⊢ B ∈ ℂ → 2 ⁢ B 2 = B
30 29 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ B 2 = B
31 24 27 30 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 − A − B 2 = B
32 18 31 jca ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A ∧ A + B 2 − A − B 2 = B