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 ) } )