Metamath Proof Explorer

Theorem fourierdlem26

Description: Periodic image of a point Y that's in the period that begins with the point X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem26.1 
|- ( ph -> A e. RR )
fourierdlem26.2 
|- ( ph -> B e. RR )
fourierdlem26.3 
|- ( ph -> A < B )
fourierdlem26.4 
|- T = ( B - A )
fourierdlem26.5 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem26.6 
|- ( ph -> X e. RR )
fourierdlem26.7 
|- ( ph -> ( E ` X ) = B )
fourierdlem26.8 
|- ( ph -> Y e. ( X (,] ( X + T ) ) )
Assertion fourierdlem26 
|- ( ph -> ( E ` Y ) = ( A + ( Y - X ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem26.1 
 |-  ( ph -> A e. RR )
2 fourierdlem26.2 
 |-  ( ph -> B e. RR )
3 fourierdlem26.3 
 |-  ( ph -> A < B )
4 fourierdlem26.4 
 |-  T = ( B - A )
5 fourierdlem26.5 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
6 fourierdlem26.6 
 |-  ( ph -> X e. RR )
7 fourierdlem26.7 
 |-  ( ph -> ( E ` X ) = B )
8 fourierdlem26.8 
 |-  ( ph -> Y e. ( X (,] ( X + T ) ) )
9 5 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
10 simpr 
 |-  ( ( ph /\ x = Y ) -> x = Y )
11 10 oveq2d 
 |-  ( ( ph /\ x = Y ) -> ( B - x ) = ( B - Y ) )
12 11 oveq1d 
 |-  ( ( ph /\ x = Y ) -> ( ( B - x ) / T ) = ( ( B - Y ) / T ) )
13 12 fveq2d 
 |-  ( ( ph /\ x = Y ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Y ) / T ) ) )
14 13 oveq1d 
 |-  ( ( ph /\ x = Y ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) )
15 10 14 oveq12d 
 |-  ( ( ph /\ x = Y ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
16 6 rexrd 
 |-  ( ph -> X e. RR* )
17 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
18 4 17 eqeltrid 
 |-  ( ph -> T e. RR )
19 6 18 readdcld 
 |-  ( ph -> ( X + T ) e. RR )
20 elioc2 
 |-  ( ( X e. RR* /\ ( X + T ) e. RR ) -> ( Y e. ( X (,] ( X + T ) ) <-> ( Y e. RR /\ X < Y /\ Y <_ ( X + T ) ) ) )
21 16 19 20 syl2anc 
 |-  ( ph -> ( Y e. ( X (,] ( X + T ) ) <-> ( Y e. RR /\ X < Y /\ Y <_ ( X + T ) ) ) )
22 8 21 mpbid 
 |-  ( ph -> ( Y e. RR /\ X < Y /\ Y <_ ( X + T ) ) )
23 22 simp1d 
 |-  ( ph -> Y e. RR )
24 2 23 resubcld 
 |-  ( ph -> ( B - Y ) e. RR )
25 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
26 3 25 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
27 26 4 breqtrrdi 
 |-  ( ph -> 0 < T )
28 27 gt0ne0d 
 |-  ( ph -> T =/= 0 )
29 24 18 28 redivcld 
 |-  ( ph -> ( ( B - Y ) / T ) e. RR )
30 29 flcld 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. ZZ )
31 30 zred 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. RR )
32 31 18 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. RR )
33 23 32 readdcld 
 |-  ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) e. RR )
34 9 15 23 33 fvmptd 
 |-  ( ph -> ( E ` Y ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) )
35 6 recnd 
 |-  ( ph -> X e. CC )
36 23 recnd 
 |-  ( ph -> Y e. CC )
37 35 36 pncan3d 
 |-  ( ph -> ( X + ( Y - X ) ) = Y )
38 37 eqcomd 
 |-  ( ph -> Y = ( X + ( Y - X ) ) )
39 38 oveq2d 
 |-  ( ph -> ( B - Y ) = ( B - ( X + ( Y - X ) ) ) )
40 2 recnd 
 |-  ( ph -> B e. CC )
41 36 35 subcld 
 |-  ( ph -> ( Y - X ) e. CC )
42 40 35 41 subsub4d 
 |-  ( ph -> ( ( B - X ) - ( Y - X ) ) = ( B - ( X + ( Y - X ) ) ) )
43 39 42 eqtr4d 
 |-  ( ph -> ( B - Y ) = ( ( B - X ) - ( Y - X ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( B - Y ) / T ) = ( ( ( B - X ) - ( Y - X ) ) / T ) )
45 2 6 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
46 45 recnd 
 |-  ( ph -> ( B - X ) e. CC )
47 18 recnd 
 |-  ( ph -> T e. CC )
48 46 41 47 28 divsubdird 
 |-  ( ph -> ( ( ( B - X ) - ( Y - X ) ) / T ) = ( ( ( B - X ) / T ) - ( ( Y - X ) / T ) ) )
49 41 47 28 divnegd 
 |-  ( ph -> -u ( ( Y - X ) / T ) = ( -u ( Y - X ) / T ) )
50 36 35 negsubdi2d 
 |-  ( ph -> -u ( Y - X ) = ( X - Y ) )
51 50 oveq1d 
 |-  ( ph -> ( -u ( Y - X ) / T ) = ( ( X - Y ) / T ) )
52 49 51 eqtrd 
 |-  ( ph -> -u ( ( Y - X ) / T ) = ( ( X - Y ) / T ) )
53 52 oveq2d 
 |-  ( ph -> ( ( ( B - X ) / T ) + -u ( ( Y - X ) / T ) ) = ( ( ( B - X ) / T ) + ( ( X - Y ) / T ) ) )
54 45 18 28 redivcld 
 |-  ( ph -> ( ( B - X ) / T ) e. RR )
55 54 recnd 
 |-  ( ph -> ( ( B - X ) / T ) e. CC )
56 41 47 28 divcld 
 |-  ( ph -> ( ( Y - X ) / T ) e. CC )
57 55 56 negsubd 
 |-  ( ph -> ( ( ( B - X ) / T ) + -u ( ( Y - X ) / T ) ) = ( ( ( B - X ) / T ) - ( ( Y - X ) / T ) ) )
58 1cnd 
 |-  ( ph -> 1 e. CC )
59 55 58 npcand 
 |-  ( ph -> ( ( ( ( B - X ) / T ) - 1 ) + 1 ) = ( ( B - X ) / T ) )
60 59 eqcomd 
 |-  ( ph -> ( ( B - X ) / T ) = ( ( ( ( B - X ) / T ) - 1 ) + 1 ) )
61 60 oveq1d 
 |-  ( ph -> ( ( ( B - X ) / T ) + ( ( X - Y ) / T ) ) = ( ( ( ( ( B - X ) / T ) - 1 ) + 1 ) + ( ( X - Y ) / T ) ) )
62 55 58 subcld 
 |-  ( ph -> ( ( ( B - X ) / T ) - 1 ) e. CC )
63 35 36 subcld 
 |-  ( ph -> ( X - Y ) e. CC )
64 63 47 28 divcld 
 |-  ( ph -> ( ( X - Y ) / T ) e. CC )
65 62 58 64 addassd 
 |-  ( ph -> ( ( ( ( ( B - X ) / T ) - 1 ) + 1 ) + ( ( X - Y ) / T ) ) = ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) )
66 61 65 eqtrd 
 |-  ( ph -> ( ( ( B - X ) / T ) + ( ( X - Y ) / T ) ) = ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) )
67 53 57 66 3eqtr3d 
 |-  ( ph -> ( ( ( B - X ) / T ) - ( ( Y - X ) / T ) ) = ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) )
68 44 48 67 3eqtrd 
 |-  ( ph -> ( ( B - Y ) / T ) = ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) )
69 68 fveq2d 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) = ( |_ ` ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) ) )
70 6 23 resubcld 
 |-  ( ph -> ( X - Y ) e. RR )
71 18 70 readdcld 
 |-  ( ph -> ( T + ( X - Y ) ) e. RR )
72 18 27 elrpd 
 |-  ( ph -> T e. RR+ )
73 35 47 addcomd 
 |-  ( ph -> ( X + T ) = ( T + X ) )
74 73 oveq2d 
 |-  ( ph -> ( X (,] ( X + T ) ) = ( X (,] ( T + X ) ) )
75 8 74 eleqtrd 
 |-  ( ph -> Y e. ( X (,] ( T + X ) ) )
76 18 6 readdcld 
 |-  ( ph -> ( T + X ) e. RR )
77 elioc2 
 |-  ( ( X e. RR* /\ ( T + X ) e. RR ) -> ( Y e. ( X (,] ( T + X ) ) <-> ( Y e. RR /\ X < Y /\ Y <_ ( T + X ) ) ) )
78 16 76 77 syl2anc 
 |-  ( ph -> ( Y e. ( X (,] ( T + X ) ) <-> ( Y e. RR /\ X < Y /\ Y <_ ( T + X ) ) ) )
79 75 78 mpbid 
 |-  ( ph -> ( Y e. RR /\ X < Y /\ Y <_ ( T + X ) ) )
80 79 simp3d 
 |-  ( ph -> Y <_ ( T + X ) )
81 23 6 18 lesubaddd 
 |-  ( ph -> ( ( Y - X ) <_ T <-> Y <_ ( T + X ) ) )
82 80 81 mpbird 
 |-  ( ph -> ( Y - X ) <_ T )
83 23 6 resubcld 
 |-  ( ph -> ( Y - X ) e. RR )
84 18 83 subge0d 
 |-  ( ph -> ( 0 <_ ( T - ( Y - X ) ) <-> ( Y - X ) <_ T ) )
85 82 84 mpbird 
 |-  ( ph -> 0 <_ ( T - ( Y - X ) ) )
86 47 36 35 subsub2d 
 |-  ( ph -> ( T - ( Y - X ) ) = ( T + ( X - Y ) ) )
87 85 86 breqtrd 
 |-  ( ph -> 0 <_ ( T + ( X - Y ) ) )
88 71 72 87 divge0d 
 |-  ( ph -> 0 <_ ( ( T + ( X - Y ) ) / T ) )
89 47 63 47 28 divdird 
 |-  ( ph -> ( ( T + ( X - Y ) ) / T ) = ( ( T / T ) + ( ( X - Y ) / T ) ) )
90 47 28 dividd 
 |-  ( ph -> ( T / T ) = 1 )
91 90 eqcomd 
 |-  ( ph -> 1 = ( T / T ) )
92 91 oveq1d 
 |-  ( ph -> ( 1 + ( ( X - Y ) / T ) ) = ( ( T / T ) + ( ( X - Y ) / T ) ) )
93 89 92 eqtr4d 
 |-  ( ph -> ( ( T + ( X - Y ) ) / T ) = ( 1 + ( ( X - Y ) / T ) ) )
94 88 93 breqtrd 
 |-  ( ph -> 0 <_ ( 1 + ( ( X - Y ) / T ) ) )
95 22 simp2d 
 |-  ( ph -> X < Y )
96 6 23 sublt0d 
 |-  ( ph -> ( ( X - Y ) < 0 <-> X < Y ) )
97 95 96 mpbird 
 |-  ( ph -> ( X - Y ) < 0 )
98 70 72 97 divlt0gt0d 
 |-  ( ph -> ( ( X - Y ) / T ) < 0 )
99 70 18 28 redivcld 
 |-  ( ph -> ( ( X - Y ) / T ) e. RR )
100 1red 
 |-  ( ph -> 1 e. RR )
101 ltaddneg 
 |-  ( ( ( ( X - Y ) / T ) e. RR /\ 1 e. RR ) -> ( ( ( X - Y ) / T ) < 0 <-> ( 1 + ( ( X - Y ) / T ) ) < 1 ) )
102 99 100 101 syl2anc 
 |-  ( ph -> ( ( ( X - Y ) / T ) < 0 <-> ( 1 + ( ( X - Y ) / T ) ) < 1 ) )
103 98 102 mpbid 
 |-  ( ph -> ( 1 + ( ( X - Y ) / T ) ) < 1 )
104 54 flcld 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
105 104 zcnd 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
106 105 47 mulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
107 35 106 pncan2d 
 |-  ( ph -> ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
108 107 eqcomd 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) )
109 108 oveq1d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) / T ) = ( ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) / T ) )
110 105 47 28 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - X ) / T ) ) )
111 id 
 |-  ( x = X -> x = X )
112 oveq2 
 |-  ( x = X -> ( B - x ) = ( B - X ) )
113 112 oveq1d 
 |-  ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
114 113 fveq2d 
 |-  ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
115 114 oveq1d 
 |-  ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
116 111 115 oveq12d 
 |-  ( x = X -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
117 116 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
118 reflcl 
 |-  ( ( ( B - X ) / T ) e. RR -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
119 54 118 syl 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
120 119 18 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
121 6 120 readdcld 
 |-  ( ph -> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
122 9 117 6 121 fvmptd 
 |-  ( ph -> ( E ` X ) = ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
123 122 eqcomd 
 |-  ( ph -> ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( E ` X ) )
124 123 oveq1d 
 |-  ( ph -> ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) = ( ( E ` X ) - X ) )
125 124 oveq1d 
 |-  ( ph -> ( ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) / T ) = ( ( ( E ` X ) - X ) / T ) )
126 7 oveq1d 
 |-  ( ph -> ( ( E ` X ) - X ) = ( B - X ) )
127 126 oveq1d 
 |-  ( ph -> ( ( ( E ` X ) - X ) / T ) = ( ( B - X ) / T ) )
128 125 127 eqtrd 
 |-  ( ph -> ( ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - X ) / T ) = ( ( B - X ) / T ) )
129 109 110 128 3eqtr3d 
 |-  ( ph -> ( |_ ` ( ( B - X ) / T ) ) = ( ( B - X ) / T ) )
130 129 104 eqeltrrd 
 |-  ( ph -> ( ( B - X ) / T ) e. ZZ )
131 1zzd 
 |-  ( ph -> 1 e. ZZ )
132 130 131 zsubcld 
 |-  ( ph -> ( ( ( B - X ) / T ) - 1 ) e. ZZ )
133 100 99 readdcld 
 |-  ( ph -> ( 1 + ( ( X - Y ) / T ) ) e. RR )
134 flbi2 
 |-  ( ( ( ( ( B - X ) / T ) - 1 ) e. ZZ /\ ( 1 + ( ( X - Y ) / T ) ) e. RR ) -> ( ( |_ ` ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) ) = ( ( ( B - X ) / T ) - 1 ) <-> ( 0 <_ ( 1 + ( ( X - Y ) / T ) ) /\ ( 1 + ( ( X - Y ) / T ) ) < 1 ) ) )
135 132 133 134 syl2anc 
 |-  ( ph -> ( ( |_ ` ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) ) = ( ( ( B - X ) / T ) - 1 ) <-> ( 0 <_ ( 1 + ( ( X - Y ) / T ) ) /\ ( 1 + ( ( X - Y ) / T ) ) < 1 ) ) )
136 94 103 135 mpbir2and 
 |-  ( ph -> ( |_ ` ( ( ( ( B - X ) / T ) - 1 ) + ( 1 + ( ( X - Y ) / T ) ) ) ) = ( ( ( B - X ) / T ) - 1 ) )
137 129 eqcomd 
 |-  ( ph -> ( ( B - X ) / T ) = ( |_ ` ( ( B - X ) / T ) ) )
138 137 oveq1d 
 |-  ( ph -> ( ( ( B - X ) / T ) - 1 ) = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) )
139 69 136 138 3eqtrd 
 |-  ( ph -> ( |_ ` ( ( B - Y ) / T ) ) = ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) )
140 139 oveq1d 
 |-  ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) = ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) )
141 140 oveq2d 
 |-  ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) = ( Y + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
142 38 oveq1d 
 |-  ( ph -> ( Y + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) = ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) )
143 105 58 47 subdird 
 |-  ( ph -> ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) = ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - ( 1 x. T ) ) )
144 143 oveq2d 
 |-  ( ph -> ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) = ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - ( 1 x. T ) ) ) )
145 35 41 addcld 
 |-  ( ph -> ( X + ( Y - X ) ) e. CC )
146 58 47 mulcld 
 |-  ( ph -> ( 1 x. T ) e. CC )
147 145 106 146 addsubassd 
 |-  ( ph -> ( ( ( X + ( Y - X ) ) + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( 1 x. T ) ) = ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - ( 1 x. T ) ) ) )
148 147 eqcomd 
 |-  ( ph -> ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) x. T ) - ( 1 x. T ) ) ) = ( ( ( X + ( Y - X ) ) + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( 1 x. T ) ) )
149 35 41 106 add32d 
 |-  ( ph -> ( ( X + ( Y - X ) ) + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + ( Y - X ) ) )
150 149 oveq1d 
 |-  ( ph -> ( ( ( X + ( Y - X ) ) + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( 1 x. T ) ) = ( ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + ( Y - X ) ) - ( 1 x. T ) ) )
151 123 oveq1d 
 |-  ( ph -> ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + ( Y - X ) ) = ( ( E ` X ) + ( Y - X ) ) )
