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+B2+A−B2=A∧A+B2−A−B2=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−B2=2⁢A2
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−B2=A+B2+A−B2
11 9 10 mp3an3 ⊢A+B∈ℂ∧A−B∈ℂ→A+B+A−B2=A+B2+A−B2
12 7 8 11 syl2anc ⊢A∈ℂ∧B∈ℂ→A+B+A−B2=A+B2+A−B2
13 2cn ⊢2∈ℂ
14 2ne0 ⊢2≠0
15 divcan3 ⊢A∈ℂ∧2∈ℂ∧2≠0→2⁢A2=A
16 13 14 15 mp3an23 ⊢A∈ℂ→2⁢A2=A
17 16 adantr ⊢A∈ℂ∧B∈ℂ→2⁢A2=A
18 6 12 17 3eqtr3d ⊢A∈ℂ∧B∈ℂ→A+B2+A−B2=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−B2=2⁢B2
25 divsubdir ⊢A+B∈ℂ∧A−B∈ℂ∧2∈ℂ∧2≠0→A+B-A−B2=A+B2−A−B2
26 9 25 mp3an3 ⊢A+B∈ℂ∧A−B∈ℂ→A+B-A−B2=A+B2−A−B2
27 7 8 26 syl2anc ⊢A∈ℂ∧B∈ℂ→A+B-A−B2=A+B2−A−B2
28 divcan3 ⊢B∈ℂ∧2∈ℂ∧2≠0→2⁢B2=B
29 13 14 28 mp3an23 ⊢B∈ℂ→2⁢B2=B
30 29 adantl ⊢A∈ℂ∧B∈ℂ→2⁢B2=B
31 24 27 30 3eqtr3d ⊢A∈ℂ∧B∈ℂ→A+B2−A−B2=B
32 18 31 jca ⊢A∈ℂ∧B∈ℂ→A+B2+A−B2=A∧A+B2−A−B2=B