Metamath Proof Explorer


Theorem eluzsubi

Description: Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Hypotheses eluzsubi.1
|- M e. ZZ
eluzsubi.2
|- K e. ZZ
Assertion eluzsubi
|- ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )

Proof

Step Hyp Ref Expression
1 eluzsubi.1
 |-  M e. ZZ
2 eluzsubi.2
 |-  K e. ZZ
3 eluzsub
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ( ZZ>= ` M ) )
4 1 2 3 mp3an12
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )