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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐴 ∧ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐵 ) )

Proof

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