Metamath Proof Explorer


Theorem eluzd

Description: Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses eluzd.1
|- Z = ( ZZ>= ` M )
eluzd.2
|- ( ph -> M e. ZZ )
eluzd.3
|- ( ph -> N e. ZZ )
eluzd.4
|- ( ph -> M <_ N )
Assertion eluzd
|- ( ph -> N e. Z )

Proof

Step Hyp Ref Expression
1 eluzd.1
 |-  Z = ( ZZ>= ` M )
2 eluzd.2
 |-  ( ph -> M e. ZZ )
3 eluzd.3
 |-  ( ph -> N e. ZZ )
4 eluzd.4
 |-  ( ph -> M <_ N )
5 eluz2
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
6 2 3 4 5 syl3anbrc
 |-  ( ph -> N e. ( ZZ>= ` M ) )
7 6 1 eleqtrrdi
 |-  ( ph -> N e. Z )