Metamath Proof Explorer

Theorem elfzolborelfzop1

Description: An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020)

Ref Expression
Assertion elfzolborelfzop1 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elfzo2 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
2 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) )
3 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
5 leloe ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝑀 < 𝐾 ∨ 𝑀 = 𝐾 ) ) )
6 3 4 5 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝑀 < 𝐾 ∨ 𝑀 = 𝐾 ) ) )
7 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
8 7 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 + 1 ) ∈ ℤ )
9 8 ad2antrl ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 + 1 ) ∈ ℤ )
10 simprlr ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
11 simpl ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → 𝑀 < 𝐾 )
12 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 < 𝐾 ↔ ( 𝑀 + 1 ) ≤ 𝐾 ) )
13 12 ad2antrl ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 < 𝐾 ↔ ( 𝑀 + 1 ) ≤ 𝐾 ) )
14 11 13 mpbid ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 + 1 ) ≤ 𝐾 )
15 9 10 14 3jca ⊢ ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐾 ) )
16 15 adantr ⊢ ( ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐾 < 𝑁 ) → ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐾 ) )
17 simplrr ⊢ ( ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℤ )
18 simpr ⊢ ( ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
19 elfzo2 ⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
20 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐾 ) )
21 20 3anbi1i ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐾 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
22 19 21 bitri ⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ↔ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝐾 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
23 16 17 18 22 syl3anbrc ⊢ ( ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
24 23 olcd ⊢ ( ( ( 𝑀 < 𝐾 ∧ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
25 24 exp31 ⊢ ( 𝑀 < 𝐾 → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) )
26 orc ⊢ ( 𝐾 = 𝑀 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
27 26 eqcoms ⊢ ( 𝑀 = 𝐾 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
28 27 2a1d ⊢ ( 𝑀 = 𝐾 → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) )
29 25 28 jaoi ⊢ ( ( 𝑀 < 𝐾 ∨ 𝑀 = 𝐾 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) )
30 29 expd ⊢ ( ( 𝑀 < 𝐾 ∨ 𝑀 = 𝐾 ) → ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) ) )
31 30 com12 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 < 𝐾 ∨ 𝑀 = 𝐾 ) → ( 𝑁 ∈ ℤ → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) ) )
32 6 31 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 → ( 𝑁 ∈ ℤ → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) ) )
33 32 3impia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝑁 ∈ ℤ → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) )
34 2 33 sylbi ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ℤ → ( 𝐾 < 𝑁 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ) ) )
35 34 3imp ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
36 1 35 sylbi ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )