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 +∞ ∈ SubMnd ⁡ R

Proof

Step Hyp Ref Expression
1 xrs1mnd.1 ⊢ R = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
2 simpl ⊢ x ∈ ℝ * ∧ 0 ≤ x → x ∈ ℝ *
3 ge0nemnf ⊢ x ∈ ℝ * ∧ 0 ≤ x → x ≠ −∞
4 2 3 jca ⊢ x ∈ ℝ * ∧ 0 ≤ x → x ∈ ℝ * ∧ x ≠ −∞
5 elxrge0 ⊢ x ∈ 0 +∞ ↔ x ∈ ℝ * ∧ 0 ≤ x
6 eldifsn ⊢ x ∈ ℝ * ∖ −∞ ↔ x ∈ ℝ * ∧ x ≠ −∞
7 4 5 6 3imtr4i ⊢ x ∈ 0 +∞ → x ∈ ℝ * ∖ −∞
8 7 ssriv ⊢ 0 +∞ ⊆ ℝ * ∖ −∞
9 0e0iccpnf ⊢ 0 ∈ 0 +∞
10 ge0xaddcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + 𝑒 y ∈ 0 +∞
11 10 rgen2 ⊢ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x + 𝑒 y ∈ 0 +∞
12 1 xrs1mnd ⊢ R ∈ Mnd
13 difss ⊢ ℝ * ∖ −∞ ⊆ ℝ *
14 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
15 1 14 ressbas2 ⊢ ℝ * ∖ −∞ ⊆ ℝ * → ℝ * ∖ −∞ = Base R
16 13 15 ax-mp ⊢ ℝ * ∖ −∞ = Base R
17 1 xrs10 ⊢ 0 = 0 R
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 ⊢ R ∈ Mnd → 0 +∞ ∈ SubMnd ⁡ R ↔ 0 +∞ ⊆ ℝ * ∖ −∞ ∧ 0 ∈ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x + 𝑒 y ∈ 0 +∞
24 12 23 ax-mp ⊢ 0 +∞ ∈ SubMnd ⁡ R ↔ 0 +∞ ⊆ ℝ * ∖ −∞ ∧ 0 ∈ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ x + 𝑒 y ∈ 0 +∞
25 8 9 11 24 mpbir3an ⊢ 0 +∞ ∈ SubMnd ⁡ R