This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrgtnelicc

Description: A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021)

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

Proof

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