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