Metamath Proof Explorer


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 ) ∈ ℂ ) )