Metamath Proof Explorer


Theorem fourierdlem79

Description: E projects every interval of the partition induced by S on H into a corresponding interval of the partition induced by Q on [ A , B ] . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem79.t T = B A
fourierdlem79.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem79.m φ M
fourierdlem79.q φ Q P M
fourierdlem79.c φ C
fourierdlem79.d φ D
fourierdlem79.cltd φ C < D
fourierdlem79.o O = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
fourierdlem79.h H = C D x C D | k x + k T ran Q
fourierdlem79.n N = H 1
fourierdlem79.s S = ι f | f Isom < , < 0 N H
fourierdlem79.e E = x x + B x T T
fourierdlem79.l L = y A B if y = B A y
fourierdlem79.z Z = S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
fourierdlem79.i I = x sup i 0 ..^ M | Q i L E x <
Assertion fourierdlem79 φ j 0 ..^ N L E S j E S j + 1 Q I S j Q I S j + 1

Proof

Step Hyp Ref Expression
1 fourierdlem79.t T = B A
2 fourierdlem79.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
3 fourierdlem79.m φ M
4 fourierdlem79.q φ Q P M
5 fourierdlem79.c φ C
6 fourierdlem79.d φ D
7 fourierdlem79.cltd φ C < D
8 fourierdlem79.o O = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
9 fourierdlem79.h H = C D x C D | k x + k T ran Q
10 fourierdlem79.n N = H 1
11 fourierdlem79.s S = ι f | f Isom < , < 0 N H
12 fourierdlem79.e E = x x + B x T T
13 fourierdlem79.l L = y A B if y = B A y
14 fourierdlem79.z Z = S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
15 fourierdlem79.i I = x sup i 0 ..^ M | Q i L E x <
16 2 fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
17 3 16 syl φ Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
18 4 17 mpbid φ Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
19 18 simpld φ Q 0 M
20 elmapi Q 0 M Q : 0 M
21 19 20 syl φ Q : 0 M
22 21 adantr φ j 0 ..^ N Q : 0 M
23 2 3 4 1 12 13 15 fourierdlem37 φ I : 0 ..^ M x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
24 23 simpld φ I : 0 ..^ M
25 fzossfz 0 ..^ M 0 M
26 25 a1i φ 0 ..^ M 0 M
27 24 26 fssd φ I : 0 M
28 27 adantr φ j 0 ..^ N I : 0 M
29 1 2 3 4 5 6 7 8 9 10 11 fourierdlem54 φ N S O N S Isom < , < 0 N H
30 29 simpld φ N S O N
31 30 simprd φ S O N
32 31 adantr φ j 0 ..^ N S O N
33 30 simpld φ N
34 33 adantr φ j 0 ..^ N N
35 8 fourierdlem2 N S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
36 34 35 syl φ j 0 ..^ N S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
37 32 36 mpbid φ j 0 ..^ N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
38 37 simpld φ j 0 ..^ N S 0 N
39 elmapi S 0 N S : 0 N
40 38 39 syl φ j 0 ..^ N S : 0 N
41 elfzofz j 0 ..^ N j 0 N
42 41 adantl φ j 0 ..^ N j 0 N
43 40 42 ffvelrnd φ j 0 ..^ N S j
44 28 43 ffvelrnd φ j 0 ..^ N I S j 0 M
45 22 44 ffvelrnd φ j 0 ..^ N Q I S j
46 45 rexrd φ j 0 ..^ N Q I S j *
47 24 adantr φ j 0 ..^ N I : 0 ..^ M
48 47 43 ffvelrnd φ j 0 ..^ N I S j 0 ..^ M
49 fzofzp1 I S j 0 ..^ M I S j + 1 0 M
50 48 49 syl φ j 0 ..^ N I S j + 1 0 M
51 22 50 ffvelrnd φ j 0 ..^ N Q I S j + 1
52 51 rexrd φ j 0 ..^ N Q I S j + 1 *
53 15 a1i φ j 0 ..^ N I = x sup i 0 ..^ M | Q i L E x <
54 fveq2 x = S j E x = E S j
55 54 fveq2d x = S j L E x = L E S j
56 55 breq2d x = S j Q i L E x Q i L E S j
57 56 rabbidv x = S j i 0 ..^ M | Q i L E x = i 0 ..^ M | Q i L E S j
58 57 supeq1d x = S j sup i 0 ..^ M | Q i L E x < = sup i 0 ..^ M | Q i L E S j <
59 58 adantl φ j 0 ..^ N x = S j sup i 0 ..^ M | Q i L E x < = sup i 0 ..^ M | Q i L E S j <
60 ltso < Or
61 60 supex sup i 0 ..^ M | Q i L E S j < V
62 61 a1i φ j 0 ..^ N sup i 0 ..^ M | Q i L E S j < V
63 53 59 43 62 fvmptd φ j 0 ..^ N I S j = sup i 0 ..^ M | Q i L E S j <
64 63 fveq2d φ j 0 ..^ N Q I S j = Q sup i 0 ..^ M | Q i L E S j <
65 simpl φ j 0 ..^ N φ
66 65 43 jca φ j 0 ..^ N φ S j
67 eleq1 x = S j x S j
68 67 anbi2d x = S j φ x φ S j
69 58 57 eleq12d x = S j sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x sup i 0 ..^ M | Q i L E S j < i 0 ..^ M | Q i L E S j
70 68 69 imbi12d x = S j φ x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x φ S j sup i 0 ..^ M | Q i L E S j < i 0 ..^ M | Q i L E S j
71 23 simprd φ x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
72 71 imp φ x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
73 70 72 vtoclg S j φ S j sup i 0 ..^ M | Q i L E S j < i 0 ..^ M | Q i L E S j
74 43 66 73 sylc φ j 0 ..^ N sup i 0 ..^ M | Q i L E S j < i 0 ..^ M | Q i L E S j
75 nfrab1 _ i i 0 ..^ M | Q i L E S j
76 nfcv _ i
77 nfcv _ i <
78 75 76 77 nfsup _ i sup i 0 ..^ M | Q i L E S j <
79 nfcv _ i 0 ..^ M
80 nfcv _ i Q
81 80 78 nffv _ i Q sup i 0 ..^ M | Q i L E S j <
82 nfcv _ i
83 nfcv _ i L E S j
84 81 82 83 nfbr i Q sup i 0 ..^ M | Q i L E S j < L E S j
85 fveq2 i = sup i 0 ..^ M | Q i L E S j < Q i = Q sup i 0 ..^ M | Q i L E S j <
86 85 breq1d i = sup i 0 ..^ M | Q i L E S j < Q i L E S j Q sup i 0 ..^ M | Q i L E S j < L E S j
87 78 79 84 86 elrabf sup i 0 ..^ M | Q i L E S j < i 0 ..^ M | Q i L E S j sup i 0 ..^ M | Q i L E S j < 0 ..^ M Q sup i 0 ..^ M | Q i L E S j < L E S j
88 74 87 sylib φ j 0 ..^ N sup i 0 ..^ M | Q i L E S j < 0 ..^ M Q sup i 0 ..^ M | Q i L E S j < L E S j
89 88 simprd φ j 0 ..^ N Q sup i 0 ..^ M | Q i L E S j < L E S j
90 64 89 eqbrtrd φ j 0 ..^ N Q I S j L E S j
91 3 ad2antrr φ j 0 ..^ N E S j = B M
92 4 ad2antrr φ j 0 ..^ N E S j = B Q P M
93 5 ad2antrr φ j 0 ..^ N E S j = B C
94 6 ad2antrr φ j 0 ..^ N E S j = B D
95 7 ad2antrr φ j 0 ..^ N E S j = B C < D
96 0zd φ 0
97 3 nnzd φ M
98 1zzd φ 1
99 0le1 0 1
100 99 a1i φ 0 1
101 3 nnge1d φ 1 M
102 96 97 98 100 101 elfzd φ 1 0 M
103 102 ad2antrr φ j 0 ..^ N E S j = B 1 0 M
104 simplr φ j 0 ..^ N E S j = B j 0 ..^ N
105 fzofzp1 j 0 ..^ N j + 1 0 N
106 105 adantl φ j 0 ..^ N j + 1 0 N
107 40 106 ffvelrnd φ j 0 ..^ N S j + 1
108 107 43 resubcld φ j 0 ..^ N S j + 1 S j
109 108 rehalfcld φ j 0 ..^ N S j + 1 S j 2
110 21 102 ffvelrnd φ Q 1
111 2 3 4 fourierdlem11 φ A B A < B
112 111 simp1d φ A
113 110 112 resubcld φ Q 1 A
114 113 rehalfcld φ Q 1 A 2
115 114 adantr φ j 0 ..^ N Q 1 A 2
116 109 115 ifcld φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
117 43 116 readdcld φ j 0 ..^ N S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
118 14 117 eqeltrid φ j 0 ..^ N Z
119 2re 2
120 119 a1i φ j 0 ..^ N 2
121 elfzoelz j 0 ..^ N j
122 121 zred j 0 ..^ N j
123 122 ltp1d j 0 ..^ N j < j + 1
124 123 adantl φ j 0 ..^ N j < j + 1
125 29 simprd φ S Isom < , < 0 N H
126 125 adantr φ j 0 ..^ N S Isom < , < 0 N H
127 isorel S Isom < , < 0 N H j 0 N j + 1 0 N j < j + 1 S j < S j + 1
128 126 42 106 127 syl12anc φ j 0 ..^ N j < j + 1 S j < S j + 1
129 124 128 mpbid φ j 0 ..^ N S j < S j + 1
130 43 107 posdifd φ j 0 ..^ N S j < S j + 1 0 < S j + 1 S j
131 129 130 mpbid φ j 0 ..^ N 0 < S j + 1 S j
132 2pos 0 < 2
133 132 a1i φ j 0 ..^ N 0 < 2
134 108 120 131 133 divgt0d φ j 0 ..^ N 0 < S j + 1 S j 2
135 109 134 elrpd φ j 0 ..^ N S j + 1 S j 2 +
136 119 a1i φ 2
137 3 nngt0d φ 0 < M
138 fzolb 0 0 ..^ M 0 M 0 < M
139 96 97 137 138 syl3anbrc φ 0 0 ..^ M
140 0re 0
141 eleq1 i = 0 i 0 ..^ M 0 0 ..^ M
142 141 anbi2d i = 0 φ i 0 ..^ M φ 0 0 ..^ M
143 fveq2 i = 0 Q i = Q 0
144 oveq1 i = 0 i + 1 = 0 + 1
145 144 fveq2d i = 0 Q i + 1 = Q 0 + 1
146 143 145 breq12d i = 0 Q i < Q i + 1 Q 0 < Q 0 + 1
147 142 146 imbi12d i = 0 φ i 0 ..^ M Q i < Q i + 1 φ 0 0 ..^ M Q 0 < Q 0 + 1
148 18 simprd φ Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
149 148 simprd φ i 0 ..^ M Q i < Q i + 1
150 149 r19.21bi φ i 0 ..^ M Q i < Q i + 1
151 147 150 vtoclg 0 φ 0 0 ..^ M Q 0 < Q 0 + 1
152 140 151 ax-mp φ 0 0 ..^ M Q 0 < Q 0 + 1
153 139 152 mpdan φ Q 0 < Q 0 + 1
154 148 simpld φ Q 0 = A Q M = B
155 154 simpld φ Q 0 = A
156 0p1e1 0 + 1 = 1
157 156 fveq2i Q 0 + 1 = Q 1
158 157 a1i φ Q 0 + 1 = Q 1
159 153 155 158 3brtr3d φ A < Q 1
160 112 110 posdifd φ A < Q 1 0 < Q 1 A
161 159 160 mpbid φ 0 < Q 1 A
162 132 a1i φ 0 < 2
163 113 136 161 162 divgt0d φ 0 < Q 1 A 2
164 114 163 elrpd φ Q 1 A 2 +
165 164 adantr φ j 0 ..^ N Q 1 A 2 +
166 135 165 ifcld φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 +
167 43 166 ltaddrpd φ j 0 ..^ N S j < S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
168 43 117 167 ltled φ j 0 ..^ N S j S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
169 168 14 breqtrrdi φ j 0 ..^ N S j Z
170 43 109 readdcld φ j 0 ..^ N S j + S j + 1 S j 2
171 iftrue S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = S j + 1 S j 2
172 171 adantl φ j 0 ..^ N S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = S j + 1 S j 2
173 109 leidd φ j 0 ..^ N S j + 1 S j 2 S j + 1 S j 2
174 173 adantr φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j 2 S j + 1 S j 2
175 172 174 eqbrtrd φ j 0 ..^ N S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 S j + 1 S j 2
176 iffalse ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = Q 1 A 2
177 176 adantl φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = Q 1 A 2
178 113 ad2antrr φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A Q 1 A
179 108 adantr φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A S j + 1 S j
180 2rp 2 +
181 180 a1i φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A 2 +
182 simpr φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A ¬ S j + 1 S j < Q 1 A
183 178 179 182 nltled φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A Q 1 A S j + 1 S j
184 178 179 181 183 lediv1dd φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A Q 1 A 2 S j + 1 S j 2
185 177 184 eqbrtrd φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 S j + 1 S j 2
186 175 185 pm2.61dan φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 S j + 1 S j 2
187 116 109 43 186 leadd2dd φ j 0 ..^ N S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 S j + S j + 1 S j 2
188 43 recnd φ j 0 ..^ N S j
189 107 recnd φ j 0 ..^ N S j + 1
190 188 189 addcomd φ j 0 ..^ N S j + S j + 1 = S j + 1 + S j
191 190 oveq1d φ j 0 ..^ N S j + S j + 1 2 = S j + 1 + S j 2
192 191 oveq1d φ j 0 ..^ N S j + S j + 1 2 S j + 1 S j 2 = S j + 1 + S j 2 S j + 1 S j 2
193 halfaddsub S j + 1 S j S j + 1 + S j 2 + S j + 1 S j 2 = S j + 1 S j + 1 + S j 2 S j + 1 S j 2 = S j
194 189 188 193 syl2anc φ j 0 ..^ N S j + 1 + S j 2 + S j + 1 S j 2 = S j + 1 S j + 1 + S j 2 S j + 1 S j 2 = S j
195 194 simprd φ j 0 ..^ N S j + 1 + S j 2 S j + 1 S j 2 = S j
196 192 195 eqtrd φ j 0 ..^ N S j + S j + 1 2 S j + 1 S j 2 = S j
197 188 189 addcld φ j 0 ..^ N S j + S j + 1
198 197 halfcld φ j 0 ..^ N S j + S j + 1 2
199 109 recnd φ j 0 ..^ N S j + 1 S j 2
200 198 199 188 subsub23d φ j 0 ..^ N S j + S j + 1 2 S j + 1 S j 2 = S j S j + S j + 1 2 S j = S j + 1 S j 2
201 196 200 mpbid φ j 0 ..^ N S j + S j + 1 2 S j = S j + 1 S j 2
202 198 188 199 subaddd φ j 0 ..^ N S j + S j + 1 2 S j = S j + 1 S j 2 S j + S j + 1 S j 2 = S j + S j + 1 2
203 201 202 mpbid φ j 0 ..^ N S j + S j + 1 S j 2 = S j + S j + 1 2
204 avglt2 S j S j + 1 S j < S j + 1 S j + S j + 1 2 < S j + 1
205 43 107 204 syl2anc φ j 0 ..^ N S j < S j + 1 S j + S j + 1 2 < S j + 1
206 129 205 mpbid φ j 0 ..^ N S j + S j + 1 2 < S j + 1
207 203 206 eqbrtrd φ j 0 ..^ N S j + S j + 1 S j 2 < S j + 1
208 117 170 107 187 207 lelttrd φ j 0 ..^ N S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 < S j + 1
209 14 208 eqbrtrid φ j 0 ..^ N Z < S j + 1
210 107 rexrd φ j 0 ..^ N S j + 1 *
211 elico2 S j S j + 1 * Z S j S j + 1 Z S j Z Z < S j + 1
212 43 210 211 syl2anc φ j 0 ..^ N Z S j S j + 1 Z S j Z Z < S j + 1
213 118 169 209 212 mpbir3and φ j 0 ..^ N Z S j S j + 1
214 213 adantr φ j 0 ..^ N E S j = B Z S j S j + 1
215 112 ad2antrr φ j 0 ..^ N E S j = B A
216 111 simp2d φ B
217 216 ad2antrr φ j 0 ..^ N E S j = B B
218 111 simp3d φ A < B
219 218 ad2antrr φ j 0 ..^ N E S j = B A < B
220 43 adantr φ j 0 ..^ N E S j = B S j
221 simpr φ j 0 ..^ N E S j = B E S j = B
222 167 14 breqtrrdi φ j 0 ..^ N S j < Z
223 216 112 resubcld φ B A
224 1 223 eqeltrid φ T
225 224 adantr φ j 0 ..^ N T
226 109 adantr φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j 2
227 114 ad2antrr φ j 0 ..^ N S j + 1 S j < Q 1 A Q 1 A 2
228 108 adantr φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j
229 113 ad2antrr φ j 0 ..^ N S j + 1 S j < Q 1 A Q 1 A
230 180 a1i φ j 0 ..^ N S j + 1 S j < Q 1 A 2 +
231 simpr φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j < Q 1 A
232 228 229 230 231 ltdiv1dd φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j 2 < Q 1 A 2
233 226 227 232 ltled φ j 0 ..^ N S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
234 172 233 eqbrtrd φ j 0 ..^ N S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 Q 1 A 2
235 176 adantl φ ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = Q 1 A 2
236 114 leidd φ Q 1 A 2 Q 1 A 2
237 236 adantr φ ¬ S j + 1 S j < Q 1 A Q 1 A 2 Q 1 A 2
238 235 237 eqbrtrd φ ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 Q 1 A 2
239 238 adantlr φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 Q 1 A 2
240 234 239 pm2.61dan φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 Q 1 A 2
241 223 rehalfcld φ B A 2
242 180 a1i φ 2 +
243 112 rexrd φ A *
244 216 rexrd φ B *
245 2 3 4 fourierdlem15 φ Q : 0 M A B
246 245 102 ffvelrnd φ Q 1 A B
247 iccleub A * B * Q 1 A B Q 1 B
248 243 244 246 247 syl3anc φ Q 1 B
249 110 216 112 248 lesub1dd φ Q 1 A B A
250 113 223 242 249 lediv1dd φ Q 1 A 2 B A 2
251 1 eqcomi B A = T
252 251 oveq1i B A 2 = T 2
253 112 216 posdifd φ A < B 0 < B A
254 218 253 mpbid φ 0 < B A
255 254 1 breqtrrdi φ 0 < T
256 224 255 elrpd φ T +
257 rphalflt T + T 2 < T
258 256 257 syl φ T 2 < T
259 252 258 eqbrtrid φ B A 2 < T
260 114 241 224 250 259 lelttrd φ Q 1 A 2 < T
261 114 224 260 ltled φ Q 1 A 2 T
262 261 adantr φ j 0 ..^ N Q 1 A 2 T
263 116 115 225 240 262 letrd φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 T
264 116 225 43 263 leadd2dd φ j 0 ..^ N S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 S j + T
265 14 264 eqbrtrid φ j 0 ..^ N Z S j + T
266 43 rexrd φ j 0 ..^ N S j *
267 43 225 readdcld φ j 0 ..^ N S j + T
268 elioc2 S j * S j + T Z S j S j + T Z S j < Z Z S j + T
269 266 267 268 syl2anc φ j 0 ..^ N Z S j S j + T Z S j < Z Z S j + T
270 118 222 265 269 mpbir3and φ j 0 ..^ N Z S j S j + T
271 270 adantr φ j 0 ..^ N E S j = B Z S j S j + T
272 215 217 219 1 12 220 221 271 fourierdlem26 φ j 0 ..^ N E S j = B E Z = A + Z - S j
273 14 a1i φ j 0 ..^ N Z = S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
274 273 oveq1d φ j 0 ..^ N Z S j = S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j
275 274 oveq2d φ j 0 ..^ N A + Z - S j = A + S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j
276 275 adantr φ j 0 ..^ N E S j = B A + Z - S j = A + S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j
277 116 recnd φ j 0 ..^ N if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
278 188 277 pncan2d φ j 0 ..^ N S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j = if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
279 278 oveq2d φ j 0 ..^ N A + S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j = A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
280 279 adantr φ j 0 ..^ N E S j = B A + S j + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 - S j = A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
281 272 276 280 3eqtrd φ j 0 ..^ N E S j = B E Z = A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2
282 171 oveq2d S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = A + S j + 1 S j 2
283 282 adantl φ j 0 ..^ N S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = A + S j + 1 S j 2
284 112 adantr φ j 0 ..^ N A
285 284 109 readdcld φ j 0 ..^ N A + S j + 1 S j 2
286 285 adantr φ j 0 ..^ N S j + 1 S j < Q 1 A A + S j + 1 S j 2
287 284 115 readdcld φ j 0 ..^ N A + Q 1 A 2
288 287 adantr φ j 0 ..^ N S j + 1 S j < Q 1 A A + Q 1 A 2
289 110 ad2antrr φ j 0 ..^ N S j + 1 S j < Q 1 A Q 1
290 112 ad2antrr φ j 0 ..^ N S j + 1 S j < Q 1 A A
291 226 227 290 232 ltadd2dd φ j 0 ..^ N S j + 1 S j < Q 1 A A + S j + 1 S j 2 < A + Q 1 A 2
292 110 recnd φ Q 1
293 112 recnd φ A
294 halfaddsub Q 1 A Q 1 + A 2 + Q 1 A 2 = Q 1 Q 1 + A 2 Q 1 A 2 = A
295 292 293 294 syl2anc φ Q 1 + A 2 + Q 1 A 2 = Q 1 Q 1 + A 2 Q 1 A 2 = A
296 295 simprd φ Q 1 + A 2 Q 1 A 2 = A
297 296 oveq1d φ Q 1 + A 2 - Q 1 A 2 + Q 1 A 2 = A + Q 1 A 2
298 110 112 readdcld φ Q 1 + A
299 298 rehalfcld φ Q 1 + A 2
300 299 recnd φ Q 1 + A 2
301 114 recnd φ Q 1 A 2
302 300 301 npcand φ Q 1 + A 2 - Q 1 A 2 + Q 1 A 2 = Q 1 + A 2
303 297 302 eqtr3d φ A + Q 1 A 2 = Q 1 + A 2
304 110 110 readdcld φ Q 1 + Q 1
305 112 110 110 159 ltadd2dd φ Q 1 + A < Q 1 + Q 1
306 298 304 242 305 ltdiv1dd φ Q 1 + A 2 < Q 1 + Q 1 2
307 292 2timesd φ 2 Q 1 = Q 1 + Q 1
308 307 eqcomd φ Q 1 + Q 1 = 2 Q 1
309 308 oveq1d φ Q 1 + Q 1 2 = 2 Q 1 2
310 2cnd φ 2
311 2ne0 2 0
312 311 a1i φ 2 0
313 292 310 312 divcan3d φ 2 Q 1 2 = Q 1
314 309 313 eqtrd φ Q 1 + Q 1 2 = Q 1
315 306 314 breqtrd φ Q 1 + A 2 < Q 1
316 303 315 eqbrtrd φ A + Q 1 A 2 < Q 1
317 316 ad2antrr φ j 0 ..^ N S j + 1 S j < Q 1 A A + Q 1 A 2 < Q 1
318 286 288 289 291 317 lttrd φ j 0 ..^ N S j + 1 S j < Q 1 A A + S j + 1 S j 2 < Q 1
319 283 318 eqbrtrd φ j 0 ..^ N S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 < Q 1
320 176 oveq2d ¬ S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = A + Q 1 A 2
321 320 adantl φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 = A + Q 1 A 2
322 316 ad2antrr φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A A + Q 1 A 2 < Q 1
323 321 322 eqbrtrd φ j 0 ..^ N ¬ S j + 1 S j < Q 1 A A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 < Q 1
324 319 323 pm2.61dan φ j 0 ..^ N A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 < Q 1
325 324 adantr φ j 0 ..^ N E S j = B A + if S j + 1 S j < Q 1 A S j + 1 S j 2 Q 1 A 2 < Q 1
326 281 325 eqbrtrd φ j 0 ..^ N E S j = B E Z < Q 1
327 eqid Q 1 E Z Z = Q 1 E Z Z
328 1 2 91 92 93 94 95 8 9 10 11 12 103 104 214 326 327 fourierdlem63 φ j 0 ..^ N E S j = B E S j + 1 Q 1
329 15 a1i φ j 0 ..^ N E S j = B I = x sup i 0 ..^ M | Q i L E x <
330 58 adantl φ j 0 ..^ N E S j = B x = S j sup i 0 ..^ M | Q i L E x < = sup i 0 ..^ M | Q i L E S j <
331 61 a1i φ j 0 ..^ N E S j = B sup i 0 ..^ M | Q i L E S j < V
332 329 330 220 331 fvmptd φ j 0 ..^ N E S j = B I S j = sup i 0 ..^ M | Q i L E S j <
333 fveq2 E S j = B L E S j = L B
334 13 a1i φ L = y A B if y = B A y
335 iftrue y = B if y = B A y = A
336 335 adantl φ y = B if y = B A y = A
337 ubioc1 A * B * A < B B A B
338 243 244 218 337 syl3anc φ B A B
339 334 336 338 112 fvmptd φ L B = A
340 333 339 sylan9eqr φ E S j = B L E S j = A
341 340 breq2d φ E S j = B Q i L E S j Q i A
342 341 rabbidv φ E S j = B i 0 ..^ M | Q i L E S j = i 0 ..^ M | Q i A
343 342 supeq1d φ E S j = B sup i 0 ..^ M | Q i L E S j < = sup i 0 ..^ M | Q i A <
344 343 adantlr φ j 0 ..^ N E S j = B sup i 0 ..^ M | Q i L E S j < = sup i 0 ..^ M | Q i A <
345 simpl φ j i 0 ..^ M | Q i A φ
346 elrabi j i 0 ..^ M | Q i A j 0 ..^ M
347 346 adantl φ j i 0 ..^ M | Q i A j 0 ..^ M
348 fveq2 i = j Q i = Q j
349 348 breq1d i = j Q i A Q j A
350 349 elrab j i 0 ..^ M | Q i A j 0 ..^ M Q j A
351 350 simprbi j i 0 ..^ M | Q i A Q j A
352 351 adantl φ j i 0 ..^ M | Q i A Q j A
353 simp3 φ j 0 ..^ M Q j A Q j A
354 112 ad2antrr φ j 0 ..^ M ¬ j 0 A
355 110 ad2antrr φ j 0 ..^ M ¬ j 0 Q 1
356 21 adantr φ j 0 ..^ M Q : 0 M
357 26 sselda φ j 0 ..^ M j 0 M
358 356 357 ffvelrnd φ j 0 ..^ M Q j
359 358 adantr φ j 0 ..^ M ¬ j 0 Q j
360 159 ad2antrr φ j 0 ..^ M ¬ j 0 A < Q 1
361 1zzd φ j 0 ..^ M ¬ j 0 1
362 elfzoelz j 0 ..^ M j
363 362 ad2antlr φ j 0 ..^ M ¬ j 0 j
364 1e0p1 1 = 0 + 1
365 simpr φ j 0 ..^ M ¬ j 0 ¬ j 0
366 0red φ j 0 ..^ M ¬ j 0 0
367 363 zred φ j 0 ..^ M ¬ j 0 j
368 366 367 ltnled φ j 0 ..^ M ¬ j 0 0 < j ¬ j 0
369 365 368 mpbird φ j 0 ..^ M ¬ j 0 0 < j
370 0zd φ j 0 ..^ M ¬ j 0 0
371 zltp1le 0 j 0 < j 0 + 1 j
372 370 363 371 syl2anc φ j 0 ..^ M ¬ j 0 0 < j 0 + 1 j
373 369 372 mpbid φ j 0 ..^ M ¬ j 0 0 + 1 j
374 364 373 eqbrtrid φ j 0 ..^ M ¬ j 0 1 j
375 eluz2 j 1 1 j 1 j
376 361 363 374 375 syl3anbrc φ j 0 ..^ M ¬ j 0 j 1
377 21 ad2antrr φ j 0 ..^ M l 1 j Q : 0 M
378 0zd φ j 0 ..^ M l 1 j 0
379 97 ad2antrr φ j 0 ..^ M l 1 j M
380 elfzelz l 1 j l
381 380 adantl φ j 0 ..^ M l 1 j l
382 0red l 1 j 0
383 380 zred l 1 j l
384 1red l 1 j 1
385 0lt1 0 < 1
386 385 a1i l 1 j 0 < 1
387 elfzle1 l 1 j 1 l
388 382 384 383 386 387 ltletrd l 1 j 0 < l
389 382 383 388 ltled l 1 j 0 l
390 389 adantl φ j 0 ..^ M l 1 j 0 l
391 383 adantl φ j 0 ..^ M l 1 j l
392 97 zred φ M
393 392 ad2antrr φ j 0 ..^ M l 1 j M
394 362 zred j 0 ..^ M j
395 394 ad2antlr φ j 0 ..^ M l 1 j j
396 elfzle2 l 1 j l j
397 396 adantl φ j 0 ..^ M l 1 j l j
398 elfzolt2 j 0 ..^ M j < M
399 398 ad2antlr φ j 0 ..^ M l 1 j j < M
400 391 395 393 397 399 lelttrd φ j 0 ..^ M l 1 j l < M
401 391 393 400 ltled φ j 0 ..^ M l 1 j l M
402 378 379 381 390 401 elfzd φ j 0 ..^ M l 1 j l 0 M
403 377 402 ffvelrnd φ j 0 ..^ M l 1 j Q l
404 403 adantlr φ j 0 ..^ M ¬ j 0 l 1 j Q l
405 21 ad2antrr φ j 0 ..^ M l 1 j 1 Q : 0 M
406 0zd φ j 0 ..^ M l 1 j 1 0
407 97 ad2antrr φ j 0 ..^ M l 1 j 1 M
408 elfzelz l 1 j 1 l
409 408 adantl φ j 0 ..^ M l 1 j 1 l
410 0red l 1 j 1 0
411 408 zred l 1 j 1 l
412 1red l 1 j 1 1
413 385 a1i l 1 j 1 0 < 1
414 elfzle1 l 1 j 1 1 l
415 410 412 411 413 414 ltletrd l 1 j 1 0 < l
416 410 411 415 ltled l 1 j 1 0 l
417 416 adantl φ j 0 ..^ M l 1 j 1 0 l
418 409 zred φ j 0 ..^ M l 1 j 1 l
419 392 ad2antrr φ j 0 ..^ M l 1 j 1 M
420 394 ad2antlr φ j 0 ..^ M l 1 j 1 j
421 411 adantl j 0 ..^ M l 1 j 1 l
422 peano2rem j j 1
423 394 422 syl j 0 ..^ M j 1
424 423 adantr j 0 ..^ M l 1 j 1 j 1
425 394 adantr j 0 ..^ M l 1 j 1 j
426 elfzle2 l 1 j 1 l j 1
427 426 adantl j 0 ..^ M l 1 j 1 l j 1
428 425 ltm1d j 0 ..^ M l 1 j 1 j 1 < j
429 421 424 425 427 428 lelttrd j 0 ..^ M l 1 j 1 l < j
430 429 adantll φ j 0 ..^ M l 1 j 1 l < j
431 398 ad2antlr φ j 0 ..^ M l 1 j 1 j < M
432 418 420 419 430 431 lttrd φ j 0 ..^ M l 1 j 1 l < M
433 418 419 432 ltled φ j 0 ..^ M l 1 j 1 l M
434 406 407 409 417 433 elfzd φ j 0 ..^ M l 1 j 1 l 0 M
435 405 434 ffvelrnd φ j 0 ..^ M l 1 j 1 Q l
436 409 peano2zd φ j 0 ..^ M l 1 j 1 l + 1
437 411 412 readdcld l 1 j 1 l + 1
438 411 412 415 413 addgt0d l 1 j 1 0 < l + 1
439 410 437 438 ltled l 1 j 1 0 l + 1
440 439 adantl φ j 0 ..^ M l 1 j 1 0 l + 1
441 437 adantl φ j 0 ..^ M l 1 j 1 l + 1
442 437 recnd l 1 j 1 l + 1
443 1cnd l 1 j 1 1
444 442 443 npcand l 1 j 1 l + 1 - 1 + 1 = l + 1
445 444 eqcomd l 1 j 1 l + 1 = l + 1 - 1 + 1
446 445 adantl j 0 ..^ M l 1 j 1 l + 1 = l + 1 - 1 + 1
447 peano2re l l + 1
448 peano2rem l + 1 l + 1 - 1
449 421 447 448 3syl j 0 ..^ M l 1 j 1 l + 1 - 1
450 peano2re j 1 j - 1 + 1
451 peano2rem j - 1 + 1 j 1 + 1 - 1
452 424 450 451 3syl j 0 ..^ M l 1 j 1 j 1 + 1 - 1
453 1red j 0 ..^ M l 1 j 1 1
454 elfzel2 l 1 j 1 j 1
455 454 zred l 1 j 1 j 1
456 455 412 readdcld l 1 j 1 j - 1 + 1
457 411 455 412 426 leadd1dd l 1 j 1 l + 1 j - 1 + 1
458 437 456 412 457 lesub1dd l 1 j 1 l + 1 - 1 j 1 + 1 - 1
459 458 adantl j 0 ..^ M l 1 j 1 l + 1 - 1 j 1 + 1 - 1
460 449 452 453 459 leadd1dd j 0 ..^ M l 1 j 1 l + 1 - 1 + 1 j - 1 + 1 - 1 + 1
461 peano2zm j j 1
462 362 461 syl j 0 ..^ M j 1
463 462 peano2zd j 0 ..^ M j - 1 + 1
464 463 zcnd j 0 ..^ M j - 1 + 1
465 1cnd j 0 ..^ M 1
466 464 465 npcand j 0 ..^ M j - 1 + 1 - 1 + 1 = j - 1 + 1
467 394 recnd j 0 ..^ M j
468 467 465 npcand j 0 ..^ M j - 1 + 1 = j
469 466 468 eqtrd j 0 ..^ M j - 1 + 1 - 1 + 1 = j
470 469 adantr j 0 ..^ M l 1 j 1 j - 1 + 1 - 1 + 1 = j
471 460 470 breqtrd j 0 ..^ M l 1 j 1 l + 1 - 1 + 1 j
472 446 471 eqbrtrd j 0 ..^ M l 1 j 1 l + 1 j
473 472 adantll φ j 0 ..^ M l 1 j 1 l + 1 j
474 441 420 419 473 431 lelttrd φ j 0 ..^ M l 1 j 1 l + 1 < M
475 441 419 474 ltled φ j 0 ..^ M l 1 j 1 l + 1 M
476 406 407 436 440 475 elfzd φ j 0 ..^ M l 1 j 1 l + 1 0 M
477 405 476 ffvelrnd φ j 0 ..^ M l 1 j 1 Q l + 1
478 simpll φ j 0 ..^ M l 1 j 1 φ
479 0zd j 0 ..^ M l 1 j 1 0
480 408 adantl j 0 ..^ M l 1 j 1 l
481 416 adantl j 0 ..^ M l 1 j 1 0 l
482 eluz2 l 0 0 l 0 l
483 479 480 481 482 syl3anbrc j 0 ..^ M l 1 j 1 l 0
484 elfzoel2 j 0 ..^ M M
485 484 adantr j 0 ..^ M l 1 j 1 M
486 485 zred j 0 ..^ M l 1 j 1 M
487 398 adantr j 0 ..^ M l 1 j 1 j < M
488 421 425 486 429 487 lttrd j 0 ..^ M l 1 j 1 l < M
489 elfzo2 l 0 ..^ M l 0 M l < M
490 483 485 488 489 syl3anbrc j 0 ..^ M l 1 j 1 l 0 ..^ M
491 490 adantll φ j 0 ..^ M l 1 j 1 l 0 ..^ M
492 eleq1 i = l i 0 ..^ M l 0 ..^ M
493 492 anbi2d i = l φ i 0 ..^ M φ l 0 ..^ M
494 fveq2 i = l Q i = Q l
495 oveq1 i = l i + 1 = l + 1
496 495 fveq2d i = l Q i + 1 = Q l + 1
497 494 496 breq12d i = l Q i < Q i + 1 Q l < Q l + 1
498 493 497 imbi12d i = l φ i 0 ..^ M Q i < Q i + 1 φ l 0 ..^ M Q l < Q l + 1
499 498 150 chvarvv φ l 0 ..^ M Q l < Q l + 1
500 478 491 499 syl2anc φ j 0 ..^ M l 1 j 1 Q l < Q l + 1
501 435 477 500 ltled φ j 0 ..^ M l 1 j 1 Q l Q l + 1
502 501 adantlr φ j 0 ..^ M ¬ j 0 l 1 j 1 Q l Q l + 1
503 376 404 502 monoord φ j 0 ..^ M ¬ j 0 Q 1 Q j
504 354 355 359 360 503 ltletrd φ j 0 ..^ M ¬ j 0 A < Q j
505 354 359 ltnled φ j 0 ..^ M ¬ j 0 A < Q j ¬ Q j A
506 504 505 mpbid φ j 0 ..^ M ¬ j 0 ¬ Q j A
507 506 ex φ j 0 ..^ M ¬ j 0 ¬ Q j A
508 507 3adant3 φ j 0 ..^ M Q j A ¬ j 0 ¬ Q j A
509 353 508 mt4d φ j 0 ..^ M Q j A j 0
510 elfzole1 j 0 ..^ M 0 j
511 510 3ad2ant2 φ j 0 ..^ M Q j A 0 j
512 394 3ad2ant2 φ j 0 ..^ M Q j A j
513 0red φ j 0 ..^ M Q j A 0
514 512 513 letri3d φ j 0 ..^ M Q j A j = 0 j 0 0 j
515 509 511 514 mpbir2and φ j 0 ..^ M Q j A j = 0
516 345 347 352 515 syl3anc φ j i 0 ..^ M | Q i A j = 0
517 velsn j 0 j = 0
518 516 517 sylibr φ j i 0 ..^ M | Q i A j 0
519 518 ralrimiva φ j i 0 ..^ M | Q i A j 0
520 dfss3 i 0 ..^ M | Q i A 0 j i 0 ..^ M | Q i A j 0
521 519 520 sylibr φ i 0 ..^ M | Q i A 0
522 155 112 eqeltrd φ Q 0
523 522 155 eqled φ Q 0 A
524 143 breq1d i = 0 Q i A Q 0 A
525 524 elrab 0 i 0 ..^ M | Q i A 0 0 ..^ M Q 0 A
526 139 523 525 sylanbrc φ 0 i 0 ..^ M | Q i A
527 526 snssd φ 0 i 0 ..^ M | Q i A
528 521 527 eqssd φ i 0 ..^ M | Q i A = 0
529 528 supeq1d φ sup i 0 ..^ M | Q i A < = sup 0 <
530 supsn < Or 0 sup 0 < = 0
531 60 140 530 mp2an sup 0 < = 0
532 531 a1i φ sup 0 < = 0
533 529 532 eqtrd φ sup i 0 ..^ M | Q i A < = 0
534 533 ad2antrr φ j 0 ..^ N E S j = B sup i 0 ..^ M | Q i A < = 0
535 332 344 534 3eqtrd φ j 0 ..^ N E S j = B I S j = 0
536 535 oveq1d φ j 0 ..^ N E S j = B I S j + 1 = 0 + 1
537 536 fveq2d φ j 0 ..^ N E S j = B Q I S j + 1 = Q 0 + 1
538 537 157 eqtr2di φ j 0 ..^ N E S j = B Q 1 = Q I S j + 1
539 328 538 breqtrd φ j 0 ..^ N E S j = B E S j + 1 Q I S j + 1
540 66 adantr φ j 0 ..^ N ¬ E S j = B φ S j
541 simplr φ j 0 ..^ N ¬ E S j = B j 0 ..^ N
542 13 a1i φ j 0 ..^ N ¬ E S j = B L = y A B if y = B A y
543 simpr ¬ E S j = B y = E S j y = E S j
544 neqne ¬ E S j = B E S j B
545 544 adantr ¬ E S j = B y = E S j E S j B
546 543 545 eqnetrd ¬ E S j = B y = E S j y B
547 546 neneqd ¬ E S j = B y = E S j ¬ y = B
548 547 iffalsed ¬ E S j = B y = E S j if y = B A y = y
549 548 543 eqtrd ¬ E S j = B y = E S j if y = B A y = E S j
550 549 adantll φ j 0 ..^ N ¬ E S j = B y = E S j if y = B A y = E S j
551 112 216 218 1 12 fourierdlem4 φ E : A B
552 551 adantr φ j 0 ..^ N E : A B
553 552 43 ffvelrnd φ j 0 ..^ N E S j A B
554 553 adantr φ j 0 ..^ N ¬ E S j = B E S j A B
555 542 550 554 554 fvmptd φ j 0 ..^ N ¬ E S j = B L E S j = E S j
556 555 eqcomd φ j 0 ..^ N ¬ E S j = B E S j = L E S j
557 112 216 218 13 fourierdlem17 φ L : A B A B
558 557 adantr φ j 0 ..^ N L : A B A B
559 112 216 iccssred φ A B
560 559 adantr φ j 0 ..^ N A B
561 558 560 fssd φ j 0 ..^ N L : A B
562 561 553 ffvelrnd φ j 0 ..^ N L E S j
563 562 adantr φ j 0 ..^ N ¬ E S j = B L E S j
564 556 563 eqeltrd φ j 0 ..^ N ¬ E S j = B E S j
565 216 ad2antrr φ j 0 ..^ N ¬ E S j = B B
566 243 adantr φ j 0 ..^ N A *
567 216 adantr φ j 0 ..^ N B
568 elioc2 A * B E S j A B E S j A < E S j E S j B
569 566 567 568 syl2anc φ j 0 ..^ N E S j A B E S j A < E S j E S j B
570 553 569 mpbid φ j 0 ..^ N E S j A < E S j E S j B
571 570 simp3d φ j 0 ..^ N E S j B
572 571 adantr φ j 0 ..^ N ¬ E S j = B E S j B
573 544 necomd ¬ E S j = B B E S j
574 573 adantl φ j 0 ..^ N ¬ E S j = B B E S j
575 564 565 572 574 leneltd φ j 0 ..^ N ¬ E S j = B E S j < B
576 575 adantr φ j 0 ..^ N ¬ E S j = B I S j = M 1 E S j < B
577 oveq1 I S j = M 1 I S j + 1 = M - 1 + 1
578 3 nncnd φ M
579 1cnd φ 1
580 578 579 npcand φ M - 1 + 1 = M
581 577 580 sylan9eqr φ I S j = M 1 I S j + 1 = M
582 581 fveq2d φ I S j = M 1 Q I S j + 1 = Q M
583 154 simprd φ Q M = B
584 583 adantr φ I S j = M 1 Q M = B
585 582 584 eqtr2d φ I S j = M 1 B = Q I S j + 1
586 585 adantlr φ j 0 ..^ N I S j = M 1 B = Q I S j + 1
587 586 adantlr φ j 0 ..^ N ¬ E S j = B I S j = M 1 B = Q I S j + 1
588 576 587 breqtrd φ j 0 ..^ N ¬ E S j = B I S j = M 1 E S j < Q I S j + 1
589 556 adantr φ j 0 ..^ N ¬ E S j = B ¬ I S j = M 1 E S j = L E S j
590 ssrab2 i 0 ..^ M | Q i L E S j 0 ..^ M
591 fzssz 0 M
592 25 591 sstri 0 ..^ M
593 zssre
594 592 593 sstri 0 ..^ M
595 590 594 sstri i 0 ..^ M | Q i L E S j
596 595 a1i φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j i 0 ..^ M | Q i L E S j
597 57 neeq1d x = S j i 0 ..^ M | Q i L E x i 0 ..^ M | Q i L E S j
598 68 597 imbi12d x = S j φ x i 0 ..^ M | Q i L E x φ S j i 0 ..^ M | Q i L E S j
599 139 adantr φ x 0 0 ..^ M
600 523 ad2antrr φ x E x = B Q 0 A
601 iftrue E x = B if E x = B A E x = A
602 601 eqcomd E x = B A = if E x = B A E x
603 602 adantl φ x E x = B A = if E x = B A E x
604 600 603 breqtrd φ x E x = B Q 0 if E x = B A E x
605 522 adantr φ x Q 0
606 112 adantr φ x A
607 606 rexrd φ x A *
608 216 adantr φ x B
609 iocssre A * B A B
610 607 608 609 syl2anc φ x A B
611 551 ffvelrnda φ x E x A B
612 610 611 sseldd φ x E x
613 155 adantr φ x Q 0 = A
614 elioc2 A * B E x A B E x A < E x E x B
615 607 608 614 syl2anc φ x E x A B E x A < E x E x B
616 611 615 mpbid φ x E x A < E x E x B
617 616 simp2d φ x A < E x
618 613 617 eqbrtrd φ x Q 0 < E x
619 605 612 618 ltled φ x Q 0 E x
620 619 adantr φ x ¬ E x = B Q 0 E x
621 iffalse ¬ E x = B if E x = B A E x = E x
622 621 eqcomd ¬ E x = B E x = if E x = B A E x
623 622 adantl φ x ¬ E x = B E x = if E x = B A E x
624 620 623 breqtrd φ x ¬ E x = B Q 0 if E x = B A E x
625 604 624 pm2.61dan φ x Q 0 if E x = B A E x
626 13 a1i φ x L = y A B if y = B A y
627 eqeq1 y = E x y = B E x = B
628 id y = E x y = E x
629 627 628 ifbieq2d y = E x if y = B A y = if E x = B A E x
630 629 adantl φ x y = E x if y = B A y = if E x = B A E x
631 606 612 ifcld φ x if E x = B A E x
632 626 630 611 631 fvmptd φ x L E x = if E x = B A E x
633 625 632 breqtrrd φ x Q 0 L E x
634 143 breq1d i = 0 Q i L E x Q 0 L E x
635 634 elrab 0 i 0 ..^ M | Q i L E x 0 0 ..^ M Q 0 L E x
636 599 633 635 sylanbrc φ x 0 i 0 ..^ M | Q i L E x
637 ne0i 0 i 0 ..^ M | Q i L E x i 0 ..^ M | Q i L E x
638 636 637 syl φ x i 0 ..^ M | Q i L E x
639 598 638 vtoclg S j φ S j i 0 ..^ M | Q i L E S j
640 43 66 639 sylc φ j 0 ..^ N i 0 ..^ M | Q i L E S j
641 640 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j i 0 ..^ M | Q i L E S j
642 595 a1i φ j 0 ..^ N i 0 ..^ M | Q i L E S j
643 fzofi 0 ..^ M Fin
644 ssfi 0 ..^ M Fin i 0 ..^ M | Q i L E S j 0 ..^ M i 0 ..^ M | Q i L E S j Fin
645 643 590 644 mp2an i 0 ..^ M | Q i L E S j Fin
646 645 a1i φ j 0 ..^ N i 0 ..^ M | Q i L E S j Fin
647 fimaxre2 i 0 ..^ M | Q i L E S j i 0 ..^ M | Q i L E S j Fin x l i 0 ..^ M | Q i L E S j l x
648 642 646 647 syl2anc φ j 0 ..^ N x l i 0 ..^ M | Q i L E S j l x
649 648 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j x l i 0 ..^ M | Q i L E S j l x
650 0red φ j 0 ..^ N 0
651 594 48 sseldi φ j 0 ..^ N I S j
652 1red φ j 0 ..^ N 1
653 651 652 readdcld φ j 0 ..^ N I S j + 1
654 elfzouz I S j 0 ..^ M I S j 0
655 eluzle I S j 0 0 I S j
656 48 654 655 3syl φ j 0 ..^ N 0 I S j
657 385 a1i φ j 0 ..^ N 0 < 1
658 651 652 656 657 addgegt0d φ j 0 ..^ N 0 < I S j + 1
659 650 653 658 ltled φ j 0 ..^ N 0 I S j + 1
660 659 adantr φ j 0 ..^ N ¬ I S j = M 1 0 I S j + 1
661 651 adantr φ j 0 ..^ N ¬ I S j = M 1 I S j
662 1red φ 1
663 392 662 resubcld φ M 1
664 663 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 M 1
665 1red φ j 0 ..^ N ¬ I S j = M 1 1
666 elfzolt2 I S j 0 ..^ M I S j < M
667 48 666 syl φ j 0 ..^ N I S j < M
668 44 elfzelzd φ j 0 ..^ N I S j
669 97 adantr φ j 0 ..^ N M
670 zltlem1 I S j M I S j < M I S j M 1
671 668 669 670 syl2anc φ j 0 ..^ N I S j < M I S j M 1
672 667 671 mpbid φ j 0 ..^ N I S j M 1
673 672 adantr φ j 0 ..^ N ¬ I S j = M 1 I S j M 1
674 neqne ¬ I S j = M 1 I S j M 1
675 674 necomd ¬ I S j = M 1 M 1 I S j
676 675 adantl φ j 0 ..^ N ¬ I S j = M 1 M 1 I S j
677 661 664 673 676 leneltd φ j 0 ..^ N ¬ I S j = M 1 I S j < M 1
678 661 664 665 677 ltadd1dd φ j 0 ..^ N ¬ I S j = M 1 I S j + 1 < M - 1 + 1
679 580 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 M - 1 + 1 = M
680 678 679 breqtrd φ j 0 ..^ N ¬ I S j = M 1 I S j + 1 < M
681 50 elfzelzd φ j 0 ..^ N I S j + 1
682 681 adantr φ j 0 ..^ N ¬ I S j = M 1 I S j + 1
683 0zd φ j 0 ..^ N ¬ I S j = M 1 0
684 97 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 M
685 elfzo I S j + 1 0 M I S j + 1 0 ..^ M 0 I S j + 1 I S j + 1 < M
686 682 683 684 685 syl3anc φ j 0 ..^ N ¬ I S j = M 1 I S j + 1 0 ..^ M 0 I S j + 1 I S j + 1 < M
687 660 680 686 mpbir2and φ j 0 ..^ N ¬ I S j = M 1 I S j + 1 0 ..^ M
688 687 adantr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j I S j + 1 0 ..^ M
689 simpr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j Q I S j + 1 L E S j
690 fveq2 i = I S j + 1 Q i = Q I S j + 1
691 690 breq1d i = I S j + 1 Q i L E S j Q I S j + 1 L E S j
692 691 elrab I S j + 1 i 0 ..^ M | Q i L E S j I S j + 1 0 ..^ M Q I S j + 1 L E S j
693 688 689 692 sylanbrc φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j I S j + 1 i 0 ..^ M | Q i L E S j
694 suprub i 0 ..^ M | Q i L E S j i 0 ..^ M | Q i L E S j x l i 0 ..^ M | Q i L E S j l x I S j + 1 i 0 ..^ M | Q i L E S j I S j + 1 sup i 0 ..^ M | Q i L E S j <
695 596 641 649 693 694 syl31anc φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j I S j + 1 sup i 0 ..^ M | Q i L E S j <
696 63 eqcomd φ j 0 ..^ N sup i 0 ..^ M | Q i L E S j < = I S j
697 696 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j sup i 0 ..^ M | Q i L E S j < = I S j
698 695 697 breqtrd φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j I S j + 1 I S j
699 651 ltp1d φ j 0 ..^ N I S j < I S j + 1
700 651 653 ltnled φ j 0 ..^ N I S j < I S j + 1 ¬ I S j + 1 I S j
701 699 700 mpbid φ j 0 ..^ N ¬ I S j + 1 I S j
702 701 ad2antrr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1 L E S j ¬ I S j + 1 I S j
703 698 702 pm2.65da φ j 0 ..^ N ¬ I S j = M 1 ¬ Q I S j + 1 L E S j
704 562 adantr φ j 0 ..^ N ¬ I S j = M 1 L E S j
705 51 adantr φ j 0 ..^ N ¬ I S j = M 1 Q I S j + 1
706 704 705 ltnled φ j 0 ..^ N ¬ I S j = M 1 L E S j < Q I S j + 1 ¬ Q I S j + 1 L E S j
707 703 706 mpbird φ j 0 ..^ N ¬ I S j = M 1 L E S j < Q I S j + 1
708 707 adantlr φ j 0 ..^ N ¬ E S j = B ¬ I S j = M 1 L E S j < Q I S j + 1
709 589 708 eqbrtrd φ j 0 ..^ N ¬ E S j = B ¬ I S j = M 1 E S j < Q I S j + 1
710 588 709 pm2.61dan φ j 0 ..^ N ¬ E S j = B E S j < Q I S j + 1
711 3 3ad2ant1 φ j 0 ..^ N E S j < Q I S j + 1 M
712 4 3ad2ant1 φ j 0 ..^ N E S j < Q I S j + 1 Q P M
713 5 3ad2ant1 φ j 0 ..^ N E S j < Q I S j + 1 C
714 6 3ad2ant1 φ j 0 ..^ N E S j < Q I S j + 1 D
715 7 3ad2ant1 φ j 0 ..^ N E S j < Q I S j + 1 C < D
716 50 3adant3 φ j 0 ..^ N E S j < Q I S j + 1 I S j + 1 0 M
717 simp2 φ j 0 ..^ N E S j < Q I S j + 1 j 0 ..^ N
718 43 leidd φ j 0 ..^ N S j S j
719 elico2 S j S j + 1 * S j S j S j + 1 S j S j S j S j < S j + 1
720 43 210 719 syl2anc φ j 0 ..^ N S j S j S j + 1 S j S j S j S j < S j + 1
721 43 718 129 720 mpbir3and φ j 0 ..^ N S j S j S j + 1
722 721 3adant3 φ j 0 ..^ N E S j < Q I S j + 1 S j S j S j + 1
723 simp3 φ j 0 ..^ N E S j < Q I S j + 1 E S j < Q I S j + 1
724 eqid Q I S j + 1 E S j S j = Q I S j + 1 E S j S j
725 1 2 711 712 713 714 715 8 9 10 11 12 716 717 722 723 724 fourierdlem63 φ j 0 ..^ N E S j < Q I S j + 1 E S j + 1 Q I S j + 1
726 725 3adant1r φ S j j 0 ..^ N E S j < Q I S j + 1 E S j + 1 Q I S j + 1
727 540 541 710 726 syl3anc φ j 0 ..^ N ¬ E S j = B E S j + 1 Q I S j + 1
728 539 727 pm2.61dan φ j 0 ..^ N E S j + 1 Q I S j + 1
729 ioossioo Q I S j * Q I S j + 1 * Q I S j L E S j E S j + 1 Q I S j + 1 L E S j E S j + 1 Q I S j Q I S j + 1
730 46 52 90 728 729 syl22anc φ j 0 ..^ N L E S j E S j + 1 Q I S j Q I S j + 1