Metamath Proof Explorer


Theorem eluzelz2

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

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

Proof

Step Hyp Ref Expression
1 eluzelz2.1
 |-  Z = ( ZZ>= ` M )
2 1 eleq2i
 |-  ( N e. Z <-> N e. ( ZZ>= ` M ) )
3 2 biimpi
 |-  ( N e. Z -> N e. ( ZZ>= ` M ) )
4 eluzelz
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 3 4 syl
 |-  ( N e. Z -> N e. ZZ )