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	⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℝ )
3	2	recnd	⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℂ )
4		ge0addcl	⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
5		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
6	3 4 5	cnsubmlem	⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld )