Theorem elfzod

Description: Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elfzod.1	|- ( ph -> K e. ( ZZ>= ` M ) )
	elfzod.2	|- ( ph -> N e. ZZ )
	elfzod.3	|- ( ph -> K < N )
Assertion	elfzod	|- ( ph -> K e. ( M ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzod.1	|- ( ph -> K e. ( ZZ>= ` M ) )
2		elfzod.2	|- ( ph -> N e. ZZ )
3		elfzod.3	|- ( ph -> K < N )
4		elfzo2	|- ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
5	1 2 3 4	syl3anbrc	|- ( ph -> K e. ( M ..^ N ) )