Metamath Proof Explorer

Theorem fourierdlem19

Description: If two elements of D have the same periodic image in ( A (,] B ) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem19.a 
|- ( ph -> A e. RR )
fourierdlem19.b 
|- ( ph -> B e. RR )
fourierdlem19.altb 
|- ( ph -> A < B )
fourierdlem19.x 
|- ( ph -> X e. RR )
fourierdlem19.d 
|- D = { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
fourierdlem19.t 
|- T = ( B - A )
fourierdlem19.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem19.w 
|- ( ph -> W e. D )
fourierdlem19.z 
|- ( ph -> Z e. D )
fourierdlem19.ezew 
|- ( ph -> ( E ` Z ) = ( E ` W ) )
Assertion fourierdlem19 
|- ( ph -> -. W < Z )

Proof

Step Hyp Ref Expression
1 fourierdlem19.a 
 |-  ( ph -> A e. RR )
2 fourierdlem19.b 
 |-  ( ph -> B e. RR )
3 fourierdlem19.altb 
 |-  ( ph -> A < B )
4 fourierdlem19.x 
 |-  ( ph -> X e. RR )
5 fourierdlem19.d 
 |-  D = { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C }
6 fourierdlem19.t 
 |-  T = ( B - A )
7 fourierdlem19.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
8 fourierdlem19.w 
 |-  ( ph -> W e. D )
9 fourierdlem19.z 
 |-  ( ph -> Z e. D )
10 fourierdlem19.ezew 
 |-  ( ph -> ( E ` Z ) = ( E ` W ) )
11 1 4 readdcld 
 |-  ( ph -> ( A + X ) e. RR )
12 11 rexrd 
 |-  ( ph -> ( A + X ) e. RR* )
13 2 4 readdcld 
 |-  ( ph -> ( B + X ) e. RR )
14 13 rexrd 
 |-  ( ph -> ( B + X ) e. RR* )
15 ssrab2 
 |-  { y e. ( ( A + X ) (,] ( B + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. C } C_ ( ( A + X ) (,] ( B + X ) )
16 5 15 eqsstri 
 |-  D C_ ( ( A + X ) (,] ( B + X ) )
17 16 9 sseldi 
 |-  ( ph -> Z e. ( ( A + X ) (,] ( B + X ) ) )
18 iocleub 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR* /\ Z e. ( ( A + X ) (,] ( B + X ) ) ) -> Z <_ ( B + X ) )
19 12 14 17 18 syl3anc 
 |-  ( ph -> Z <_ ( B + X ) )
20 19 adantr 
 |-  ( ( ph /\ W < Z ) -> Z <_ ( B + X ) )
21 13 adantr 
 |-  ( ( ph /\ W < Z ) -> ( B + X ) e. RR )
22 iocssre 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR ) -> ( ( A + X ) (,] ( B + X ) ) C_ RR )
23 12 13 22 syl2anc 
 |-  ( ph -> ( ( A + X ) (,] ( B + X ) ) C_ RR )
24 16 8 sseldi 
 |-  ( ph -> W e. ( ( A + X ) (,] ( B + X ) ) )
25 23 24 sseldd 
 |-  ( ph -> W e. RR )
26 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
27 6 26 eqeltrid 
 |-  ( ph -> T e. RR )
28 25 27 readdcld 
 |-  ( ph -> ( W + T ) e. RR )
29 28 adantr 
 |-  ( ( ph /\ W < Z ) -> ( W + T ) e. RR )
30 23 17 sseldd 
 |-  ( ph -> Z e. RR )
31 30 adantr 
 |-  ( ( ph /\ W < Z ) -> Z e. RR )
32 6 eqcomi 
 |-  ( B - A ) = T
33 32 a1i 
 |-  ( ph -> ( B - A ) = T )
34 2 recnd 
 |-  ( ph -> B e. CC )
35 1 recnd 
 |-  ( ph -> A e. CC )
36 27 recnd 
 |-  ( ph -> T e. CC )
37 34 35 36 subaddd 
 |-  ( ph -> ( ( B - A ) = T <-> ( A + T ) = B ) )
38 33 37 mpbid 
 |-  ( ph -> ( A + T ) = B )
39 38 eqcomd 
 |-  ( ph -> B = ( A + T ) )
40 39 oveq1d 
 |-  ( ph -> ( B + X ) = ( ( A + T ) + X ) )
41 4 recnd 
 |-  ( ph -> X e. CC )
42 35 36 41 add32d 
 |-  ( ph -> ( ( A + T ) + X ) = ( ( A + X ) + T ) )
43 40 42 eqtrd 
 |-  ( ph -> ( B + X ) = ( ( A + X ) + T ) )
44 iocgtlb 
 |-  ( ( ( A + X ) e. RR* /\ ( B + X ) e. RR* /\ W e. ( ( A + X ) (,] ( B + X ) ) ) -> ( A + X ) < W )
45 12 14 24 44 syl3anc 
 |-  ( ph -> ( A + X ) < W )
46 11 25 27 45 ltadd1dd 
 |-  ( ph -> ( ( A + X ) + T ) < ( W + T ) )
47 43 46 eqbrtrd 
 |-  ( ph -> ( B + X ) < ( W + T ) )
48 47 adantr 
 |-  ( ( ph /\ W < Z ) -> ( B + X ) < ( W + T ) )
49 7 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
50 id 
 |-  ( x = W -> x = W )
51 oveq2 
 |-  ( x = W -> ( B - x ) = ( B - W ) )
52 51 oveq1d 
 |-  ( x = W -> ( ( B - x ) / T ) = ( ( B - W ) / T ) )
53 52 fveq2d 
 |-  ( x = W -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - W ) / T ) ) )
54 53 oveq1d 
 |-  ( x = W -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - W ) / T ) ) x. T ) )
55 50 54 oveq12d 
 |-  ( x = W -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) )
56 55 adantl 
 |-  ( ( ph /\ x = W ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) )
57 2 25 resubcld 
 |-  ( ph -> ( B - W ) e. RR )
58 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
59 3 58 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
60 59 6 breqtrrdi 
 |-  ( ph -> 0 < T )
61 60 gt0ne0d 
 |-  ( ph -> T =/= 0 )
62 57 27 61 redivcld 
 |-  ( ph -> ( ( B - W ) / T ) e. RR )
63 62 flcld 
 |-  ( ph -> ( |_ ` ( ( B - W ) / T ) ) e. ZZ )
64 63 zred 
 |-  ( ph -> ( |_ ` ( ( B - W ) / T ) ) e. RR )
65 64 27 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - W ) / T ) ) x. T ) e. RR )
66 25 65 readdcld 
 |-  ( ph -> ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) e. RR )
67 49 56 25 66 fvmptd 
 |-  ( ph -> ( E ` W ) = ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) )
68 67 66 eqeltrd 
 |-  ( ph -> ( E ` W ) e. RR )
69 68 recnd 
 |-  ( ph -> ( E ` W ) e. CC )
70 69 adantr 
 |-  ( ( ph /\ W < Z ) -> ( E ` W ) e. CC )
71 65 recnd 
 |-  ( ph -> ( ( |_ ` ( ( B - W ) / T ) ) x. T ) e. CC )
72 71 adantr 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - W ) / T ) ) x. T ) e. CC )
73 36 adantr 
 |-  ( ( ph /\ W < Z ) -> T e. CC )
74 70 72 73 subsubd 
 |-  ( ( ph /\ W < Z ) -> ( ( E ` W ) - ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) ) = ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) + T ) )
75 74 eqcomd 
 |-  ( ( ph /\ W < Z ) -> ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) + T ) = ( ( E ` W ) - ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) ) )
76 2 30 resubcld 
 |-  ( ph -> ( B - Z ) e. RR )
77 76 27 61 redivcld 
 |-  ( ph -> ( ( B - Z ) / T ) e. RR )
78 77 flcld 
 |-  ( ph -> ( |_ ` ( ( B - Z ) / T ) ) e. ZZ )
79 78 zred 
 |-  ( ph -> ( |_ ` ( ( B - Z ) / T ) ) e. RR )
80 79 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - Z ) / T ) ) e. RR )
81 27 adantr 
 |-  ( ( ph /\ W < Z ) -> T e. RR )
82 80 81 remulcld 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) e. RR )
83 64 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - W ) / T ) ) e. RR )
84 83 81 remulcld 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - W ) / T ) ) x. T ) e. RR )
85 84 81 resubcld 
 |-  ( ( ph /\ W < Z ) -> ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) e. RR )
86 68 adantr 
 |-  ( ( ph /\ W < Z ) -> ( E ` W ) e. RR )
87 79 27 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) e. RR )
88 87 recnd 
 |-  ( ph -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) e. CC )
89 88 36 pncand 
 |-  ( ph -> ( ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) - T ) = ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) )
90 89 eqcomd 
 |-  ( ph -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) = ( ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) - T ) )
91 90 adantr 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) = ( ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) - T ) )
92 82 81 readdcld 
 |-  ( ( ph /\ W < Z ) -> ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) e. RR )
