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	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝑀 − 𝐿 ) ..^ ( 𝑁 − 𝐿 ) ) ↔ ( 𝐾 + 𝐿 ) ∈ ( 𝑀 ..^ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zsubcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑀 − 𝐿 ) ∈ ℤ )
2	1	ad2ant2rl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑀 − 𝐿 ) ∈ ℤ )
3		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
4	3	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
5	2 4	2thd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝑀 − 𝐿 ) ∈ ℤ ↔ 𝑀 ∈ ℤ ) )
6		simpl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐾 ∈ ℤ )
7	6	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
8		zaddcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐾 + 𝐿 ) ∈ ℤ )
9	8	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 + 𝐿 ) ∈ ℤ )
10	7 9	2thd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ↔ ( 𝐾 + 𝐿 ) ∈ ℤ ) )
11		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
13	12	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝑀 ∈ ℝ )
14		zre	⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
15	14	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
16	15	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝐿 ∈ ℝ )
17		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
18	17	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐾 ∈ ℝ )
19	18	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝐾 ∈ ℝ )
20	13 16 19	lesubaddd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝑀 − 𝐿 ) ≤ 𝐾 ↔ 𝑀 ≤ ( 𝐾 + 𝐿 ) ) )
21	5 10 20	3anbi123d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝐿 ) ≤ 𝐾 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝐾 + 𝐿 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝐾 + 𝐿 ) ) ) )
22		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝐿 ) ) ↔ ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 − 𝐿 ) ≤ 𝐾 ) )
23		eluz2	⊢ ( ( 𝐾 + 𝐿 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝐾 + 𝐿 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝐾 + 𝐿 ) ) )
24	21 22 23	3bitr4g	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝐿 ) ) ↔ ( 𝐾 + 𝐿 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
25		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
26	25	ad2ant2l	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
27		simplr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
28	26 27	2thd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝑁 − 𝐿 ) ∈ ℤ ↔ 𝑁 ∈ ℤ ) )
29		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
30	29	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
31	30	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → 𝑁 ∈ ℝ )
32	19 16 31	ltaddsubd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐾 + 𝐿 ) < 𝑁 ↔ 𝐾 < ( 𝑁 − 𝐿 ) ) )
33	32	bicomd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 < ( 𝑁 − 𝐿 ) ↔ ( 𝐾 + 𝐿 ) < 𝑁 ) )
34	24 28 33	3anbi123d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝐿 ) ) ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ∧ 𝐾 < ( 𝑁 − 𝐿 ) ) ↔ ( ( 𝐾 + 𝐿 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 + 𝐿 ) < 𝑁 ) ) )
35		elfzo2	⊢ ( 𝐾 ∈ ( ( 𝑀 − 𝐿 ) ..^ ( 𝑁 − 𝐿 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝐿 ) ) ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ∧ 𝐾 < ( 𝑁 − 𝐿 ) ) )
36		elfzo2	⊢ ( ( 𝐾 + 𝐿 ) ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( ( 𝐾 + 𝐿 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 + 𝐿 ) < 𝑁 ) )
37	34 35 36	3bitr4g	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝑀 − 𝐿 ) ..^ ( 𝑁 − 𝐿 ) ) ↔ ( 𝐾 + 𝐿 ) ∈ ( 𝑀 ..^ 𝑁 ) ) )