Metamath Proof Explorer

Theorem xaddcl

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddcl 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )

Proof

Step Hyp Ref Expression
1 xaddf 
 |-  +e : ( RR* X. RR* ) --> RR*
2 1 fovcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )