Metamath Proof Explorer

Theorem iooshift

Description: An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iooshift.1 
|- ( ph -> A e. RR )
iooshift.2 
|- ( ph -> B e. RR )
iooshift.3 
|- ( ph -> T e. RR )
Assertion iooshift 
|- ( ph -> ( ( A + T ) (,) ( B + T ) ) = { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )

Proof

Step Hyp Ref Expression
1 iooshift.1 
 |-  ( ph -> A e. RR )
2 iooshift.2 
 |-  ( ph -> B e. RR )
3 iooshift.3 
 |-  ( ph -> T e. RR )
4 eqeq1 
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
5 4 rexbidv 
 |-  ( w = x -> ( E. z e. ( A (,) B ) w = ( z + T ) <-> E. z e. ( A (,) B ) x = ( z + T ) ) )
6 5 elrab 
 |-  ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } <-> ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) )
7 simprr 
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) ) -> E. z e. ( A (,) B ) x = ( z + T ) )
8 nfv 
 |-  F/ z ph
9 nfv 
 |-  F/ z x e. CC
10 nfre1 
 |-  F/ z E. z e. ( A (,) B ) x = ( z + T )
11 9 10 nfan 
 |-  F/ z ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) )
12 8 11 nfan 
 |-  F/ z ( ph /\ ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) )
13 nfv 
 |-  F/ z x e. ( ( A + T ) (,) ( B + T ) )
14 simp3 
 |-  ( ( ph /\ z e. ( A (,) B ) /\ x = ( z + T ) ) -> x = ( z + T ) )
15 1 3 readdcld 
 |-  ( ph -> ( A + T ) e. RR )
16 15 rexrd 
 |-  ( ph -> ( A + T ) e. RR* )
17 16 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( A + T ) e. RR* )
18 2 3 readdcld 
 |-  ( ph -> ( B + T ) e. RR )
19 18 rexrd 
 |-  ( ph -> ( B + T ) e. RR* )
20 19 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( B + T ) e. RR* )
21 ioossre 
 |-  ( A (,) B ) C_ RR
22 21 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
23 22 sselda 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. RR )
24 3 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> T e. RR )
25 23 24 readdcld 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( z + T ) e. RR )
26 1 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> A e. RR )
27 26 rexrd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> A e. RR* )
28 2 adantr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> B e. RR )
29 28 rexrd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> B e. RR* )
30 simpr 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z e. ( A (,) B ) )
31 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. ( A (,) B ) ) -> A < z )
32 27 29 30 31 syl3anc 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> A < z )
33 26 23 24 32 ltadd1dd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( A + T ) < ( z + T ) )
34 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. ( A (,) B ) ) -> z < B )
35 27 29 30 34 syl3anc 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> z < B )
36 23 28 24 35 ltadd1dd 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( z + T ) < ( B + T ) )
37 17 20 25 33 36 eliood 
 |-  ( ( ph /\ z e. ( A (,) B ) ) -> ( z + T ) e. ( ( A + T ) (,) ( B + T ) ) )
38 37 3adant3 
 |-  ( ( ph /\ z e. ( A (,) B ) /\ x = ( z + T ) ) -> ( z + T ) e. ( ( A + T ) (,) ( B + T ) ) )
39 14 38 eqeltrd 
 |-  ( ( ph /\ z e. ( A (,) B ) /\ x = ( z + T ) ) -> x e. ( ( A + T ) (,) ( B + T ) ) )
40 39 3exp 
 |-  ( ph -> ( z e. ( A (,) B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) (,) ( B + T ) ) ) ) )
41 40 adantr 
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) ) -> ( z e. ( A (,) B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) (,) ( B + T ) ) ) ) )
42 12 13 41 rexlimd 
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) ) -> ( E. z e. ( A (,) B ) x = ( z + T ) -> x e. ( ( A + T ) (,) ( B + T ) ) ) )
43 7 42 mpd 
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A (,) B ) x = ( z + T ) ) ) -> x e. ( ( A + T ) (,) ( B + T ) ) )
44 6 43 sylan2b 
 |-  ( ( ph /\ x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } ) -> x e. ( ( A + T ) (,) ( B + T ) ) )
45 elioore 
 |-  ( x e. ( ( A + T ) (,) ( B + T ) ) -> x e. RR )
46 45 adantl 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x e. RR )
47 46 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x e. CC )
48 1 rexrd 
 |-  ( ph -> A e. RR* )
49 48 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> A e. RR* )
50 2 rexrd 
 |-  ( ph -> B e. RR* )
51 50 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> B e. RR* )
52 3 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> T e. RR )
53 46 52 resubcld 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( x - T ) e. RR )
54 1 recnd 
 |-  ( ph -> A e. CC )
55 3 recnd 
 |-  ( ph -> T e. CC )
56 54 55 pncand 
 |-  ( ph -> ( ( A + T ) - T ) = A )
57 56 eqcomd 
 |-  ( ph -> A = ( ( A + T ) - T ) )
58 57 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> A = ( ( A + T ) - T ) )
59 15 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( A + T ) e. RR )
60 16 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( A + T ) e. RR* )
61 19 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( B + T ) e. RR* )
62 simpr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x e. ( ( A + T ) (,) ( B + T ) ) )
63 ioogtlb 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( A + T ) < x )
64 60 61 62 63 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( A + T ) < x )
65 59 46 52 64 ltsub1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( ( A + T ) - T ) < ( x - T ) )
66 58 65 eqbrtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> A < ( x - T ) )
67 18 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( B + T ) e. RR )
68 iooltub 
 |-  ( ( ( A + T ) e. RR* /\ ( B + T ) e. RR* /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x < ( B + T ) )
69 60 61 62 68 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x < ( B + T ) )
70 46 67 52 69 ltsub1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( x - T ) < ( ( B + T ) - T ) )
71 2 recnd 
 |-  ( ph -> B e. CC )
72 71 55 pncand 
 |-  ( ph -> ( ( B + T ) - T ) = B )
73 72 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
74 70 73 breqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( x - T ) < B )
75 49 51 53 66 74 eliood 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( x - T ) e. ( A (,) B ) )
76 55 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> T e. CC )
77 47 76 npcand 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
78 77 eqcomd 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x = ( ( x - T ) + T ) )
79 oveq1 
 |-  ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
80 79 rspceeqv 
 |-  ( ( ( x - T ) e. ( A (,) B ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( A (,) B ) x = ( z + T ) )
81 75 78 80 syl2anc 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> E. z e. ( A (,) B ) x = ( z + T ) )
82 47 81 6 sylanbrc 
 |-  ( ( ph /\ x e. ( ( A + T ) (,) ( B + T ) ) ) -> x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )
83 44 82 impbida 
 |-  ( ph -> ( x e. { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } <-> x e. ( ( A + T ) (,) ( B + T ) ) ) )
84 83 eqrdv 
 |-  ( ph -> { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } = ( ( A + T ) (,) ( B + T ) ) )
85 84 eqcomd 
 |-  ( ph -> ( ( A + T ) (,) ( B + T ) ) = { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )