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 )