Metamath Proof Explorer

Theorem nn0subm

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

Ref Expression
Assertion nn0subm 
|- NN0 e. ( SubMnd ` CCfld )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
2 nn0addcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 )
3 0nn0 
 |-  0 e. NN0
4 1 2 3 cnsubmlem 
 |-  NN0 e. ( SubMnd ` CCfld )