Metamath Proof Explorer

Theorem eluzelre

Description: A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013)

Ref Expression
Assertion eluzelre 
|- ( N e. ( ZZ>= ` M ) -> N e. RR )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2 1 zred 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )