Metamath Proof Explorer


Theorem xrge0subm

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 R=𝑠*𝑠*−∞
Assertion xrge0subm 0+∞SubMndR

Proof

Step Hyp Ref Expression
1 xrs1mnd.1 R=𝑠*𝑠*−∞
2 simpl x*0xx*
3 ge0nemnf x*0xx−∞
4 2 3 jca x*0xx*x−∞
5 elxrge0 x0+∞x*0x
6 eldifsn x*−∞x*x−∞
7 4 5 6 3imtr4i x0+∞x*−∞
8 7 ssriv 0+∞*−∞
9 0e0iccpnf 00+∞
10 ge0xaddcl x0+∞y0+∞x+𝑒y0+∞
11 10 rgen2 x0+∞y0+∞x+𝑒y0+∞
12 1 xrs1mnd RMnd
13 difss *−∞*
14 xrsbas *=Base𝑠*
15 1 14 ressbas2 *−∞**−∞=BaseR
16 13 15 ax-mp *−∞=BaseR
17 1 xrs10 0=0R
18 xrex *V
19 18 difexi *−∞V
20 xrsadd +𝑒=+𝑠*
21 1 20 ressplusg *−∞V+𝑒=+R
22 19 21 ax-mp +𝑒=+R
23 16 17 22 issubm RMnd0+∞SubMndR0+∞*−∞00+∞x0+∞y0+∞x+𝑒y0+∞
24 12 23 ax-mp 0+∞SubMndR0+∞*−∞00+∞x0+∞y0+∞x+𝑒y0+∞
25 8 9 11 24 mpbir3an 0+∞SubMndR