Metamath Proof Explorer

Theorem iccshift

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

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

Proof

Step Hyp Ref Expression
1 iccshift.1 
 |-  ( ph -> A e. RR )
2 iccshift.2 
 |-  ( ph -> B e. RR )
3 iccshift.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 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
16 15 sselda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z e. RR )
17 3 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> T e. RR )
18 16 17 readdcld 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) e. RR )
19 1 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> A e. RR )
20 simpr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
21 2 adantr 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> B e. RR )
22 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
23 19 21 22 syl2anc 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
24 20 23 mpbid 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. RR /\ A <_ z /\ z <_ B ) )
25 24 simp2d 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> A <_ z )
26 19 16 17 25 leadd1dd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( A + T ) <_ ( z + T ) )
27 24 simp3d 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z <_ B )
28 16 21 17 27 leadd1dd 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) <_ ( B + T ) )
29 18 26 28 3jca 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
30 29 3adant3 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
31 1 3 readdcld 
 |-  ( ph -> ( A + T ) e. RR )
32 31 3ad2ant1 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( A + T ) e. RR )
33 2 3 readdcld 
 |-  ( ph -> ( B + T ) e. RR )
34 33 3ad2ant1 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( B + T ) e. RR )
35 elicc2 
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) ) )
36 32 34 35 syl2anc 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) ) )
37 30 36 mpbird 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) )
38 14 37 eqeltrd 
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
39 38 3exp 
 |-  ( ph -> ( z e. ( A [,] B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) ) )
40 39 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 ) ) ) ) )
41 12 13 40 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 ) ) ) )
42 7 41 mpd 
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
43 6 42 sylan2b 
 |-  ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
44 31 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
45 33 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
46 simpr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
47 eliccre 
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
48 44 45 46 47 syl3anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
49 48 recnd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
50 1 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
51 2 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 48 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 elicc2 
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
60 44 45 59 syl2anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
61 46 60 mpbid 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) )
62 61 simp2d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
63 44 48 52 62 lesub1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) - T ) <_ ( x - T ) )
64 58 63 eqbrtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x - T ) )
65 61 simp3d 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
66 48 45 52 65 lesub1dd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ ( ( B + T ) - T ) )
67 2 recnd 
 |-  ( ph -> B e. CC )
68 67 55 pncand 
 |-  ( ph -> ( ( B + T ) - T ) = B )
69 68 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
70 66 69 breqtrd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ B )
71 50 51 53 64 70 eliccd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
72 55 adantr 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
73 49 72 npcand 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
74 73 eqcomd 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x = ( ( x - T ) + T ) )
75 oveq1 
 |-  ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
76 75 rspceeqv 
 |-  ( ( ( x - T ) e. ( A [,] B ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
77 71 74 76 syl2anc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
78 49 77 6 sylanbrc 
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
79 43 78 impbida 
 |-  ( ph -> ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> x e. ( ( A + T ) [,] ( B + T ) ) ) )
80 79 eqrdv 
 |-  ( ph -> { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = ( ( A + T ) [,] ( B + T ) ) )
81 80 eqcomd 
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) = { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )