Metamath Proof Explorer

Theorem iccneg

Description: Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007)

Ref Expression
Assertion iccneg 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> -u C e. ( -u B [,] -u A ) ) )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( C e. RR -> -u C e. RR )
2 ax-1 
 |-  ( C e. RR -> ( -u C e. RR -> C e. RR ) )
3 1 2 impbid2 
 |-  ( C e. RR -> ( C e. RR <-> -u C e. RR ) )
4 3 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. RR <-> -u C e. RR ) )
5 ancom 
 |-  ( ( C <_ B /\ A <_ C ) <-> ( A <_ C /\ C <_ B ) )
6 leneg 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C <_ B <-> -u B <_ -u C ) )
7 6 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C <_ B <-> -u B <_ -u C ) )
8 7 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C <_ B <-> -u B <_ -u C ) )
9 leneg 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A <_ C <-> -u C <_ -u A ) )
10 9 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ C <-> -u C <_ -u A ) )
11 8 10 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C <_ B /\ A <_ C ) <-> ( -u B <_ -u C /\ -u C <_ -u A ) ) )
12 5 11 bitr3id 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ C /\ C <_ B ) <-> ( -u B <_ -u C /\ -u C <_ -u A ) ) )
13 4 12 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C e. RR /\ ( A <_ C /\ C <_ B ) ) <-> ( -u C e. RR /\ ( -u B <_ -u C /\ -u C <_ -u A ) ) ) )
14 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
15 14 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
16 3anass 
 |-  ( ( C e. RR /\ A <_ C /\ C <_ B ) <-> ( C e. RR /\ ( A <_ C /\ C <_ B ) ) )
17 15 16 bitrdi 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ ( A <_ C /\ C <_ B ) ) ) )
18 renegcl 
 |-  ( B e. RR -> -u B e. RR )
19 renegcl 
 |-  ( A e. RR -> -u A e. RR )
20 elicc2 
 |-  ( ( -u B e. RR /\ -u A e. RR ) -> ( -u C e. ( -u B [,] -u A ) <-> ( -u C e. RR /\ -u B <_ -u C /\ -u C <_ -u A ) ) )
21 18 19 20 syl2anr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -u C e. ( -u B [,] -u A ) <-> ( -u C e. RR /\ -u B <_ -u C /\ -u C <_ -u A ) ) )
22 21 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -u C e. ( -u B [,] -u A ) <-> ( -u C e. RR /\ -u B <_ -u C /\ -u C <_ -u A ) ) )
23 3anass 
 |-  ( ( -u C e. RR /\ -u B <_ -u C /\ -u C <_ -u A ) <-> ( -u C e. RR /\ ( -u B <_ -u C /\ -u C <_ -u A ) ) )
24 22 23 bitrdi 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -u C e. ( -u B [,] -u A ) <-> ( -u C e. RR /\ ( -u B <_ -u C /\ -u C <_ -u A ) ) ) )
25 13 17 24 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> -u C e. ( -u B [,] -u A ) ) )