Theorem halfaddsubcl

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

	Ref	Expression
Assertion	halfaddsubcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\frac{A+B}{2}\in ℂ\wedge \frac{A-B}{2}\in ℂ\right)$$

Proof

Step	Hyp	Ref	Expression
1		addcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ$$
2		halfcl	$$⊢A+B\in ℂ\to \frac{A+B}{2}\in ℂ$$
3	1 2	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{A+B}{2}\in ℂ$$
4		subcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A-B\in ℂ$$
5		halfcl	$$⊢A-B\in ℂ\to \frac{A-B}{2}\in ℂ$$
6	4 5	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{A-B}{2}\in ℂ$$
7	3 6	jca	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\frac{A+B}{2}\in ℂ\wedge \frac{A-B}{2}\in ℂ\right)$$