Metamath Proof Explorer


Theorem elicc2

Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007) (Revised by Mario Carneiro, 14-Jun-2014)

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