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