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 φA0+∞
xrge0subcld.b φB0+∞
xrge0subcld.c φBA
Assertion xrge0subcld φA+𝑒B0+∞

Proof

Step Hyp Ref Expression
1 xrge0subcld.a φA0+∞
2 xrge0subcld.b φB0+∞
3 xrge0subcld.c φBA
4 iccssxr 0+∞*
5 4 1 sselid φA*
6 4 2 sselid φB*
7 6 xnegcld φB*
8 5 7 xaddcld φA+𝑒B*
9 xsubge0 A*B*0A+𝑒BBA
10 5 6 9 syl2anc φ0A+𝑒BBA
11 3 10 mpbird φ0A+𝑒B
12 8 11 jca φA+𝑒B*0A+𝑒B
13 elxrge0 A+𝑒B0+∞A+𝑒B*0A+𝑒B
14 12 13 sylibr φA+𝑒B0+∞