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 [,) +oo ) e. ( SubMnd ` CCfld )

Proof

Step Hyp Ref Expression
1 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
2 1 sseli 
 |-  ( x e. ( 0 [,) +oo ) -> x e. RR )
3 2 recnd 
 |-  ( x e. ( 0 [,) +oo ) -> x e. CC )
4 ge0addcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
5 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
6 3 4 5 cnsubmlem 
 |-  ( 0 [,) +oo ) e. ( SubMnd ` CCfld )