Theorem fzone1

Description: Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

	Ref	Expression
Assertion	fzone1	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzofz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
2	1	adantr	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
3		elfzlmr	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
4	2 3	syl	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
5		df-3or	⊢ ( ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ↔ ( ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∨ 𝐾 = 𝑁 ) )
6	4 5	sylib	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) ∨ 𝐾 = 𝑁 ) )
7		elfzelz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
8	2 7	syl	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℤ )
9	8	zred	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℝ )
10		elfzolt2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
11	10	adantr	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 < 𝑁 )
12	9 11	ltned	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ 𝑁 )
13	12	neneqd	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ¬ 𝐾 = 𝑁 )
14	6 13	olcnd	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
15		simpr	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ 𝑀 )
16	15	neneqd	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ¬ 𝐾 = 𝑀 )
17	14 16	orcnd	⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )