Theorem rege0subm

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

	Ref	Expression
Assertion	rege0subm	$$⊢\left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
2	1	sseli	$$⊢x\in \left[0,\mathrm{+\infty }\right)\to x\in ℝ$$
3	2	recnd	$$⊢x\in \left[0,\mathrm{+\infty }\right)\to x\in ℂ$$
4		ge0addcl	$$⊢\left(x\in \left[0,\mathrm{+\infty }\right)\wedge y\in \left[0,\mathrm{+\infty }\right)\right)\to x+y\in \left[0,\mathrm{+\infty }\right)$$
5		0e0icopnf	$$⊢0\in \left[0,\mathrm{+\infty }\right)$$
6	3 4 5	cnsubmlem	$$⊢\left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$