Metamath Proof Explorer

Theorem iooshf

Description: Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion iooshf 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) e. ( C (,) D ) <-> A e. ( ( C + B ) (,) ( D + B ) ) ) )

Proof

Step Hyp Ref Expression
1 ltaddsub 
 |-  ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( ( C + B ) < A <-> C < ( A - B ) ) )
2 1 3com13 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + B ) < A <-> C < ( A - B ) ) )
3 2 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( C + B ) < A <-> C < ( A - B ) ) )
4 3 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( C + B ) < A <-> C < ( A - B ) ) )
5 ltsubadd 
 |-  ( ( A e. RR /\ B e. RR /\ D e. RR ) -> ( ( A - B ) < D <-> A < ( D + B ) ) )
6 5 bicomd 
 |-  ( ( A e. RR /\ B e. RR /\ D e. RR ) -> ( A < ( D + B ) <-> ( A - B ) < D ) )
7 6 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ D e. RR ) -> ( A < ( D + B ) <-> ( A - B ) < D ) )
8 7 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < ( D + B ) <-> ( A - B ) < D ) )
9 4 8 anbi12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( C + B ) < A /\ A < ( D + B ) ) <-> ( C < ( A - B ) /\ ( A - B ) < D ) ) )
10 readdcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR )
11 10 rexrd 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C + B ) e. RR* )
12 11 ad2ant2rl 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( A e. RR /\ B e. RR ) ) -> ( C + B ) e. RR* )
13 readdcl 
 |-  ( ( D e. RR /\ B e. RR ) -> ( D + B ) e. RR )
14 13 rexrd 
 |-  ( ( D e. RR /\ B e. RR ) -> ( D + B ) e. RR* )
15 14 ad2ant2l 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( A e. RR /\ B e. RR ) ) -> ( D + B ) e. RR* )
16 rexr 
 |-  ( A e. RR -> A e. RR* )
17 16 ad2antrl 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( A e. RR /\ B e. RR ) ) -> A e. RR* )
18 elioo5 
 |-  ( ( ( C + B ) e. RR* /\ ( D + B ) e. RR* /\ A e. RR* ) -> ( A e. ( ( C + B ) (,) ( D + B ) ) <-> ( ( C + B ) < A /\ A < ( D + B ) ) ) )
19 12 15 17 18 syl3anc 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( A e. RR /\ B e. RR ) ) -> ( A e. ( ( C + B ) (,) ( D + B ) ) <-> ( ( C + B ) < A /\ A < ( D + B ) ) ) )
20 19 ancoms 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A e. ( ( C + B ) (,) ( D + B ) ) <-> ( ( C + B ) < A /\ A < ( D + B ) ) ) )
21 rexr 
 |-  ( C e. RR -> C e. RR* )
22 21 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR* )
23 rexr 
 |-  ( D e. RR -> D e. RR* )
24 23 ad2antll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR* )
25 resubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
26 25 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR* )
27 26 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A - B ) e. RR* )
28 elioo5 
 |-  ( ( C e. RR* /\ D e. RR* /\ ( A - B ) e. RR* ) -> ( ( A - B ) e. ( C (,) D ) <-> ( C < ( A - B ) /\ ( A - B ) < D ) ) )
29 22 24 27 28 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) e. ( C (,) D ) <-> ( C < ( A - B ) /\ ( A - B ) < D ) ) )
30 9 20 29 3bitr4rd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) e. ( C (,) D ) <-> A e. ( ( C + B ) (,) ( D + B ) ) ) )