Description: A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzolt2 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzoelz | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ ) | |
2 | elfzoel1 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ ) | |
3 | elfzoel2 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ ) | |
4 | elfzo | ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ) | |
5 | 1 2 3 4 | syl3anc | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) ) |
6 | 5 | ibi | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) ) |
7 | 6 | simprd | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 ) |