Metamath Proof Explorer

Theorem eluzelzd

Description: A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypothesis eluzelzd.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion eluzelzd 
|- ( ph -> N e. ZZ )

Proof

Step Hyp Ref Expression
1 eluzelzd.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
3 1 2 syl 
 |-  ( ph -> N e. ZZ )