This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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