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	|- ( ph -> K e. ( M ... N ) )
	fzne2d.2	|- ( ph -> K =/= N )
Assertion	fzne2d	|- ( ph -> K < N )

Proof

Step	Hyp	Ref	Expression
1		fzne2d.1	|- ( ph -> K e. ( M ... N ) )
2		fzne2d.2	|- ( ph -> K =/= N )
3	2	necomd	|- ( ph -> N =/= K )
4		elfz2	|- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
5	1 4	sylib	|- ( ph -> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
6	5	simpld	|- ( ph -> ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) )
7	6	simp3d	|- ( ph -> K e. ZZ )
8	7	zred	|- ( ph -> K e. RR )
9	6	simp2d	|- ( ph -> N e. ZZ )
10	9	zred	|- ( ph -> N e. RR )
11	5	simprrd	|- ( ph -> K <_ N )
12	8 10 11	leltned	|- ( ph -> ( K < N <-> N =/= K ) )
13	3 12	mpbird	|- ( ph -> K < N )