Metamath Proof Explorer


Theorem ltnelicc

Description: A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ltnelicc.a
|- ( ph -> A e. RR )
ltnelicc.b
|- ( ph -> B e. RR* )
ltnelicc.c
|- ( ph -> C e. RR* )
ltnelicc.clta
|- ( ph -> C < A )
Assertion ltnelicc
|- ( ph -> -. C e. ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 ltnelicc.a
 |-  ( ph -> A e. RR )
2 ltnelicc.b
 |-  ( ph -> B e. RR* )
3 ltnelicc.c
 |-  ( ph -> C e. RR* )
4 ltnelicc.clta
 |-  ( ph -> C < A )
5 1 rexrd
 |-  ( ph -> A e. RR* )
6 xrltnle
 |-  ( ( C e. RR* /\ A e. RR* ) -> ( C < A <-> -. A <_ C ) )
7 3 5 6 syl2anc
 |-  ( ph -> ( C < A <-> -. A <_ C ) )
8 4 7 mpbid
 |-  ( ph -> -. A <_ C )
9 8 intnanrd
 |-  ( ph -> -. ( A <_ C /\ C <_ B ) )
10 elicc4
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
11 5 2 3 10 syl3anc
 |-  ( ph -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
12 9 11 mtbird
 |-  ( ph -> -. C e. ( A [,] B ) )