Metamath Proof Explorer

Theorem elfzomelpfzo

Description: An integer increased by another integer is an element of a half-open integer range if and only if the integer is contained in the half-open integer range with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018)

Ref Expression
Assertion elfzomelpfzo 
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K e. ( ( M - L ) ..^ ( N - L ) ) <-> ( K + L ) e. ( M ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 zsubcl 
 |-  ( ( M e. ZZ /\ L e. ZZ ) -> ( M - L ) e. ZZ )
2 1 ad2ant2rl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( M - L ) e. ZZ )
3 simpl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
4 3 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> M e. ZZ )
5 2 4 2thd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( M - L ) e. ZZ <-> M e. ZZ ) )
6 simpl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> K e. ZZ )
7 6 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> K e. ZZ )
8 zaddcl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( K + L ) e. ZZ )
9 8 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K + L ) e. ZZ )
10 7 9 2thd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K e. ZZ <-> ( K + L ) e. ZZ ) )
11 zre 
 |-  ( M e. ZZ -> M e. RR )
12 11 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. RR )
13 12 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> M e. RR )
14 zre 
 |-  ( L e. ZZ -> L e. RR )
15 14 adantl 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> L e. RR )
16 15 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> L e. RR )
17 zre 
 |-  ( K e. ZZ -> K e. RR )
18 17 adantr 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> K e. RR )
19 18 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> K e. RR )
20 13 16 19 lesubaddd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( M - L ) <_ K <-> M <_ ( K + L ) ) )
21 5 10 20 3anbi123d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( ( M - L ) e. ZZ /\ K e. ZZ /\ ( M - L ) <_ K ) <-> ( M e. ZZ /\ ( K + L ) e. ZZ /\ M <_ ( K + L ) ) ) )
22 eluz2 
 |-  ( K e. ( ZZ>= ` ( M - L ) ) <-> ( ( M - L ) e. ZZ /\ K e. ZZ /\ ( M - L ) <_ K ) )
23 eluz2 
 |-  ( ( K + L ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( K + L ) e. ZZ /\ M <_ ( K + L ) ) )
24 21 22 23 3bitr4g 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K e. ( ZZ>= ` ( M - L ) ) <-> ( K + L ) e. ( ZZ>= ` M ) ) )
25 zsubcl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( N - L ) e. ZZ )
26 25 ad2ant2l 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( N - L ) e. ZZ )
27 simplr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> N e. ZZ )
28 26 27 2thd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( N - L ) e. ZZ <-> N e. ZZ ) )
29 zre 
 |-  ( N e. ZZ -> N e. RR )
30 29 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. RR )
31 30 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> N e. RR )
32 19 16 31 ltaddsubd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( K + L ) < N <-> K < ( N - L ) ) )
33 32 bicomd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K < ( N - L ) <-> ( K + L ) < N ) )
34 24 28 33 3anbi123d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( K e. ( ZZ>= ` ( M - L ) ) /\ ( N - L ) e. ZZ /\ K < ( N - L ) ) <-> ( ( K + L ) e. ( ZZ>= ` M ) /\ N e. ZZ /\ ( K + L ) < N ) ) )
35 elfzo2 
 |-  ( K e. ( ( M - L ) ..^ ( N - L ) ) <-> ( K e. ( ZZ>= ` ( M - L ) ) /\ ( N - L ) e. ZZ /\ K < ( N - L ) ) )
36 elfzo2 
 |-  ( ( K + L ) e. ( M ..^ N ) <-> ( ( K + L ) e. ( ZZ>= ` M ) /\ N e. ZZ /\ ( K + L ) < N ) )
37 34 35 36 3bitr4g 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K e. ( ( M - L ) ..^ ( N - L ) ) <-> ( K + L ) e. ( M ..^ N ) ) )