Description: Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrge0subcld.a | |
|
xrge0subcld.b | |
||
xrge0subcld.c | |
||
Assertion | xrge0subcld | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrge0subcld.a | |
|
2 | xrge0subcld.b | |
|
3 | xrge0subcld.c | |
|
4 | iccssxr | |
|
5 | 4 1 | sselid | |
6 | 4 2 | sselid | |
7 | 6 | xnegcld | |
8 | 5 7 | xaddcld | |
9 | xsubge0 | |
|
10 | 5 6 9 | syl2anc | |
11 | 3 10 | mpbird | |
12 | 8 11 | jca | |
13 | elxrge0 | |
|
14 | 12 13 | sylibr | |