Metamath Proof Explorer

Theorem eluzsubi

Description: Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007)

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

Proof

Step Hyp Ref Expression
1 eluzaddi.1 
 |-  M e. ZZ
2 eluzaddi.2 
 |-  K e. ZZ
3 eluzelz 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> N e. ZZ )
4 zsubcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N - K ) e. ZZ )
5 3 2 4 sylancl 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ZZ )
6 zaddcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M + K ) e. ZZ )
7 1 2 6 mp2an 
 |-  ( M + K ) e. ZZ
8 7 eluz1i 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) <-> ( N e. ZZ /\ ( M + K ) <_ N ) )
9 1 zrei 
 |-  M e. RR
10 2 zrei 
 |-  K e. RR
11 zre 
 |-  ( N e. ZZ -> N e. RR )
12 leaddsub 
 |-  ( ( M e. RR /\ K e. RR /\ N e. RR ) -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
13 9 10 11 12 mp3an12i 
 |-  ( N e. ZZ -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
14 13 biimpa 
 |-  ( ( N e. ZZ /\ ( M + K ) <_ N ) -> M <_ ( N - K ) )
15 8 14 sylbi 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> M <_ ( N - K ) )
16 1 eluz1i 
 |-  ( ( N - K ) e. ( ZZ>= ` M ) <-> ( ( N - K ) e. ZZ /\ M <_ ( N - K ) ) )
17 5 15 16 sylanbrc 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> ( N - K ) e. ( ZZ>= ` M ) )