Theorem ge0xaddcl

Description: The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	ge0xaddcl	|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) -> ( A +e B ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		elxrge0	|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )
2		elxrge0	|- ( B e. ( 0 [,] +oo ) <-> ( B e. RR* /\ 0 <_ B ) )
3		xaddcl	|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
4	3	ad2ant2r	|- ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( A +e B ) e. RR* )
5		xaddge0	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A +e B ) )
6	5	an4s	|- ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> 0 <_ ( A +e B ) )
7		elxrge0	|- ( ( A +e B ) e. ( 0 [,] +oo ) <-> ( ( A +e B ) e. RR* /\ 0 <_ ( A +e B ) ) )
8	4 6 7	sylanbrc	|- ( ( ( A e. RR* /\ 0 <_ A ) /\ ( B e. RR* /\ 0 <_ B ) ) -> ( A +e B ) e. ( 0 [,] +oo ) )
9	1 2 8	syl2anb	|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) -> ( A +e B ) e. ( 0 [,] +oo ) )