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 ) ) = 𝐵 ) )