Metamath Proof Explorer

Theorem rege0subm

Description: The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion rege0subm ⊢ 0 +∞ ∈ SubMnd ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 rge0ssre ⊢ 0 +∞ ⊆ ℝ
2 1 sseli ⊢ x ∈ 0 +∞ → x ∈ ℝ
3 2 recnd ⊢ x ∈ 0 +∞ → x ∈ ℂ
4 ge0addcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
5 0e0icopnf ⊢ 0 ∈ 0 +∞
6 3 4 5 cnsubmlem ⊢ 0 +∞ ∈ SubMnd ⁡ ℂ fld