Metamath Proof Explorer

Theorem elico2

Description: Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elico2 
|- ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( A e. RR -> A e. RR* )
2 elico1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
3 1 2 sylan 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
4 mnfxr 
 |-  -oo e. RR*
5 4 a1i 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> -oo e. RR* )
6 1 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> A e. RR* )
7 simpr1 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> C e. RR* )
8 mnflt 
 |-  ( A e. RR -> -oo < A )
9 8 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> -oo < A )
10 simpr2 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> A <_ C )
11 5 6 7 9 10 xrltletrd 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> -oo < C )
12 simplr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> B e. RR* )
13 pnfxr 
 |-  +oo e. RR*
14 13 a1i 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> +oo e. RR* )
15 simpr3 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> C < B )
16 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
17 16 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> B <_ +oo )
18 7 12 14 15 17 xrltletrd 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> C < +oo )
19 xrrebnd 
 |-  ( C e. RR* -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) )
20 7 19 syl 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) )
21 11 18 20 mpbir2and 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> C e. RR )
22 21 10 15 3jca 
 |-  ( ( ( A e. RR /\ B e. RR* ) /\ ( C e. RR* /\ A <_ C /\ C < B ) ) -> ( C e. RR /\ A <_ C /\ C < B ) )
23 22 ex 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C < B ) -> ( C e. RR /\ A <_ C /\ C < B ) ) )
24 rexr 
 |-  ( C e. RR -> C e. RR* )
25 24 3anim1i 
 |-  ( ( C e. RR /\ A <_ C /\ C < B ) -> ( C e. RR* /\ A <_ C /\ C < B ) )
26 23 25 impbid1 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( ( C e. RR* /\ A <_ C /\ C < B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
27 3 26 bitrd 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )