Description: Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzolt3b | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzoel1 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ ) | |
2 | elfzoel2 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ ) | |
3 | elfzolt3 | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 < 𝑁 ) | |
4 | fzolb | ⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) | |
5 | 1 2 3 4 | syl3anbrc | ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) ) |