Metamath Proof Explorer

Theorem iooneg

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

Ref Expression
Assertion iooneg 
|- ( ( 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 ltneg 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A < C <-> -u C < -u A ) )
2 1 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < C <-> -u C < -u A ) )
3 ltneg 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C < B <-> -u B < -u C ) )
4 3 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C < B <-> -u B < -u C ) )
5 4 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C < B <-> -u B < -u C ) )
6 2 5 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < C /\ C < B ) <-> ( -u C < -u A /\ -u B < -u C ) ) )
7 6 biancomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < C /\ C < B ) <-> ( -u B < -u C /\ -u C < -u A ) ) )
8 rexr 
 |-  ( A e. RR -> A e. RR* )
9 rexr 
 |-  ( B e. RR -> B e. RR* )
10 rexr 
 |-  ( C e. RR -> C e. RR* )
11 elioo5 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )
12 8 9 10 11 syl3an 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )
13 renegcl 
 |-  ( B e. RR -> -u B e. RR )
14 renegcl 
 |-  ( A e. RR -> -u A e. RR )
15 renegcl 
 |-  ( C e. RR -> -u C e. RR )
16 rexr 
 |-  ( -u B e. RR -> -u B e. RR* )
17 rexr 
 |-  ( -u A e. RR -> -u A e. RR* )
18 rexr 
 |-  ( -u C e. RR -> -u C e. RR* )
19 elioo5 
 |-  ( ( -u B e. RR* /\ -u A e. RR* /\ -u C e. RR* ) -> ( -u C e. ( -u B (,) -u A ) <-> ( -u B < -u C /\ -u C < -u A ) ) )
20 16 17 18 19 syl3an 
 |-  ( ( -u B e. RR /\ -u A e. RR /\ -u C e. RR ) -> ( -u C e. ( -u B (,) -u A ) <-> ( -u B < -u C /\ -u C < -u A ) ) )
21 13 14 15 20 syl3an 
 |-  ( ( B e. RR /\ A e. RR /\ C e. RR ) -> ( -u C e. ( -u B (,) -u A ) <-> ( -u B < -u C /\ -u C < -u A ) ) )
22 21 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -u C e. ( -u B (,) -u A ) <-> ( -u B < -u C /\ -u C < -u A ) ) )
23 7 12 22 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A (,) B ) <-> -u C e. ( -u B (,) -u A ) ) )