Metamath Proof Explorer

Theorem elicore

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

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

Proof

Step Hyp Ref Expression
1 df-ico 
 |-  [,) = ( 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 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> C e. RR* )
7 simpl 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> A e. RR )
8 3 simprd 
 |-  ( C e. ( A [,) B ) -> ( A <_ C /\ C < B ) )
9 8 simpld 
 |-  ( C e. ( A [,) B ) -> A <_ C )
10 9 adantl 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> A <_ C )
11 4 simp2d 
 |-  ( C e. ( A [,) B ) -> B e. RR* )
12 11 adantl 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> B e. RR* )
13 pnfxr 
 |-  +oo e. RR*
14 13 a1i 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> +oo e. RR* )
15 8 simprd 
 |-  ( C e. ( A [,) B ) -> C < B )
16 15 adantl 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> C < B )
17 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
18 11 17 syl 
 |-  ( C e. ( A [,) B ) -> B <_ +oo )
19 18 adantl 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> B <_ +oo )
20 6 12 14 16 19 xrltletrd 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> C < +oo )
21 xrre3 
 |-  ( ( ( C e. RR* /\ A e. RR ) /\ ( A <_ C /\ C < +oo ) ) -> C e. RR )
22 6 7 10 20 21 syl22anc 
 |-  ( ( A e. RR /\ C e. ( A [,) B ) ) -> C e. RR )