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
|- ( ph -> A e. RR* )
iccgelbd.2
|- ( ph -> B e. RR* )
iccgelbd.3
|- ( ph -> C e. ( A [,] B ) )
Assertion iccgelbd
|- ( ph -> A <_ C )

Proof

Step Hyp Ref Expression
1 iccgelbd.1
 |-  ( ph -> A e. RR* )
2 iccgelbd.2
 |-  ( ph -> B e. RR* )
3 iccgelbd.3
 |-  ( ph -> C e. ( A [,] B ) )
4 iccgelb
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
5 1 2 3 4 syl3anc
 |-  ( ph -> A <_ C )