Theorem xrge0subcld

Description: Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020)

	Ref	Expression
Hypotheses	xrge0subcld.a	|- ( ph -> A e. ( 0 [,] +oo ) )
	xrge0subcld.b	|- ( ph -> B e. ( 0 [,] +oo ) )
	xrge0subcld.c	|- ( ph -> B <_ A )
Assertion	xrge0subcld	|- ( ph -> ( A +e -e B ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0subcld.a	|- ( ph -> A e. ( 0 [,] +oo ) )
2		xrge0subcld.b	|- ( ph -> B e. ( 0 [,] +oo ) )
3		xrge0subcld.c	|- ( ph -> B <_ A )
4		iccssxr	|- ( 0 [,] +oo ) C_ RR*
5	4 1	sseldi	|- ( ph -> A e. RR* )
6	4 2	sseldi	|- ( ph -> B e. RR* )
7	6	xnegcld	|- ( ph -> -e B e. RR* )
8	5 7	xaddcld	|- ( ph -> ( A +e -e B ) e. RR* )
9		xsubge0	|- ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
10	5 6 9	syl2anc	|- ( ph -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
11	3 10	mpbird	|- ( ph -> 0 <_ ( A +e -e B ) )
12	8 11	jca	|- ( ph -> ( ( A +e -e B ) e. RR* /\ 0 <_ ( A +e -e B ) ) )
13		elxrge0	|- ( ( A +e -e B ) e. ( 0 [,] +oo ) <-> ( ( A +e -e B ) e. RR* /\ 0 <_ ( A +e -e B ) ) )
14	12 13	sylibr	|- ( ph -> ( A +e -e B ) e. ( 0 [,] +oo ) )