This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid 
 |-  ( ph -> A e. RR* )
6 4 2 sselid 
 |-  ( 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 ) )