This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem halfaddsubcl

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

Ref Expression
Assertion halfaddsubcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ

Proof

Step Hyp Ref Expression
1 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
2 halfcl ⊢ A + B ∈ ℂ → A + B 2 ∈ ℂ
3 1 2 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ
4 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
5 halfcl ⊢ A − B ∈ ℂ → A − B 2 ∈ ℂ
6 4 5 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B 2 ∈ ℂ
7 3 6 jca ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