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	$$⊢\phi \to K\in \left(M\dots N\right)$$
	fzne2d.2	$$⊢\phi \to K\ne N$$
Assertion	fzne2d	$$⊢\phi \to K<N$$

Proof

Step	Hyp	Ref	Expression
1		fzne2d.1	$$⊢\phi \to K\in \left(M\dots N\right)$$
2		fzne2d.2	$$⊢\phi \to K\ne N$$
3	2	necomd	$$⊢\phi \to N\ne K$$
4		elfz2	$$⊢K\in \left(M\dots N\right)\leftrightarrow \left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge K\in \mathbb{Z}\right)\wedge \left(M\le K\wedge K\le N\right)\right)$$
5	1 4	sylib	$$⊢\phi \to \left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge K\in \mathbb{Z}\right)\wedge \left(M\le K\wedge K\le N\right)\right)$$
6	5	simpld	$$⊢\phi \to \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge K\in \mathbb{Z}\right)$$
7	6	simp3d	$$⊢\phi \to K\in \mathbb{Z}$$
8	7	zred	$$⊢\phi \to K\in ℝ$$
9	6	simp2d	$$⊢\phi \to N\in \mathbb{Z}$$
10	9	zred	$$⊢\phi \to N\in ℝ$$
11	5	simprrd	$$⊢\phi \to K\le N$$
12	8 10 11	leltned	$$⊢\phi \to \left(K<N\leftrightarrow N\ne K\right)$$
13	3 12	mpbird	$$⊢\phi \to K<N$$