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