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

Metamath Proof Explorer

Theorem eliocre

Description: A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliocre 
|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR )

Proof

Step Hyp Ref Expression
1 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
2 1 elixx3g 
 |-  ( C e. ( A (,] B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C <_ B ) ) )
3 2 biimpi 
 |-  ( C e. ( A (,] B ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C <_ B ) ) )
4 3 simpld 
 |-  ( C e. ( A (,] B ) -> ( A e. RR* /\ B e. RR* /\ C e. RR* ) )
5 4 simp3d 
 |-  ( C e. ( A (,] B ) -> C e. RR* )
6 5 adantl 
 |-  ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR* )
7 simpl 
 |-  ( ( B e. RR /\ C e. ( A (,] B ) ) -> B e. RR )
8 mnfxr 
 |-  -oo e. RR*
9 8 a1i 
 |-  ( C e. ( A (,] B ) -> -oo e. RR* )
10 4 simp1d 
 |-  ( C e. ( A (,] B ) -> A e. RR* )
11 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
12 10 11 syl 
 |-  ( C e. ( A (,] B ) -> -oo <_ A )
13 3 simprd 
 |-  ( C e. ( A (,] B ) -> ( A < C /\ C <_ B ) )
14 13 simpld 
 |-  ( C e. ( A (,] B ) -> A < C )
15 9 10 5 12 14 xrlelttrd 
 |-  ( C e. ( A (,] B ) -> -oo < C )
16 15 adantl 
 |-  ( ( B e. RR /\ C e. ( A (,] B ) ) -> -oo < C )
17 13 simprd 
 |-  ( C e. ( A (,] B ) -> C <_ B )
18 17 adantl 
 |-  ( ( B e. RR /\ C e. ( A (,] B ) ) -> C <_ B )
19 xrre 
 |-  ( ( ( C e. RR* /\ B e. RR ) /\ ( -oo < C /\ C <_ B ) ) -> C e. RR )
20 6 7 16 18 19 syl22anc 
 |-  ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR )