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 ) ... 𝑁 ) )