Metamath Proof Explorer

Theorem elfzmlbp

Description: Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018)

Ref Expression
Assertion elfzmlbp 
|- ( ( N e. ZZ /\ K e. ( M ... ( M + N ) ) ) -> ( K - M ) e. ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 elfz2 
 |-  ( K e. ( M ... ( M + N ) ) <-> ( ( M e. ZZ /\ ( M + N ) e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) )
2 znn0sub 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M <_ K <-> ( K - M ) e. NN0 ) )
3 2 adantr 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( M <_ K <-> ( K - M ) e. NN0 ) )
4 3 biimpcd 
 |-  ( M <_ K -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K - M ) e. NN0 ) )
5 4 adantr 
 |-  ( ( M <_ K /\ K <_ ( M + N ) ) -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K - M ) e. NN0 ) )
6 5 impcom 
 |-  ( ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> ( K - M ) e. NN0 )
7 zre 
 |-  ( M e. ZZ -> M e. RR )
8 7 adantr 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> M e. RR )
9 8 adantr 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> M e. RR )
10 zre 
 |-  ( K e. ZZ -> K e. RR )
11 10 adantl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> K e. RR )
12 11 adantr 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> K e. RR )
13 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
14 13 adantlr 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( M + N ) e. ZZ )
15 14 zred 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( M + N ) e. RR )
16 letr 
 |-  ( ( M e. RR /\ K e. RR /\ ( M + N ) e. RR ) -> ( ( M <_ K /\ K <_ ( M + N ) ) -> M <_ ( M + N ) ) )
17 9 12 15 16 syl3anc 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( ( M <_ K /\ K <_ ( M + N ) ) -> M <_ ( M + N ) ) )
18 zre 
 |-  ( N e. ZZ -> N e. RR )
19 addge01 
 |-  ( ( M e. RR /\ N e. RR ) -> ( 0 <_ N <-> M <_ ( M + N ) ) )
20 8 18 19 syl2an 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( 0 <_ N <-> M <_ ( M + N ) ) )
21 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
22 21 simplbi2 
 |-  ( N e. ZZ -> ( 0 <_ N -> N e. NN0 ) )
23 22 adantl 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( 0 <_ N -> N e. NN0 ) )
24 20 23 sylbird 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( M <_ ( M + N ) -> N e. NN0 ) )
25 17 24 syld 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( ( M <_ K /\ K <_ ( M + N ) ) -> N e. NN0 ) )
26 25 imp 
 |-  ( ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> N e. NN0 )
27 df-3an 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ZZ ) <-> ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) )
28 3ancoma 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ N e. ZZ ) <-> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
29 27 28 bitr3i 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) <-> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
30 10 7 18 3anim123i 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. RR /\ M e. RR /\ N e. RR ) )
31 29 30 sylbi 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K e. RR /\ M e. RR /\ N e. RR ) )
32 lesubadd2 
 |-  ( ( K e. RR /\ M e. RR /\ N e. RR ) -> ( ( K - M ) <_ N <-> K <_ ( M + N ) ) )
33 31 32 syl 
 |-  ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( ( K - M ) <_ N <-> K <_ ( M + N ) ) )
34 33 biimprcd 
 |-  ( K <_ ( M + N ) -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K - M ) <_ N ) )
35 34 adantl 
 |-  ( ( M <_ K /\ K <_ ( M + N ) ) -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K - M ) <_ N ) )
36 35 impcom 
 |-  ( ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> ( K - M ) <_ N )
37 6 26 36 3jca 
 |-  ( ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) )
38 37 exp31 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( N e. ZZ -> ( ( M <_ K /\ K <_ ( M + N ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) ) )
39 38 com23 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( ( M <_ K /\ K <_ ( M + N ) ) -> ( N e. ZZ -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) ) )
40 39 3adant2 
 |-  ( ( M e. ZZ /\ ( M + N ) e. ZZ /\ K e. ZZ ) -> ( ( M <_ K /\ K <_ ( M + N ) ) -> ( N e. ZZ -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) ) )
41 40 imp 
 |-  ( ( ( M e. ZZ /\ ( M + N ) e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> ( N e. ZZ -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) )
42 41 com12 
 |-  ( N e. ZZ -> ( ( ( M e. ZZ /\ ( M + N ) e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ ( M + N ) ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) )
43 1 42 syl5bi 
 |-  ( N e. ZZ -> ( K e. ( M ... ( M + N ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) ) )
44 43 imp 
 |-  ( ( N e. ZZ /\ K e. ( M ... ( M + N ) ) ) -> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) )
45 elfz2nn0 
 |-  ( ( K - M ) e. ( 0 ... N ) <-> ( ( K - M ) e. NN0 /\ N e. NN0 /\ ( K - M ) <_ N ) )
46 44 45 sylibr 
 |-  ( ( N e. ZZ /\ K e. ( M ... ( M + N ) ) ) -> ( K - M ) e. ( 0 ... N ) )