Theorem fzne2d

Description: Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024)

	Ref	Expression
Hypotheses	fzne2d.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
	fzne2d.2	⊢ ( 𝜑 → 𝐾 ≠ 𝑁 )
Assertion	fzne2d	⊢ ( 𝜑 → 𝐾 < 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		fzne2d.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
2		fzne2d.2	⊢ ( 𝜑 → 𝐾 ≠ 𝑁 )
3	2	necomd	⊢ ( 𝜑 → 𝑁 ≠ 𝐾 )
4		elfz2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
5	1 4	sylib	⊢ ( 𝜑 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
6	5	simpld	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
7	6	simp3d	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
8	7	zred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
9	6	simp2d	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10	9	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11	5	simprrd	⊢ ( 𝜑 → 𝐾 ≤ 𝑁 )
12	8 10 11	leltned	⊢ ( 𝜑 → ( 𝐾 < 𝑁 ↔ 𝑁 ≠ 𝐾 ) )
13	3 12	mpbird	⊢ ( 𝜑 → 𝐾 < 𝑁 )