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

Metamath Proof Explorer

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 2 elfzelzd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℤ )
8 7 zred ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℝ )
9 elfzolt2 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
10 9 adantr ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 < 𝑁 )
11 8 10 ltned ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ 𝑁 )
12 11 neneqd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ¬ 𝐾 = 𝑁 )
13 6 12 olcnd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) )
14 simpr ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ 𝑀 )
15 14 neneqd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → ¬ 𝐾 = 𝑀 )
16 13 15 orcnd ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )