This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )