Description: A half-open range does not contain its right endpoint. (Contributed by Stefan O'Rear, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzonel | ⊢ ¬ 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzolt2 | ⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 < 𝐵 ) | |
2 | elfzoel2 | ⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℤ ) | |
3 | 2 | zred | ⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → 𝐵 ∈ ℝ ) |
4 | 3 | ltnrd | ⊢ ( 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) → ¬ 𝐵 < 𝐵 ) |
5 | 1 4 | pm2.65i | ⊢ ¬ 𝐵 ∈ ( 𝐴 ..^ 𝐵 ) |