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

Metamath Proof Explorer

Theorem fzne1

Description: Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

Ref Expression
Assertion fzne1 ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝐾 ≠ 𝑀 ↔ ¬ 𝐾 = 𝑀 )
2 elfzuz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 elfzp12 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
4 2 3 syl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
5 4 ibi ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
6 5 orcanai ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ ¬ 𝐾 = 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
7 1 6 sylan2b ⊢ ( ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )