Theorem elfzd

Description: Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elfzd.1	|- ( ph -> M e. ZZ )
	elfzd.2	|- ( ph -> N e. ZZ )
	elfzd.3	|- ( ph -> K e. ZZ )
	elfzd.4	|- ( ph -> M <_ K )
	elfzd.5	|- ( ph -> K <_ N )
Assertion	elfzd	|- ( ph -> K e. ( M ... N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzd.1	|- ( ph -> M e. ZZ )
2		elfzd.2	|- ( ph -> N e. ZZ )
3		elfzd.3	|- ( ph -> K e. ZZ )
4		elfzd.4	|- ( ph -> M <_ K )
5		elfzd.5	|- ( ph -> K <_ N )
6	1 2 3	3jca	|- ( ph -> ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) )
7	6 4 5	jca32	|- ( ph -> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
8		elfz2	|- ( K e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M <_ K /\ K <_ N ) ) )
9	7 8	sylibr	|- ( ph -> K e. ( M ... N ) )