Metamath Proof Explorer


Theorem icoltubd

Description: An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses icoltubd.1
|- ( ph -> A e. RR* )
icoltubd.2
|- ( ph -> B e. RR* )
icoltubd.3
|- ( ph -> C e. ( A [,) B ) )
Assertion icoltubd
|- ( ph -> C < B )

Proof

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