Description: An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | iooltub | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 < 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elioo2 | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) ) | |
2 | simp3 | ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 ) | |
3 | 1 2 | syl6bi | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) → 𝐶 < 𝐵 ) ) |
4 | 3 | 3impia | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 < 𝐵 ) |