93 79 recnd 
 |-  ( ph -> ( |_ ` ( ( B - Z ) / T ) ) e. CC )
94 93 36 adddirp1d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) x. T ) = ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) )
95 94 eqcomd 
 |-  ( ph -> ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) = ( ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) x. T ) )
96 95 adantr 
 |-  ( ( ph /\ W < Z ) -> ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) = ( ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) x. T ) )
97 1red 
 |-  ( ( ph /\ W < Z ) -> 1 e. RR )
98 80 97 readdcld 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) e. RR )
99 0red 
 |-  ( ph -> 0 e. RR )
100 99 27 60 ltled 
 |-  ( ph -> 0 <_ T )
101 100 adantr 
 |-  ( ( ph /\ W < Z ) -> 0 <_ T )
102 86 31 resubcld 
 |-  ( ( ph /\ W < Z ) -> ( ( E ` W ) - Z ) e. RR )
103 25 adantr 
 |-  ( ( ph /\ W < Z ) -> W e. RR )
104 86 103 resubcld 
 |-  ( ( ph /\ W < Z ) -> ( ( E ` W ) - W ) e. RR )
105 27 60 elrpd 
 |-  ( ph -> T e. RR+ )
106 105 adantr 
 |-  ( ( ph /\ W < Z ) -> T e. RR+ )
107 simpr 
 |-  ( ( ph /\ W < Z ) -> W < Z )
108 103 31 86 107 ltsub2dd 
 |-  ( ( ph /\ W < Z ) -> ( ( E ` W ) - Z ) < ( ( E ` W ) - W ) )
109 102 104 106 108 ltdiv1dd 
 |-  ( ( ph /\ W < Z ) -> ( ( ( E ` W ) - Z ) / T ) < ( ( ( E ` W ) - W ) / T ) )
110 id 
 |-  ( x = Z -> x = Z )
111 oveq2 
 |-  ( x = Z -> ( B - x ) = ( B - Z ) )
112 111 oveq1d 
 |-  ( x = Z -> ( ( B - x ) / T ) = ( ( B - Z ) / T ) )
113 112 fveq2d 
 |-  ( x = Z -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Z ) / T ) ) )
114 113 oveq1d 
 |-  ( x = Z -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) )
115 110 114 oveq12d 
 |-  ( x = Z -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
116 115 adantl 
 |-  ( ( ph /\ x = Z ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
117 30 87 readdcld 
 |-  ( ph -> ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) e. RR )
118 49 116 30 117 fvmptd 
 |-  ( ph -> ( E ` Z ) = ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
119 10 118 eqtr3d 
 |-  ( ph -> ( E ` W ) = ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
120 119 oveq1d 
 |-  ( ph -> ( ( E ` W ) - Z ) = ( ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) - Z ) )
121 30 recnd 
 |-  ( ph -> Z e. CC )
122 121 88 pncan2d 
 |-  ( ph -> ( ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) - Z ) = ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) )
123 120 122 eqtrd 
 |-  ( ph -> ( ( E ` W ) - Z ) = ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) )
124 123 oveq1d 
 |-  ( ph -> ( ( ( E ` W ) - Z ) / T ) = ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) / T ) )
125 93 36 61 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - Z ) / T ) ) )
126 124 125 eqtr2d 
 |-  ( ph -> ( |_ ` ( ( B - Z ) / T ) ) = ( ( ( E ` W ) - Z ) / T ) )
127 126 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - Z ) / T ) ) = ( ( ( E ` W ) - Z ) / T ) )
128 67 oveq1d 
 |-  ( ph -> ( ( E ` W ) - W ) = ( ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) - W ) )
129 128 oveq1d 
 |-  ( ph -> ( ( ( E ` W ) - W ) / T ) = ( ( ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) - W ) / T ) )
130 25 recnd 
 |-  ( ph -> W e. CC )
131 130 71 pncan2d 
 |-  ( ph -> ( ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) - W ) = ( ( |_ ` ( ( B - W ) / T ) ) x. T ) )
132 131 oveq1d 
 |-  ( ph -> ( ( ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) - W ) / T ) = ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) / T ) )
133 64 recnd 
 |-  ( ph -> ( |_ ` ( ( B - W ) / T ) ) e. CC )
134 133 36 61 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - W ) / T ) ) )
135 129 132 134 3eqtrrd 
 |-  ( ph -> ( |_ ` ( ( B - W ) / T ) ) = ( ( ( E ` W ) - W ) / T ) )
136 135 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - W ) / T ) ) = ( ( ( E ` W ) - W ) / T ) )
137 109 127 136 3brtr4d 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - Z ) / T ) ) < ( |_ ` ( ( B - W ) / T ) ) )
138 78 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - Z ) / T ) ) e. ZZ )
139 63 adantr 
 |-  ( ( ph /\ W < Z ) -> ( |_ ` ( ( B - W ) / T ) ) e. ZZ )
