Metamath Proof Explorer


Theorem iccgelbd

Description: An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses iccgelbd.1 ( 𝜑𝐴 ∈ ℝ* )
iccgelbd.2 ( 𝜑𝐵 ∈ ℝ* )
iccgelbd.3 ( 𝜑𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
Assertion iccgelbd ( 𝜑𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 iccgelbd.1 ( 𝜑𝐴 ∈ ℝ* )
2 iccgelbd.2 ( 𝜑𝐵 ∈ ℝ* )
3 iccgelbd.3 ( 𝜑𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
4 iccgelb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴𝐶 )
5 1 2 3 4 syl3anc ( 𝜑𝐴𝐶 )