Metamath Proof Explorer


Theorem iccleub

Description: An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009)

Ref Expression
Assertion iccleub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶𝐵 )

Proof

Step Hyp Ref Expression
1 elicc1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵 ) ) )
2 simp3 ( ( 𝐶 ∈ ℝ*𝐴𝐶𝐶𝐵 ) → 𝐶𝐵 )
3 1 2 syl6bi ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) → 𝐶𝐵 ) )
4 3 3impia ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶𝐵 )