140 zltp1le 
 |-  ( ( ( |_ ` ( ( B - Z ) / T ) ) e. ZZ /\ ( |_ ` ( ( B - W ) / T ) ) e. ZZ ) -> ( ( |_ ` ( ( B - Z ) / T ) ) < ( |_ ` ( ( B - W ) / T ) ) <-> ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) <_ ( |_ ` ( ( B - W ) / T ) ) ) )
141 138 139 140 syl2anc 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) < ( |_ ` ( ( B - W ) / T ) ) <-> ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) <_ ( |_ ` ( ( B - W ) / T ) ) ) )
142 137 141 mpbid 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) <_ ( |_ ` ( ( B - W ) / T ) ) )
143 98 83 81 101 142 lemul1ad 
 |-  ( ( ph /\ W < Z ) -> ( ( ( |_ ` ( ( B - Z ) / T ) ) + 1 ) x. T ) <_ ( ( |_ ` ( ( B - W ) / T ) ) x. T ) )
144 96 143 eqbrtrd 
 |-  ( ( ph /\ W < Z ) -> ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) <_ ( ( |_ ` ( ( B - W ) / T ) ) x. T ) )
145 92 84 81 144 lesub1dd 
 |-  ( ( ph /\ W < Z ) -> ( ( ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) + T ) - T ) <_ ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) )
146 91 145 eqbrtrd 
 |-  ( ( ph /\ W < Z ) -> ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) <_ ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) )
147 82 85 86 146 lesub2dd 
 |-  ( ( ph /\ W < Z ) -> ( ( E ` W ) - ( ( ( |_ ` ( ( B - W ) / T ) ) x. T ) - T ) ) <_ ( ( E ` W ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
148 75 147 eqbrtrd 
 |-  ( ( ph /\ W < Z ) -> ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) + T ) <_ ( ( E ` W ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
149 67 eqcomd 
 |-  ( ph -> ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) = ( E ` W ) )
150 69 71 130 subadd2d 
 |-  ( ph -> ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) = W <-> ( W + ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) = ( E ` W ) ) )
151 149 150 mpbird 
 |-  ( ph -> ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) = W )
152 151 eqcomd 
 |-  ( ph -> W = ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) )
153 152 oveq1d 
 |-  ( ph -> ( W + T ) = ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) + T ) )
154 153 adantr 
 |-  ( ( ph /\ W < Z ) -> ( W + T ) = ( ( ( E ` W ) - ( ( |_ ` ( ( B - W ) / T ) ) x. T ) ) + T ) )
155 118 eqcomd 
 |-  ( ph -> ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) = ( E ` Z ) )
156 1 rexrd 
 |-  ( ph -> A e. RR* )
157 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
158 156 2 157 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
159 1 2 3 6 7 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
160 159 30 ffvelrnd 
 |-  ( ph -> ( E ` Z ) e. ( A (,] B ) )
161 158 160 sseldd 
 |-  ( ph -> ( E ` Z ) e. RR )
162 161 recnd 
 |-  ( ph -> ( E ` Z ) e. CC )
163 162 88 121 subadd2d 
 |-  ( ph -> ( ( ( E ` Z ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) = Z <-> ( Z + ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) = ( E ` Z ) ) )
164 155 163 mpbird 
 |-  ( ph -> ( ( E ` Z ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) = Z )
165 10 oveq1d 
 |-  ( ph -> ( ( E ` Z ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) = ( ( E ` W ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
166 164 165 eqtr3d 
 |-  ( ph -> Z = ( ( E ` W ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
167 166 adantr 
 |-  ( ( ph /\ W < Z ) -> Z = ( ( E ` W ) - ( ( |_ ` ( ( B - Z ) / T ) ) x. T ) ) )
168 148 154 167 3brtr4d 
 |-  ( ( ph /\ W < Z ) -> ( W + T ) <_ Z )
169 21 29 31 48 168 ltletrd 
 |-  ( ( ph /\ W < Z ) -> ( B + X ) < Z )
170 21 31 ltnled 
 |-  ( ( ph /\ W < Z ) -> ( ( B + X ) < Z <-> -. Z <_ ( B + X ) ) )
171 169 170 mpbid 
 |-  ( ( ph /\ W < Z ) -> -. Z <_ ( B + X ) )
172 20 171 pm2.65da 
 |-  ( ph -> -. W < Z )