Metamath Proof Explorer


Theorem eluzelcn

Description: A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion eluzelcn
|- ( N e. ( ZZ>= ` M ) -> N e. CC )

Proof

Step Hyp Ref Expression
1 eluzelre
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
2 1 recnd
 |-  ( N e. ( ZZ>= ` M ) -> N e. CC )