Description: The nonnegative extended real numbers are a submonoid of the nonnegative-infinite extended reals. (Contributed by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xrs1mnd.1 | |
|
Assertion | xrge0subm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrs1mnd.1 | |
|
2 | simpl | |
|
3 | ge0nemnf | |
|
4 | 2 3 | jca | |
5 | elxrge0 | |
|
6 | eldifsn | |
|
7 | 4 5 6 | 3imtr4i | |
8 | 7 | ssriv | |
9 | 0e0iccpnf | |
|
10 | ge0xaddcl | |
|
11 | 10 | rgen2 | |
12 | 1 | xrs1mnd | |
13 | difss | |
|
14 | xrsbas | |
|
15 | 1 14 | ressbas2 | |
16 | 13 15 | ax-mp | |
17 | 1 | xrs10 | |
18 | xrex | |
|
19 | 18 | difexi | |
20 | xrsadd | |
|
21 | 1 20 | ressplusg | |
22 | 19 21 | ax-mp | |
23 | 16 17 22 | issubm | |
24 | 12 23 | ax-mp | |
25 | 8 9 11 24 | mpbir3an | |