Theorem halfaddsubcl

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

	Ref	Expression
Assertion	halfaddsubcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2		halfcl	⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
3	1 2	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
4		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
5		halfcl	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ )
6	4 5	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ )
7	3 6	jca	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) )