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 e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) )

Proof

Step Hyp Ref Expression
1 addcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 halfcl
 |-  ( ( A + B ) e. CC -> ( ( A + B ) / 2 ) e. CC )
3 1 2 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) / 2 ) e. CC )
4 subcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
5 halfcl
 |-  ( ( A - B ) e. CC -> ( ( A - B ) / 2 ) e. CC )
6 4 5 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) / 2 ) e. CC )
7 3 6 jca
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) )