Metamath Proof Explorer


Theorem fourierdlem65

Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fourierdlem65.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
2 fourierdlem65.t T = B A
3 fourierdlem65.m φ M
4 fourierdlem65.q φ Q P M
5 fourierdlem65.c φ C
6 fourierdlem65.d φ D C +∞
7 fourierdlem65.o O = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
8 fourierdlem65.n N = C D y C D | k y + k B A ran Q 1
9 fourierdlem65.s S = ι f | f Isom < , < 0 N C D y C D | k y + k B A ran Q
10 fourierdlem65.e E = x x + B x T T
11 fourierdlem65.l L = y A B if y = B A y
12 fourierdlem65.z Z = S j + B - E S j
13 11 a1i φ j 0 ..^ N E S j = B L = y A B if y = B A y
14 simpr E S j = B y = E S j y = E S j
15 simpl E S j = B y = E S j E S j = B
16 14 15 eqtrd E S j = B y = E S j y = B
17 16 iftrued E S j = B y = E S j if y = B A y = A
18 17 adantll φ j 0 ..^ N E S j = B y = E S j if y = B A y = A
19 1 3 4 fourierdlem11 φ A B A < B
20 19 simp1d φ A
21 19 simp2d φ B
22 19 simp3d φ A < B
23 20 21 22 2 10 fourierdlem4 φ E : A B
24 23 adantr φ j 0 ..^ N E : A B
25 ioossre C +∞
26 25 6 sseldi φ D
27 5 rexrd φ C *
28 pnfxr +∞ *
29 28 a1i φ +∞ *
30 ioogtlb C * +∞ * D C +∞ C < D
31 27 29 6 30 syl3anc φ C < D
32 id y = x y = x
33 2 eqcomi B A = T
34 33 oveq2i k B A = k T
35 34 a1i y = x k B A = k T
36 32 35 oveq12d y = x y + k B A = x + k T
37 36 eleq1d y = x y + k B A ran Q x + k T ran Q
38 37 rexbidv y = x k y + k B A ran Q k x + k T ran Q
39 38 cbvrabv y C D | k y + k B A ran Q = x C D | k x + k T ran Q
40 39 uneq2i C D y C D | k y + k B A ran Q = C D x C D | k x + k T ran Q
41 2 1 3 4 5 26 31 7 40 8 9 fourierdlem54 φ N S O N S Isom < , < 0 N C D y C D | k y + k B A ran Q
42 41 simpld φ N S O N
43 42 simprd φ S O N
44 42 simpld φ N
45 7 fourierdlem2 N S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
46 44 45 syl φ S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
47 43 46 mpbid φ S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
48 47 simpld φ S 0 N
49 elmapi S 0 N S : 0 N
50 48 49 syl φ S : 0 N
51 50 adantr φ j 0 ..^ N S : 0 N
52 elfzofz j 0 ..^ N j 0 N
53 52 adantl φ j 0 ..^ N j 0 N
54 51 53 ffvelrnd φ j 0 ..^ N S j
55 24 54 ffvelrnd φ j 0 ..^ N E S j A B
56 55 adantr φ j 0 ..^ N E S j = B E S j A B
57 20 ad2antrr φ j 0 ..^ N E S j = B A
58 13 18 56 57 fvmptd φ j 0 ..^ N E S j = B L E S j = A
59 58 oveq2d φ j 0 ..^ N E S j = B E S j + 1 L E S j = E S j + 1 A
60 21 ad2antrr φ j 0 ..^ N E S j = B B
61 22 ad2antrr φ j 0 ..^ N E S j = B A < B
62 54 adantr φ j 0 ..^ N E S j = B S j
63 simpr φ j 0 ..^ N E S j = B E S j = B
64 fzofzp1 j 0 ..^ N j + 1 0 N
65 64 adantl φ j 0 ..^ N j + 1 0 N
66 51 65 ffvelrnd φ j 0 ..^ N S j + 1
67 66 adantr φ j 0 ..^ N E S j = B S j + 1
68 elfzoelz j 0 ..^ N j
69 68 zred j 0 ..^ N j
70 69 adantl φ j 0 ..^ N j
71 70 ltp1d φ j 0 ..^ N j < j + 1
72 41 simprd φ S Isom < , < 0 N C D y C D | k y + k B A ran Q
73 72 adantr φ j 0 ..^ N S Isom < , < 0 N C D y C D | k y + k B A ran Q
74 isorel S Isom < , < 0 N C D y C D | k y + k B A ran Q j 0 N j + 1 0 N j < j + 1 S j < S j + 1
75 73 53 65 74 syl12anc φ j 0 ..^ N j < j + 1 S j < S j + 1
76 71 75 mpbid φ j 0 ..^ N S j < S j + 1
77 76 adantr φ j 0 ..^ N E S j = B S j < S j + 1
78 isof1o S Isom < , < 0 N C D y C D | k y + k B A ran Q S : 0 N 1-1 onto C D y C D | k y + k B A ran Q
79 f1ofo S : 0 N 1-1 onto C D y C D | k y + k B A ran Q S : 0 N onto C D y C D | k y + k B A ran Q
80 72 78 79 3syl φ S : 0 N onto C D y C D | k y + k B A ran Q
81 80 ad3antrrr φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T S : 0 N onto C D y C D | k y + k B A ran Q
82 5 ad2antrr φ j 0 ..^ N ¬ S j + 1 S j + T C
83 26 ad2antrr φ j 0 ..^ N ¬ S j + 1 S j + T D
84 21 20 resubcld φ B A
85 2 84 eqeltrid φ T
86 85 adantr φ j 0 ..^ N T
87 54 86 readdcld φ j 0 ..^ N S j + T
88 87 adantr φ j 0 ..^ N ¬ S j + 1 S j + T S j + T
89 5 adantr φ j 0 ..^ N C
90 7 44 43 fourierdlem15 φ S : 0 N C D
91 90 adantr φ j 0 ..^ N S : 0 N C D
92 91 53 ffvelrnd φ j 0 ..^ N S j C D
93 26 adantr φ j 0 ..^ N D
94 elicc2 C D S j C D S j C S j S j D
95 89 93 94 syl2anc φ j 0 ..^ N S j C D S j C S j S j D
96 92 95 mpbid φ j 0 ..^ N S j C S j S j D
97 96 simp2d φ j 0 ..^ N C S j
98 20 21 posdifd φ A < B 0 < B A
99 22 98 mpbid φ 0 < B A
100 99 2 breqtrrdi φ 0 < T
101 85 100 elrpd φ T +
102 101 adantr φ j 0 ..^ N T +
103 54 102 ltaddrpd φ j 0 ..^ N S j < S j + T
104 89 54 87 97 103 lelttrd φ j 0 ..^ N C < S j + T
105 89 87 104 ltled φ j 0 ..^ N C S j + T
106 105 adantr φ j 0 ..^ N ¬ S j + 1 S j + T C S j + T
107 66 adantr φ j 0 ..^ N ¬ S j + 1 S j + T S j + 1
108 simpr φ j 0 ..^ N ¬ S j + 1 S j + T ¬ S j + 1 S j + T
109 88 107 ltnled φ j 0 ..^ N ¬ S j + 1 S j + T S j + T < S j + 1 ¬ S j + 1 S j + T
110 108 109 mpbird φ j 0 ..^ N ¬ S j + 1 S j + T S j + T < S j + 1
111 91 65 ffvelrnd φ j 0 ..^ N S j + 1 C D
112 elicc2 C D S j + 1 C D S j + 1 C S j + 1 S j + 1 D
113 89 93 112 syl2anc φ j 0 ..^ N S j + 1 C D S j + 1 C S j + 1 S j + 1 D
114 111 113 mpbid φ j 0 ..^ N S j + 1 C S j + 1 S j + 1 D
115 114 simp3d φ j 0 ..^ N S j + 1 D
116 115 adantr φ j 0 ..^ N ¬ S j + 1 S j + T S j + 1 D
117 88 107 83 110 116 ltletrd φ j 0 ..^ N ¬ S j + 1 S j + T S j + T < D
118 88 83 117 ltled φ j 0 ..^ N ¬ S j + 1 S j + T S j + T D
119 82 83 88 106 118 eliccd φ j 0 ..^ N ¬ S j + 1 S j + T S j + T C D
120 119 adantlr φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T S j + T C D
121 10 a1i φ j 0 ..^ N E = x x + B x T T
122 id x = S j x = S j
123 oveq2 x = S j B x = B S j
124 123 oveq1d x = S j B x T = B S j T
125 124 fveq2d x = S j B x T = B S j T
126 125 oveq1d x = S j B x T T = B S j T T
127 122 126 oveq12d x = S j x + B x T T = S j + B S j T T
128 127 adantl φ j 0 ..^ N x = S j x + B x T T = S j + B S j T T
129 21 adantr φ j 0 ..^ N B
130 129 54 resubcld φ j 0 ..^ N B S j
131 130 102 rerpdivcld φ j 0 ..^ N B S j T
132 131 flcld φ j 0 ..^ N B S j T
133 132 zred φ j 0 ..^ N B S j T
134 133 86 remulcld φ j 0 ..^ N B S j T T
135 54 134 readdcld φ j 0 ..^ N S j + B S j T T
136 121 128 54 135 fvmptd φ j 0 ..^ N E S j = S j + B S j T T
137 136 oveq1d φ j 0 ..^ N E S j S j = S j + B S j T T - S j
138 137 oveq1d φ j 0 ..^ N E S j S j T = S j + B S j T T - S j T
139 54 recnd φ j 0 ..^ N S j
140 134 recnd φ j 0 ..^ N B S j T T
141 139 140 pncan2d φ j 0 ..^ N S j + B S j T T - S j = B S j T T
142 141 oveq1d φ j 0 ..^ N S j + B S j T T - S j T = B S j T T T
143 133 recnd φ j 0 ..^ N B S j T
144 86 recnd φ j 0 ..^ N T
145 102 rpne0d φ j 0 ..^ N T 0
146 143 144 145 divcan4d φ j 0 ..^ N B S j T T T = B S j T
147 138 142 146 3eqtrd φ j 0 ..^ N E S j S j T = B S j T
148 147 132 eqeltrd φ j 0 ..^ N E S j S j T
149 peano2zm E S j S j T E S j S j T 1
150 148 149 syl φ j 0 ..^ N E S j S j T 1
151 150 ad2antrr φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T E S j S j T 1
152 33 oveq2i E S j S j T 1 B A = E S j S j T 1 T
153 152 oveq2i S j + T + E S j S j T 1 B A = S j + T + E S j S j T 1 T
154 153 a1i φ j 0 ..^ N E S j = B S j + T + E S j S j T 1 B A = S j + T + E S j S j T 1 T
155 136 adantr φ j 0 ..^ N E S j = B E S j = S j + B S j T T
156 oveq1 E S j = B E S j S j = B S j
157 156 eqcomd E S j = B B S j = E S j S j
158 157 oveq1d E S j = B B S j T = E S j S j T
159 158 fveq2d E S j = B B S j T = E S j S j T
160 159 oveq1d E S j = B B S j T T = E S j S j T T
161 160 oveq2d E S j = B S j + B S j T T = S j + E S j S j T T
162 161 adantl φ j 0 ..^ N E S j = B S j + B S j T T = S j + E S j S j T T
163 147 143 eqeltrd φ j 0 ..^ N E S j S j T
164 1cnd φ j 0 ..^ N 1
165 163 164 144 subdird φ j 0 ..^ N E S j S j T 1 T = E S j S j T T 1 T
166 85 recnd φ T
167 166 mulid2d φ 1 T = T
168 167 oveq2d φ E S j S j T T 1 T = E S j S j T T T
169 168 adantr φ j 0 ..^ N E S j S j T T 1 T = E S j S j T T T
170 165 169 eqtrd φ j 0 ..^ N E S j S j T 1 T = E S j S j T T T
171 170 oveq2d φ j 0 ..^ N S j + T + E S j S j T 1 T = S j + T + E S j S j T T T
172 163 144 mulcld φ j 0 ..^ N E S j S j T T
173 139 144 172 ppncand φ j 0 ..^ N S j + T + E S j S j T T T = S j + E S j S j T T
174 flid E S j S j T E S j S j T = E S j S j T
175 148 174 syl φ j 0 ..^ N E S j S j T = E S j S j T
176 175 eqcomd φ j 0 ..^ N E S j S j T = E S j S j T
177 176 oveq1d φ j 0 ..^ N E S j S j T T = E S j S j T T
178 177 oveq2d φ j 0 ..^ N S j + E S j S j T T = S j + E S j S j T T
179 171 173 178 3eqtrrd φ j 0 ..^ N S j + E S j S j T T = S j + T + E S j S j T 1 T
180 179 adantr φ j 0 ..^ N E S j = B S j + E S j S j T T = S j + T + E S j S j T 1 T
181 155 162 180 3eqtrrd φ j 0 ..^ N E S j = B S j + T + E S j S j T 1 T = E S j
182 154 181 63 3eqtrd φ j 0 ..^ N E S j = B S j + T + E S j S j T 1 B A = B
183 1 fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
184 3 183 syl φ Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
185 4 184 mpbid φ Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
186 185 simprd φ Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
187 186 simpld φ Q 0 = A Q M = B
188 187 simprd φ Q M = B
189 188 eqcomd φ B = Q M
190 1 3 4 fourierdlem15 φ Q : 0 M A B
191 ffn Q : 0 M A B Q Fn 0 M
192 190 191 syl φ Q Fn 0 M
193 3 nnnn0d φ M 0
194 nn0uz 0 = 0
195 193 194 eleqtrdi φ M 0
196 eluzfz2 M 0 M 0 M
197 195 196 syl φ M 0 M
198 fnfvelrn Q Fn 0 M M 0 M Q M ran Q
199 192 197 198 syl2anc φ Q M ran Q
200 189 199 eqeltrd φ B ran Q
201 200 ad2antrr φ j 0 ..^ N E S j = B B ran Q
202 182 201 eqeltrd φ j 0 ..^ N E S j = B S j + T + E S j S j T 1 B A ran Q
203 202 adantr φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T S j + T + E S j S j T 1 B A ran Q
204 oveq1 k = E S j S j T 1 k B A = E S j S j T 1 B A
205 204 oveq2d k = E S j S j T 1 S j + T + k B A = S j + T + E S j S j T 1 B A
206 205 eleq1d k = E S j S j T 1 S j + T + k B A ran Q S j + T + E S j S j T 1 B A ran Q
207 206 rspcev E S j S j T 1 S j + T + E S j S j T 1 B A ran Q k S j + T + k B A ran Q
208 151 203 207 syl2anc φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T k S j + T + k B A ran Q
209 oveq1 y = S j + T y + k B A = S j + T + k B A
210 209 eleq1d y = S j + T y + k B A ran Q S j + T + k B A ran Q
211 210 rexbidv y = S j + T k y + k B A ran Q k S j + T + k B A ran Q
212 211 elrab S j + T y C D | k y + k B A ran Q S j + T C D k S j + T + k B A ran Q
213 120 208 212 sylanbrc φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T S j + T y C D | k y + k B A ran Q
214 elun2 S j + T y C D | k y + k B A ran Q S j + T C D y C D | k y + k B A ran Q
215 213 214 syl φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T S j + T C D y C D | k y + k B A ran Q
216 foelrn S : 0 N onto C D y C D | k y + k B A ran Q S j + T C D y C D | k y + k B A ran Q i 0 N S j + T = S i
217 81 215 216 syl2anc φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T i 0 N S j + T = S i
218 eqcom S j + T = S i S i = S j + T
219 218 rexbii i 0 N S j + T = S i i 0 N S i = S j + T
220 217 219 sylib φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T i 0 N S i = S j + T
221 103 ad2antrr φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S j < S j + T
222 218 biimpri S i = S j + T S j + T = S i
223 222 adantl φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S j + T = S i
224 221 223 breqtrd φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S j < S i
225 110 adantr φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S j + T < S j + 1
226 223 225 eqbrtrrd φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S i < S j + 1
227 224 226 jca φ j 0 ..^ N ¬ S j + 1 S j + T S i = S j + T S j < S i S i < S j + 1
228 227 adantlr φ j 0 ..^ N ¬ S j + 1 S j + T i 0 N S i = S j + T S j < S i S i < S j + 1
229 simplll φ j 0 ..^ N ¬ S j + 1 S j + T i 0 N S i = S j + T φ j 0 ..^ N
230 simplr φ j 0 ..^ N ¬ S j + 1 S j + T i 0 N S i = S j + T i 0 N
231 elfzelz i 0 N i
232 231 ad2antlr φ j 0 ..^ N i 0 N S j < S i S i < S j + 1 i
233 68 ad3antlr φ j 0 ..^ N i 0 N S j < S i S i < S j + 1 j
234 simpr φ j 0 ..^ N i 0 N S j < S i S j < S i
235 73 ad2antrr φ j 0 ..^ N i 0 N S j < S i S Isom < , < 0 N C D y C D | k y + k B A ran Q
236 53 ad2antrr φ j 0 ..^ N i 0 N S j < S i j 0 N
237 simplr φ j 0 ..^ N i 0 N S j < S i i 0 N
238 isorel S Isom < , < 0 N C D y C D | k y + k B A ran Q j 0 N i 0 N j < i S j < S i
239 235 236 237 238 syl12anc φ j 0 ..^ N i 0 N S j < S i j < i S j < S i
240 234 239 mpbird φ j 0 ..^ N i 0 N S j < S i j < i
241 240 adantrr φ j 0 ..^ N i 0 N S j < S i S i < S j + 1 j < i
242 simpr φ j 0 ..^ N i 0 N S i < S j + 1 S i < S j + 1
243 73 ad2antrr φ j 0 ..^ N i 0 N S i < S j + 1 S Isom < , < 0 N C D y C D | k y + k B A ran Q
244 simplr φ j 0 ..^ N i 0 N S i < S j + 1 i 0 N
245 65 ad2antrr φ j 0 ..^ N i 0 N S i < S j + 1 j + 1 0 N
246 isorel S Isom < , < 0 N C D y C D | k y + k B A ran Q i 0 N j + 1 0 N i < j + 1 S i < S j + 1
247 243 244 245 246 syl12anc φ j 0 ..^ N i 0 N S i < S j + 1 i < j + 1 S i < S j + 1
248 242 247 mpbird φ j 0 ..^ N i 0 N S i < S j + 1 i < j + 1
249 248 adantrl φ j 0 ..^ N i 0 N S j < S i S i < S j + 1 i < j + 1
250 btwnnz j j < i i < j + 1 ¬ i
251 233 241 249 250 syl3anc φ j 0 ..^ N i 0 N S j < S i S i < S j + 1 ¬ i
252 232 251 pm2.65da φ j 0 ..^ N i 0 N ¬ S j < S i S i < S j + 1
253 229 230 252 syl2anc φ j 0 ..^ N ¬ S j + 1 S j + T i 0 N S i = S j + T ¬ S j < S i S i < S j + 1
254 228 253 pm2.65da φ j 0 ..^ N ¬ S j + 1 S j + T i 0 N ¬ S i = S j + T
255 254 nrexdv φ j 0 ..^ N ¬ S j + 1 S j + T ¬ i 0 N S i = S j + T
256 255 adantlr φ j 0 ..^ N E S j = B ¬ S j + 1 S j + T ¬ i 0 N S i = S j + T
257 220 256 condan φ j 0 ..^ N E S j = B S j + 1 S j + T
258 62 rexrd φ j 0 ..^ N E S j = B S j *
259 85 ad2antrr φ j 0 ..^ N E S j = B T
260 62 259 readdcld φ j 0 ..^ N E S j = B S j + T
261 elioc2 S j * S j + T S j + 1 S j S j + T S j + 1 S j < S j + 1 S j + 1 S j + T
262 258 260 261 syl2anc φ j 0 ..^ N E S j = B S j + 1 S j S j + T S j + 1 S j < S j + 1 S j + 1 S j + T
263 67 77 257 262 mpbir3and φ j 0 ..^ N E S j = B S j + 1 S j S j + T
264 57 60 61 2 10 62 63 263 fourierdlem26 φ j 0 ..^ N E S j = B E S j + 1 = A + S j + 1 - S j
265 264 oveq1d φ j 0 ..^ N E S j = B E S j + 1 A = A + S j + 1 S j - A
266 57 recnd φ j 0 ..^ N E S j = B A
267 66 recnd φ j 0 ..^ N S j + 1
268 267 139 subcld φ j 0 ..^ N S j + 1 S j
269 268 adantr φ j 0 ..^ N E S j = B S j + 1 S j
270 266 269 pncan2d φ j 0 ..^ N E S j = B A + S j + 1 S j - A = S j + 1 S j
271 59 265 270 3eqtrd φ j 0 ..^ N E S j = B E S j + 1 L E S j = S j + 1 S j
272 11 a1i φ j 0 ..^ N ¬ E S j = B L = y A B if y = B A y
273 eqcom y = E S j E S j = y
274 273 biimpi y = E S j E S j = y
275 274 adantl ¬ E S j = B y = E S j E S j = y
276 neqne ¬ E S j = B E S j B
277 276 adantr ¬ E S j = B y = E S j E S j B
278 275 277 eqnetrrd ¬ E S j = B y = E S j y B
279 278 neneqd ¬ E S j = B y = E S j ¬ y = B
280 279 iffalsed ¬ E S j = B y = E S j if y = B A y = y
281 simpr ¬ E S j = B y = E S j y = E S j
282 280 281 eqtrd ¬ E S j = B y = E S j if y = B A y = E S j
283 282 adantll φ j 0 ..^ N ¬ E S j = B y = E S j if y = B A y = E S j
284 55 adantr φ j 0 ..^ N ¬ E S j = B E S j A B
285 272 283 284 284 fvmptd φ j 0 ..^ N ¬ E S j = B L E S j = E S j
286 285 oveq2d φ j 0 ..^ N ¬ E S j = B E S j + 1 L E S j = E S j + 1 E S j
287 id x = S j + 1 x = S j + 1
288 oveq2 x = S j + 1 B x = B S j + 1
289 288 oveq1d x = S j + 1 B x T = B S j + 1 T
290 289 fveq2d x = S j + 1 B x T = B S j + 1 T
291 290 oveq1d x = S j + 1 B x T T = B S j + 1 T T
292 287 291 oveq12d x = S j + 1 x + B x T T = S j + 1 + B S j + 1 T T
293 292 adantl φ j 0 ..^ N x = S j + 1 x + B x T T = S j + 1 + B S j + 1 T T
294 129 66 resubcld φ j 0 ..^ N B S j + 1
295 294 102 rerpdivcld φ j 0 ..^ N B S j + 1 T
296 295 flcld φ j 0 ..^ N B S j + 1 T
297 296 zred φ j 0 ..^ N B S j + 1 T
298 297 86 remulcld φ j 0 ..^ N B S j + 1 T T
299 66 298 readdcld φ j 0 ..^ N S j + 1 + B S j + 1 T T
300 121 293 66 299 fvmptd φ j 0 ..^ N E S j + 1 = S j + 1 + B S j + 1 T T
301 300 136 oveq12d φ j 0 ..^ N E S j + 1 E S j = S j + 1 + B S j + 1 T T - S j + B S j T T
302 301 adantr φ j 0 ..^ N ¬ E S j = B E S j + 1 E S j = S j + 1 + B S j + 1 T T - S j + B S j T T
303 flle B S j + 1 T B S j + 1 T B S j + 1 T
304 295 303 syl φ j 0 ..^ N B S j + 1 T B S j + 1 T
305 54 66 76 ltled φ j 0 ..^ N S j S j + 1
306 54 66 129 305 lesub2dd φ j 0 ..^ N B S j + 1 B S j
307 294 130 102 306 lediv1dd φ j 0 ..^ N B S j + 1 T B S j T
308 297 295 131 304 307 letrd φ j 0 ..^ N B S j + 1 T B S j T
309 308 adantr φ j 0 ..^ N ¬ E S j = B B S j + 1 T B S j T
310 297 adantr φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 B S j + 1 T
311 1red φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 1
312 310 311 readdcld φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 B S j + 1 T + 1
313 131 adantr φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 B S j T
314 simpr φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 ¬ B S j T < B S j + 1 T + 1
315 312 313 314 nltled φ j 0 ..^ N ¬ B S j T < B S j + 1 T + 1 B S j + 1 T + 1 B S j T
316 315 adantlr φ j 0 ..^ N ¬ E S j = B ¬ B S j T < B S j + 1 T + 1 B S j + 1 T + 1 B S j T
317 80 ad3antrrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T S : 0 N onto C D y C D | k y + k B A ran Q
318 89 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T C
319 93 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T D
320 136 135 eqeltrd φ j 0 ..^ N E S j
321 129 320 resubcld φ j 0 ..^ N B E S j
322 54 321 readdcld φ j 0 ..^ N S j + B - E S j
323 12 322 eqeltrid φ j 0 ..^ N Z
324 323 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z
325 20 rexrd φ A *
326 325 adantr φ j 0 ..^ N A *
327 elioc2 A * B E S j A B E S j A < E S j E S j B
328 326 129 327 syl2anc φ j 0 ..^ N E S j A B E S j A < E S j E S j B
329 55 328 mpbid φ j 0 ..^ N E S j A < E S j E S j B
330 329 simp3d φ j 0 ..^ N E S j B
331 129 320 subge0d φ j 0 ..^ N 0 B E S j E S j B
332 330 331 mpbird φ j 0 ..^ N 0 B E S j
333 54 321 addge01d φ j 0 ..^ N 0 B E S j S j S j + B - E S j
334 332 333 mpbid φ j 0 ..^ N S j S j + B - E S j
335 89 54 322 97 334 letrd φ j 0 ..^ N C S j + B - E S j
336 335 12 breqtrrdi φ j 0 ..^ N C Z
337 336 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T C Z
338 66 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T S j + 1
339 295 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T
340 reflcl B S j + 1 T B S j + 1 T
341 peano2re B S j + 1 T B S j + 1 T + 1
342 339 340 341 3syl φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T + 1
343 129 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B
344 343 324 resubcld φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B Z
345 102 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T T +
346 344 345 rerpdivcld φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B Z T
347 flltp1 B S j + 1 T B S j + 1 T < B S j + 1 T + 1
348 295 347 syl φ j 0 ..^ N B S j + 1 T < B S j + 1 T + 1
349 348 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T < B S j + 1 T + 1
350 296 peano2zd φ j 0 ..^ N B S j + 1 T + 1
351 350 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T + 1
352 131 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j T
353 simpr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T + 1 B S j T
354 321 102 rerpdivcld φ j 0 ..^ N B E S j T
355 354 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B E S j T
356 20 adantr φ j 0 ..^ N A
357 329 simp2d φ j 0 ..^ N A < E S j
358 356 320 129 357 ltsub2dd φ j 0 ..^ N B E S j < B A
359 358 2 breqtrrdi φ j 0 ..^ N B E S j < T
360 321 86 102 359 ltdiv1dd φ j 0 ..^ N B E S j T < T T
361 144 145 dividd φ j 0 ..^ N T T = 1
362 360 361 breqtrd φ j 0 ..^ N B E S j T < 1
363 362 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B E S j T < 1
364 130 recnd φ j 0 ..^ N B S j
365 321 recnd φ j 0 ..^ N B E S j
366 364 365 144 145 divsubdird φ j 0 ..^ N B - S j - B E S j T = B S j T B E S j T
367 366 eqcomd φ j 0 ..^ N B S j T B E S j T = B - S j - B E S j T
368 129 recnd φ j 0 ..^ N B
369 320 recnd φ j 0 ..^ N E S j
370 368 139 369 nnncan1d φ j 0 ..^ N B - S j - B E S j = E S j S j
371 370 oveq1d φ j 0 ..^ N B - S j - B E S j T = E S j S j T
372 367 371 eqtrd φ j 0 ..^ N B S j T B E S j T = E S j S j T
373 372 148 eqeltrd φ j 0 ..^ N B S j T B E S j T
374 373 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j T B E S j T
375 351 352 353 355 363 374 zltlesub φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T + 1 B S j T B E S j T
376 12 a1i φ j 0 ..^ N Z = S j + B - E S j
377 376 oveq2d φ j 0 ..^ N B Z = B S j + B - E S j
378 139 368 369 addsub12d φ j 0 ..^ N S j + B - E S j = B + S j - E S j
379 368 369 139 subsub2d φ j 0 ..^ N B E S j S j = B + S j - E S j
380 378 379 eqtr4d φ j 0 ..^ N S j + B - E S j = B E S j S j
381 380 oveq2d φ j 0 ..^ N B S j + B - E S j = B B E S j S j
382 369 139 subcld φ j 0 ..^ N E S j S j
383 368 382 nncand φ j 0 ..^ N B B E S j S j = E S j S j
384 377 381 383 3eqtrd φ j 0 ..^ N B Z = E S j S j
385 384 oveq1d φ j 0 ..^ N B Z T = E S j S j T
386 371 367 385 3eqtr4d φ j 0 ..^ N B S j T B E S j T = B Z T
387 386 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j T B E S j T = B Z T
388 375 387 breqtrd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T + 1 B Z T
389 339 342 346 349 388 ltletrd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 T < B Z T
390 294 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1
391 390 344 345 ltdiv1d φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 < B Z B S j + 1 T < B Z T
392 389 391 mpbird φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T B S j + 1 < B Z
393 324 338 343 ltsub2d φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z < S j + 1 B S j + 1 < B Z
394 392 393 mpbird φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z < S j + 1
395 115 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T S j + 1 D
396 324 338 319 394 395 ltletrd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z < D
397 324 319 396 ltled φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z D
398 318 319 324 337 397 eliccd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z C D
399 33 a1i φ j 0 ..^ N B A = T
400 399 oveq2d φ j 0 ..^ N E S j S j T B A = E S j S j T T
401 382 144 145 divcan1d φ j 0 ..^ N E S j S j T T = E S j S j
402 400 401 eqtrd φ j 0 ..^ N E S j S j T B A = E S j S j
403 376 402 oveq12d φ j 0 ..^ N Z + E S j S j T B A = S j + B E S j + E S j S j
404 139 365 addcomd φ j 0 ..^ N S j + B - E S j = B - E S j + S j
405 404 oveq1d φ j 0 ..^ N S j + B E S j + E S j S j = B E S j + S j + E S j S j
406 365 139 369 ppncand φ j 0 ..^ N B E S j + S j + E S j S j = B - E S j + E S j
407 368 369 npcand φ j 0 ..^ N B - E S j + E S j = B
408 406 407 eqtrd φ j 0 ..^ N B E S j + S j + E S j S j = B
409 403 405 408 3eqtrd φ j 0 ..^ N Z + E S j S j T B A = B
410 200 adantr φ j 0 ..^ N B ran Q
411 409 410 eqeltrd φ j 0 ..^ N Z + E S j S j T B A ran Q
412 oveq1 k = E S j S j T k B A = E S j S j T B A
413 412 oveq2d k = E S j S j T Z + k B A = Z + E S j S j T B A
414 413 eleq1d k = E S j S j T Z + k B A ran Q Z + E S j S j T B A ran Q
415 414 rspcev E S j S j T Z + E S j S j T B A ran Q k Z + k B A ran Q
416 148 411 415 syl2anc φ j 0 ..^ N k Z + k B A ran Q
417 416 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T k Z + k B A ran Q
418 oveq1 y = Z y + k B A = Z + k B A
419 418 eleq1d y = Z y + k B A ran Q Z + k B A ran Q
420 419 rexbidv y = Z k y + k B A ran Q k Z + k B A ran Q
421 420 elrab Z y C D | k y + k B A ran Q Z C D k Z + k B A ran Q
422 398 417 421 sylanbrc φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z y C D | k y + k B A ran Q
423 elun2 Z y C D | k y + k B A ran Q Z C D y C D | k y + k B A ran Q
424 422 423 syl φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z C D y C D | k y + k B A ran Q
425 foelrn S : 0 N onto C D y C D | k y + k B A ran Q Z C D y C D | k y + k B A ran Q i 0 N Z = S i
426 317 424 425 syl2anc φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T i 0 N Z = S i
427 54 adantr φ j 0 ..^ N ¬ E S j = B S j
428 321 adantr φ j 0 ..^ N ¬ E S j = B B E S j
429 320 adantr φ j 0 ..^ N ¬ E S j = B E S j
430 21 ad2antrr φ j 0 ..^ N ¬ E S j = B B
431 330 adantr φ j 0 ..^ N ¬ E S j = B E S j B
432 276 necomd ¬ E S j = B B E S j
433 432 adantl φ j 0 ..^ N ¬ E S j = B B E S j
434 429 430 431 433 leneltd φ j 0 ..^ N ¬ E S j = B E S j < B
435 429 430 posdifd φ j 0 ..^ N ¬ E S j = B E S j < B 0 < B E S j
436 434 435 mpbid φ j 0 ..^ N ¬ E S j = B 0 < B E S j
437 428 436 elrpd φ j 0 ..^ N ¬ E S j = B B E S j +
438 427 437 ltaddrpd φ j 0 ..^ N ¬ E S j = B S j < S j + B - E S j
439 438 12 breqtrrdi φ j 0 ..^ N ¬ E S j = B S j < Z
440 439 ad2antrr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i S j < Z
441 simpr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i Z = S i
442 440 441 breqtrd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i S j < S i
443 394 adantr φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i Z < S j + 1
444 441 443 eqbrtrrd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i S i < S j + 1
445 442 444 jca φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i S j < S i S i < S j + 1
446 445 ex φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T Z = S i S j < S i S i < S j + 1
447 446 reximdv φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T i 0 N Z = S i i 0 N S j < S i S i < S j + 1
448 426 447 mpd φ j 0 ..^ N ¬ E S j = B B S j + 1 T + 1 B S j T i 0 N S j < S i S i < S j + 1
449 316 448 syldan φ j 0 ..^ N ¬ E S j = B ¬ B S j T < B S j + 1 T + 1 i 0 N S j < S i S i < S j + 1
450 252 nrexdv φ j 0 ..^ N ¬ i 0 N S j < S i S i < S j + 1
451 450 ad2antrr φ j 0 ..^ N ¬ E S j = B ¬ B S j T < B S j + 1 T + 1 ¬ i 0 N S j < S i S i < S j + 1
452 449 451 condan φ j 0 ..^ N ¬ E S j = B B S j T < B S j + 1 T + 1
453 309 452 jca φ j 0 ..^ N ¬ E S j = B B S j + 1 T B S j T B S j T < B S j + 1 T + 1
454 131 adantr φ j 0 ..^ N ¬ E S j = B B S j T
455 296 adantr φ j 0 ..^ N ¬ E S j = B B S j + 1 T
456 flbi B S j T B S j + 1 T B S j T = B S j + 1 T B S j + 1 T B S j T B S j T < B S j + 1 T + 1
457 454 455 456 syl2anc φ j 0 ..^ N ¬ E S j = B B S j T = B S j + 1 T B S j + 1 T B S j T B S j T < B S j + 1 T + 1
458 453 457 mpbird φ j 0 ..^ N ¬ E S j = B B S j T = B S j + 1 T
459 458 eqcomd φ j 0 ..^ N ¬ E S j = B B S j + 1 T = B S j T
460 459 oveq1d φ j 0 ..^ N ¬ E S j = B B S j + 1 T T = B S j T T
461 460 oveq2d φ j 0 ..^ N ¬ E S j = B S j + 1 + B S j + 1 T T = S j + 1 + B S j T T
462 461 oveq1d φ j 0 ..^ N ¬ E S j = B S j + 1 + B S j + 1 T T - S j + B S j T T = S j + 1 + B S j T T - S j + B S j T T
463 267 adantr φ j 0 ..^ N ¬ E S j = B S j + 1
464 139 adantr φ j 0 ..^ N ¬ E S j = B S j
465 140 adantr φ j 0 ..^ N ¬ E S j = B B S j T T
466 463 464 465 pnpcan2d φ j 0 ..^ N ¬ E S j = B S j + 1 + B S j T T - S j + B S j T T = S j + 1 S j
467 462 466 eqtrd φ j 0 ..^ N ¬ E S j = B S j + 1 + B S j + 1 T T - S j + B S j T T = S j + 1 S j
468 286 302 467 3eqtrd φ j 0 ..^ N ¬ E S j = B E S j + 1 L E S j = S j + 1 S j
469 271 468 pm2.61dan φ j 0 ..^ N E S j + 1 L E S j = S j + 1 S j