152 47 mullidd 
 |-  ( ph -> ( 1 x. T ) = T )
153 151 152 oveq12d 
 |-  ( ph -> ( ( ( X + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + ( Y - X ) ) - ( 1 x. T ) ) = ( ( ( E ` X ) + ( Y - X ) ) - T ) )
154 7 2 eqeltrd 
 |-  ( ph -> ( E ` X ) e. RR )
155 154 recnd 
 |-  ( ph -> ( E ` X ) e. CC )
156 155 41 47 addsubd 
 |-  ( ph -> ( ( ( E ` X ) + ( Y - X ) ) - T ) = ( ( ( E ` X ) - T ) + ( Y - X ) ) )
157 7 oveq1d 
 |-  ( ph -> ( ( E ` X ) - T ) = ( B - T ) )
158 4 a1i 
 |-  ( ph -> T = ( B - A ) )
159 158 oveq2d 
 |-  ( ph -> ( B - T ) = ( B - ( B - A ) ) )
160 1 recnd 
 |-  ( ph -> A e. CC )
161 40 160 nncand 
 |-  ( ph -> ( B - ( B - A ) ) = A )
162 157 159 161 3eqtrd 
 |-  ( ph -> ( ( E ` X ) - T ) = A )
163 162 oveq1d 
 |-  ( ph -> ( ( ( E ` X ) - T ) + ( Y - X ) ) = ( A + ( Y - X ) ) )
164 156 163 eqtrd 
 |-  ( ph -> ( ( ( E ` X ) + ( Y - X ) ) - T ) = ( A + ( Y - X ) ) )
165 150 153 164 3eqtrd 
 |-  ( ph -> ( ( ( X + ( Y - X ) ) + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( 1 x. T ) ) = ( A + ( Y - X ) ) )
166 144 148 165 3eqtrd 
 |-  ( ph -> ( ( X + ( Y - X ) ) + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) = ( A + ( Y - X ) ) )
167 142 166 eqtrd 
 |-  ( ph -> ( Y + ( ( ( |_ ` ( ( B - X ) / T ) ) - 1 ) x. T ) ) = ( A + ( Y - X ) ) )
168 34 141 167 3eqtrd 
 |-  ( ph -> ( E ` Y ) = ( A + ( Y - X ) ) )