Metamath Proof Explorer

Theorem subeluzsub

Description: Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022)

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

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ZZ )
2 zsubcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
3 1 2 sylan2 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> ( M - N ) e. ZZ )
4 eluzel2 
 |-  ( N e. ( ZZ>= ` K ) -> K e. ZZ )
5 zsubcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M - K ) e. ZZ )
6 4 5 sylan2 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> ( M - K ) e. ZZ )
7 4 zred 
 |-  ( N e. ( ZZ>= ` K ) -> K e. RR )
8 7 adantl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> K e. RR )
9 1 zred 
 |-  ( N e. ( ZZ>= ` K ) -> N e. RR )
10 9 adantl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> N e. RR )
11 zre 
 |-  ( M e. ZZ -> M e. RR )
12 11 adantr 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> M e. RR )
13 eluzle 
 |-  ( N e. ( ZZ>= ` K ) -> K <_ N )
14 13 adantl 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> K <_ N )
15 8 10 12 14 lesub2dd 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> ( M - N ) <_ ( M - K ) )
16 eluz2 
 |-  ( ( M - K ) e. ( ZZ>= ` ( M - N ) ) <-> ( ( M - N ) e. ZZ /\ ( M - K ) e. ZZ /\ ( M - N ) <_ ( M - K ) ) )
17 3 6 15 16 syl3anbrc 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` K ) ) -> ( M - K ) e. ( ZZ>= ` ( M - N ) ) )