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 ) |
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 ) |