Theorem elfzod

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

	Ref	Expression
Hypotheses	elfzod.1	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
	elfzod.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	elfzod.3	⊢ ( 𝜑 → 𝐾 < 𝑁 )
Assertion	elfzod	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzod.1	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		elfzod.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		elfzod.3	⊢ ( 𝜑 → 𝐾 < 𝑁 )
4		elfzo2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
5	1 2 3 4	syl3anbrc	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )