Metamath Proof Explorer

Theorem icoshft

Description: A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008)

Ref Expression
Assertion icoshft 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( B e. RR -> B e. RR* )
2 elico2 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( X e. ( A [,) B ) <-> ( X e. RR /\ A <_ X /\ X < B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( X e. ( A [,) B ) <-> ( X e. RR /\ A <_ X /\ X < B ) ) )
4 3 biimpd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( X e. ( A [,) B ) -> ( X e. RR /\ A <_ X /\ X < B ) ) )
5 4 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X e. RR /\ A <_ X /\ X < B ) ) )
6 3anass 
 |-  ( ( X e. RR /\ A <_ X /\ X < B ) <-> ( X e. RR /\ ( A <_ X /\ X < B ) ) )
7 5 6 syl6ib 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X e. RR /\ ( A <_ X /\ X < B ) ) ) )
8 leadd1 
 |-  ( ( A e. RR /\ X e. RR /\ C e. RR ) -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) )
9 8 3com12 
 |-  ( ( X e. RR /\ A e. RR /\ C e. RR ) -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) )
10 9 3expib 
 |-  ( X e. RR -> ( ( A e. RR /\ C e. RR ) -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) ) )
11 10 com12 
 |-  ( ( A e. RR /\ C e. RR ) -> ( X e. RR -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) ) )
12 11 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. RR -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) ) )
13 12 imp 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ X e. RR ) -> ( A <_ X <-> ( A + C ) <_ ( X + C ) ) )
14 ltadd1 
 |-  ( ( X e. RR /\ B e. RR /\ C e. RR ) -> ( X < B <-> ( X + C ) < ( B + C ) ) )
15 14 3expib 
 |-  ( X e. RR -> ( ( B e. RR /\ C e. RR ) -> ( X < B <-> ( X + C ) < ( B + C ) ) ) )
16 15 com12 
 |-  ( ( B e. RR /\ C e. RR ) -> ( X e. RR -> ( X < B <-> ( X + C ) < ( B + C ) ) ) )
17 16 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. RR -> ( X < B <-> ( X + C ) < ( B + C ) ) ) )
18 17 imp 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ X e. RR ) -> ( X < B <-> ( X + C ) < ( B + C ) ) )
19 13 18 anbi12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ X e. RR ) -> ( ( A <_ X /\ X < B ) <-> ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
20 19 pm5.32da 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( X e. RR /\ ( A <_ X /\ X < B ) ) <-> ( X e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) ) )
21 readdcl 
 |-  ( ( X e. RR /\ C e. RR ) -> ( X + C ) e. RR )
22 21 expcom 
 |-  ( C e. RR -> ( X e. RR -> ( X + C ) e. RR ) )
23 22 anim1d 
 |-  ( C e. RR -> ( ( X e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) -> ( ( X + C ) e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) ) )
24 3anass 
 |-  ( ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) <-> ( ( X + C ) e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
25 23 24 syl6ibr 
 |-  ( C e. RR -> ( ( X e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) -> ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
26 25 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( X e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) -> ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
27 readdcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + C ) e. RR )
28 27 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + C ) e. RR )
29 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
30 29 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
31 rexr 
 |-  ( ( B + C ) e. RR -> ( B + C ) e. RR* )
32 elico2 
 |-  ( ( ( A + C ) e. RR /\ ( B + C ) e. RR* ) -> ( ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) <-> ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
33 31 32 sylan2 
 |-  ( ( ( A + C ) e. RR /\ ( B + C ) e. RR ) -> ( ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) <-> ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) )
34 33 biimprd 
 |-  ( ( ( A + C ) e. RR /\ ( B + C ) e. RR ) -> ( ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
35 28 30 34 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( X + C ) e. RR /\ ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
36 26 35 syld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( X e. RR /\ ( ( A + C ) <_ ( X + C ) /\ ( X + C ) < ( B + C ) ) ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
37 20 36 sylbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( X e. RR /\ ( A <_ X /\ X < B ) ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
38 7 37 syld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )