Metamath Proof Explorer

Theorem eluzsub

Description: Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Assertion eluzsub 
|- ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ( ZZ>= ` M ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> M e. ZZ )
2 eluzelz 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> N e. ZZ )
3 2 3ad2ant3 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> N e. ZZ )
4 simp2 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> K e. ZZ )
5 3 4 zsubcld 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ZZ )
6 eluzle 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> ( M + K ) <_ N )
7 6 3ad2ant3 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( M + K ) <_ N )
8 zre 
 |-  ( M e. ZZ -> M e. RR )
9 zre 
 |-  ( K e. ZZ -> K e. RR )
10 eluzelre 
 |-  ( N e. ( ZZ>= ` ( M + K ) ) -> N e. RR )
11 leaddsub 
 |-  ( ( M e. RR /\ K e. RR /\ N e. RR ) -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
12 8 9 10 11 syl3an 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( ( M + K ) <_ N <-> M <_ ( N - K ) ) )
13 7 12 mpbid 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> M <_ ( N - K ) )
14 eluz2 
 |-  ( ( N - K ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N - K ) e. ZZ /\ M <_ ( N - K ) ) )
15 1 5 13 14 syl3anbrc 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ( ZZ>= ` ( M + K ) ) ) -> ( N - K ) e. ( ZZ>= ` M ) )