Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem41 Structured version   Visualization version   Unicode version

Theorem fourierdlem41 38123
 Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem41.a
fourierdlem41.b
fourierdlem41.altb
fourierdlem41.t
fourierdlem41.dper
fourierdlem41.x
fourierdlem41.z
fourierdlem41.e
fourierdlem41.p ..^
fourierdlem41.m
fourierdlem41.q
fourierdlem41.qssd ..^
Assertion
Ref Expression
fourierdlem41
Distinct variable groups:   ,,   ,   ,,   ,,,   ,,,   ,,,   ,   ,,,   ,,   ,,   ,   ,,   ,   ,   ,,,   ,,   ,,   ,,,   ,,   ,,
Allowed substitution hints:   (,)   (,,)   (,)   (,,,,,)   (,)   (,,)   (,,)   ()   (,)   (,,)

Proof of Theorem fourierdlem41
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr 468 . . . . . 6
2 fourierdlem41.q . . . . . . . . . . 11
3 fourierdlem41.m . . . . . . . . . . . 12
4 fourierdlem41.p . . . . . . . . . . . . 13 ..^
54fourierdlem2 38083 . . . . . . . . . . . 12 ..^
63, 5syl 17 . . . . . . . . . . 11 ..^
72, 6mpbid 215 . . . . . . . . . 10 ..^
87simpld 466 . . . . . . . . 9
9 elmapi 7511 . . . . . . . . 9
10 ffn 5739 . . . . . . . . 9
118, 9, 103syl 18 . . . . . . . 8
1211adantr 472 . . . . . . 7
13 fvelrnb 5926 . . . . . . 7
1412, 13syl 17 . . . . . 6
151, 14mpbid 215 . . . . 5
16 0zd 10973 . . . . . . . . . . 11
17 elfzelz 11826 . . . . . . . . . . . . 13
18173ad2ant2 1052 . . . . . . . . . . . 12
19 1zzd 10992 . . . . . . . . . . . 12
2018, 19zsubcld 11068 . . . . . . . . . . 11
21 simpll 768 . . . . . . . . . . . . . . 15
22 elfzle1 11828 . . . . . . . . . . . . . . . . . . 19
2322anim1i 578 . . . . . . . . . . . . . . . . . 18
24 0red 9662 . . . . . . . . . . . . . . . . . . 19
2517zred 11063 . . . . . . . . . . . . . . . . . . . 20
2625adantr 472 . . . . . . . . . . . . . . . . . . 19
2724, 26eqleltd 9796 . . . . . . . . . . . . . . . . . 18
2823, 27mpbird 240 . . . . . . . . . . . . . . . . 17
2928eqcomd 2477 . . . . . . . . . . . . . . . 16
3029adantll 728 . . . . . . . . . . . . . . 15
31 fveq2 5879 . . . . . . . . . . . . . . . 16
327simprld 773 . . . . . . . . . . . . . . . . 17
3332simpld 466 . . . . . . . . . . . . . . . 16
3431, 33sylan9eqr 2527 . . . . . . . . . . . . . . 15
3521, 30, 34syl2anc 673 . . . . . . . . . . . . . 14
36353adantl3 1188 . . . . . . . . . . . . 13
37 simpr 468 . . . . . . . . . . . . . . . . 17
38 fourierdlem41.a . . . . . . . . . . . . . . . . . . 19
3938rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
40 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . 21
4140rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
42 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . 23
43 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . 23
44 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . 23
4538, 40, 42, 43, 44fourierdlem4 38085 . . . . . . . . . . . . . . . . . . . . . 22
46 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . 25
4746a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
48 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4940adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5049, 48resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5140, 38resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5243, 51syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
54 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5538, 40posdifd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5642, 55mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5743eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5857a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5956, 58breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6054, 59gtned 9787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6160adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6250, 53, 61redivcld 10457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6362flcld 12067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6463zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6564, 53remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
66 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6766fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6848, 65, 67syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6968oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25
7069mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . . . . 24
7147, 70eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23
7271feq1d 5724 . . . . . . . . . . . . . . . . . . . . . 22
7345, 72mpbird 240 . . . . . . . . . . . . . . . . . . . . 21
74 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . 21
7573, 74ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20
76 iocgtlb 37695 . . . . . . . . . . . . . . . . . . . 20
7739, 41, 75, 76syl3anc 1292 . . . . . . . . . . . . . . . . . . 19
7838, 77gtned 9787 . . . . . . . . . . . . . . . . . 18
7978adantr 472 . . . . . . . . . . . . . . . . 17
8037, 79eqnetrd 2710 . . . . . . . . . . . . . . . 16
8180adantr 472 . . . . . . . . . . . . . . 15
82813adantl2 1187 . . . . . . . . . . . . . 14
8382neneqd 2648 . . . . . . . . . . . . 13
8436, 83condan 811 . . . . . . . . . . . 12
85 zltlem1 11013 . . . . . . . . . . . . 13
8616, 18, 85syl2anc 673 . . . . . . . . . . . 12
8784, 86mpbid 215 . . . . . . . . . . 11
88 eluz2 11188 . . . . . . . . . . 11
8916, 20, 87, 88syl3anbrc 1214 . . . . . . . . . 10
90 elfzel2 11824 . . . . . . . . . . 11
91903ad2ant2 1052 . . . . . . . . . 10
92 1red 9676 . . . . . . . . . . . . 13
9325, 92resubcld 10068 . . . . . . . . . . . 12
9490zred 11063 . . . . . . . . . . . 12
9525ltm1d 10561 . . . . . . . . . . . 12
96 elfzle2 11829 . . . . . . . . . . . 12
9793, 25, 94, 95, 96ltletrd 9812 . . . . . . . . . . 11
98973ad2ant2 1052 . . . . . . . . . 10
99 elfzo2 11950 . . . . . . . . . 10 ..^
10089, 91, 98, 99syl3anbrc 1214 . . . . . . . . 9 ..^
1018, 9syl 17 . . . . . . . . . . . . 13
1021013ad2ant1 1051 . . . . . . . . . . . 12
10316, 91, 203jca 1210 . . . . . . . . . . . . . 14
10493, 94, 97ltled 9800 . . . . . . . . . . . . . . 15
1051043ad2ant2 1052 . . . . . . . . . . . . . 14
106103, 87, 105jca32 544 . . . . . . . . . . . . 13
107 elfz2 11817 . . . . . . . . . . . . 13
108106, 107sylibr 217 . . . . . . . . . . . 12
109102, 108ffvelrnd 6038 . . . . . . . . . . 11
110109rexrd 9708 . . . . . . . . . 10
11125recnd 9687 . . . . . . . . . . . . . . 15
112 1cnd 9677 . . . . . . . . . . . . . . 15
113111, 112npcand 10009 . . . . . . . . . . . . . 14
114113fveq2d 5883 . . . . . . . . . . . . 13
115114adantl 473 . . . . . . . . . . . 12
116101ffvelrnda 6037 . . . . . . . . . . . . 13
117116rexrd 9708 . . . . . . . . . . . 12
118115, 117eqeltrd 2549 . . . . . . . . . . 11
1191183adant3 1050 . . . . . . . . . 10
120 id 22 . . . . . . . . . . . . . . . 16
121 fveq2 5879 . . . . . . . . . . . . . . . 16
122120, 121oveq12d 6326 . . . . . . . . . . . . . . 15
123122adantl 473 . . . . . . . . . . . . . 14
12466a1i 11 . . . . . . . . . . . . . . . . 17
125 oveq2 6316 . . . . . . . . . . . . . . . . . . . . 21
126125oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20
127126fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
128127oveq1d 6323 . . . . . . . . . . . . . . . . . 18
129128adantl 473 . . . . . . . . . . . . . . . . 17
13040, 74resubcld 10068 . . . . . . . . . . . . . . . . . . . . 21
131130, 52, 60redivcld 10457 . . . . . . . . . . . . . . . . . . . 20
132131flcld 12067 . . . . . . . . . . . . . . . . . . 19
133132zred 11063 . . . . . . . . . . . . . . . . . 18
134133, 52remulcld 9689 . . . . . . . . . . . . . . . . 17
135124, 129, 74, 134fvmptd 5969 . . . . . . . . . . . . . . . 16
136135, 134eqeltrd 2549 . . . . . . . . . . . . . . 15
13774, 136readdcld 9688 . . . . . . . . . . . . . 14
13847, 123, 74, 137fvmptd 5969 . . . . . . . . . . . . 13
139138, 137eqeltrd 2549 . . . . . . . . . . . 12
140139rexrd 9708 . . . . . . . . . . 11
1411403ad2ant1 1051 . . . . . . . . . 10
142 simp1 1030 . . . . . . . . . . . . 13
143 ovex 6336 . . . . . . . . . . . . . 14
144 eleq1 2537 . . . . . . . . . . . . . . . 16 ..^ ..^
145144anbi2d 718 . . . . . . . . . . . . . . 15 ..^ ..^
146 fveq2 5879 . . . . . . . . . . . . . . . 16
147 oveq1 6315 . . . . . . . . . . . . . . . . 17
148147fveq2d 5883 . . . . . . . . . . . . . . . 16
149146, 148breq12d 4408 . . . . . . . . . . . . . . 15
150145, 149imbi12d 327 . . . . . . . . . . . . . 14 ..^ ..^
1517simprrd 775 . . . . . . . . . . . . . . 15 ..^
152151r19.21bi 2776 . . . . . . . . . . . . . 14 ..^
153143, 150, 152vtocl 3086 . . . . . . . . . . . . 13 ..^
154142, 100, 153syl2anc 673 . . . . . . . . . . . 12
1551143ad2ant2 1052 . . . . . . . . . . . 12
156154, 155breqtrd 4420 . . . . . . . . . . 11
157 simp3 1032 . . . . . . . . . . 11
158156, 157breqtrd 4420 . . . . . . . . . 10
159139leidd 10201 . . . . . . . . . . . . . 14
160159adantr 472 . . . . . . . . . . . . 13
16137eqcomd 2477 . . . . . . . . . . . . 13
162160, 161breqtrd 4420 . . . . . . . . . . . 12
1631623adant2 1049 . . . . . . . . . . 11
164113eqcomd 2477 . . . . . . . . . . . . 13
165164fveq2d 5883 . . . . . . . . . . . 12
1661653ad2ant2 1052 . . . . . . . . . . 11
167163, 166breqtrd 4420 . . . . . . . . . 10
168110, 119, 141, 158, 167eliocd 37701 . . . . . . . . 9
169146, 148oveq12d 6326 . . . . . . . . . . 11
170169eleq2d 2534 . . . . . . . . . 10
171170rspcev 3136 . . . . . . . . 9 ..^ ..^
172100, 168, 171syl2anc 673 . . . . . . . 8 ..^
1731723exp 1230 . . . . . . 7 ..^
174173adantr 472 . . . . . 6 ..^
175174rexlimdv 2870 . . . . 5 ..^
17615, 175mpd 15 . . . 4 ..^
1773adantr 472 . . . . . 6
178101adantr 472 . . . . . 6
179 iocssicc 11747 . . . . . . . 8
18032simprd 470 . . . . . . . . . 10
18133, 180oveq12d 6326 . . . . . . . . 9
18275, 181eleqtrrd 2552 . . . . . . . 8
183179, 182sseldi 3416 . . . . . . 7
184183adantr 472 . . . . . 6
185 simpr 468 . . . . . 6
186 fveq2 5879 . . . . . . . . 9
187186breq1d 4405 . . . . . . . 8
188187cbvrabv 3030 . . . . . . 7 ..^ ..^
189188supeq1i 7979 . . . . . 6 ..^ ..^
190177, 178, 184, 185, 189fourierdlem25 38106 . . . . 5 ..^
191 ioossioc 37684 . . . . . . . 8
192191a1i 11 . . . . . . 7 ..^
193192sseld 3417 . . . . . 6 ..^
194193reximdva 2858 . . . . 5 ..^ ..^
195190, 194mpd 15 . . . 4 ..^
196176, 195pm2.61dan 808 . . 3 ..^
197101adantr 472 . . . . . . . . 9 ..^
198 elfzofz 11962 . . . . . . . . . 10 ..^
199198adantl 473 . . . . . . . . 9 ..^
200197, 199ffvelrnd 6038 . . . . . . . 8 ..^
2012003adant3 1050 . . . . . . 7 ..^
2021363ad2ant1 1051 . . . . . . 7 ..^
203201, 202resubcld 10068 . . . . . 6 ..^
2041393ad2ant1 1051 . . . . . . . 8 ..^
205201rexrd 9708 . . . . . . . . 9 ..^
206 fzofzp1 12037 . . . . . . . . . . . . 13 ..^
207206adantl 473 . . . . . . . . . . . 12 ..^
208197, 207ffvelrnd 6038 . . . . . . . . . . 11 ..^
209208rexrd 9708 . . . . . . . . . 10 ..^
2102093adant3 1050 . . . . . . . . 9 ..^
211 simp3 1032 . . . . . . . . 9 ..^
212 iocgtlb 37695 . . . . . . . . 9
213205, 210, 211, 212syl3anc 1292 . . . . . . . 8 ..^
214201, 204, 202, 213ltsub1dd 10246 . . . . . . 7 ..^
215138oveq1d 6323 . . . . . . . . 9
21674recnd 9687 . . . . . . . . . 10
217136recnd 9687 . . . . . . . . . 10
218216, 217pncand 10006 . . . . . . . . 9
219215, 218eqtrd 2505 . . . . . . . 8
2202193ad2ant1 1051 . . . . . . 7 ..^
221214, 220breqtrd 4420 . . . . . 6 ..^
222 elioore 11691 . . . . . . . . . . 11
223135oveq2d 6324 . . . . . . . . . . . . . 14
224133recnd 9687 . . . . . . . . . . . . . . 15
22552recnd 9687 . . . . . . . . . . . . . . 15
226224, 225mulneg1d 10092 . . . . . . . . . . . . . 14
227223, 226oveq12d 6326 . . . . . . . . . . . . 13
228227adantr 472 . . . . . . . . . . . 12
229 simpr 468 . . . . . . . . . . . . . . 15
230134adantr 472 . . . . . . . . . . . . . . 15
231229, 230readdcld 9688 . . . . . . . . . . . . . 14
232231recnd 9687 . . . . . . . . . . . . 13
233230recnd 9687 . . . . . . . . . . . . 13
234232, 233negsubd 10011 . . . . . . . . . . . 12
235229recnd 9687 . . . . . . . . . . . . 13
236235, 233pncand 10006 . . . . . . . . . . . 12
237228, 234, 2363eqtrrd 2510 . . . . . . . . . . 11
238222, 237sylan2 482 . . . . . . . . . 10
2392383ad2antl1 1192 . . . . . . . . 9 ..^
240 simpl1 1033 . . . . . . . . . 10 ..^
241 fourierdlem41.qssd . . . . . . . . . . . . 13 ..^
2422413adant3 1050 . . . . . . . . . . . 12 ..^
243242adantr 472 . . . . . . . . . . 11 ..^
244205adantr 472 . . . . . . . . . . . 12 ..^
245210adantr 472 . . . . . . . . . . . 12 ..^
246222adantl 473 . . . . . . . . . . . . . 14
247136adantr 472 . . . . . . . . . . . . . 14
248246, 247readdcld 9688 . . . . . . . . . . . . 13
2492483ad2antl1 1192 . . . . . . . . . . . 12 ..^
250136adantr 472 . . . . . . . . . . . . . . . . . 18 ..^
251200, 250resubcld 10068 . . . . . . . . . . . . . . . . 17 ..^
252251rexrd 9708 . . . . . . . . . . . . . . . 16 ..^
253252adantr 472 . . . . . . . . . . . . . . 15 ..^
25474rexrd 9708 . . . . . . . . . . . . . . . 16
255254ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
256 simpr 468 . . . . . . . . . . . . . . 15 ..^
257 ioogtlb 37688 . . . . . . . . . . . . . . 15
258253, 255, 256, 257syl3anc 1292 . . . . . . . . . . . . . 14 ..^
259200adantr 472 . . . . . . . . . . . . . . 15 ..^
260136ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
261222adantl 473 . . . . . . . . . . . . . . 15 ..^
262259, 260, 261ltsubaddd 10230 . . . . . . . . . . . . . 14 ..^
263258, 262mpbid 215 . . . . . . . . . . . . 13 ..^
2642633adantl3 1188 . . . . . . . . . . . 12 ..^
265240, 139syl 17 . . . . . . . . . . . . 13 ..^
266208adantr 472 . . . . . . . . . . . . . 14 ..^
2672663adantl3 1188 . . . . . . . . . . . . 13 ..^
26874ad2antrr 740 . . . . . . . . . . . . . . . 16 ..^
269 iooltub 37706 . . . . . . . . . . . . . . . . 17
270253, 255, 256, 269syl3anc 1292 . . . . . . . . . . . . . . . 16 ..^
271261, 268, 260, 270ltadd1dd 10245 . . . . . . . . . . . . . . 15 ..^
272138eqcomd 2477 . . . . . . . . . . . . . . . 16
273272ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
274271, 273breqtrd 4420 . . . . . . . . . . . . . 14 ..^
2752743adantl3 1188 . . . . . . . . . . . . 13 ..^
276 iocleub 37696 . . . . . . . . . . . . . . 15
277205, 210, 211, 276syl3anc 1292 . . . . . . . . . . . . . 14 ..^
278277adantr 472 . . . . . . . . . . . . 13 ..^
279249, 265, 267, 275, 278ltletrd 9812 . . . . . . . . . . . 12 ..^
280244, 245, 249, 264, 279eliood 37691 . . . . . . . . . . 11 ..^
281243, 280sseldd 3419 . . . . . . . . . 10 ..^
282240, 131syl 17 . . . . . . . . . . . 12 ..^
283282flcld 12067 . . . . . . . . . . 11 ..^
284283znegcld 11065 . . . . . . . . . 10 ..^
285 negex 9893 . . . . . . . . . . 11
286 eleq1 2537 . . . . . . . . . . . . 13
2872863anbi3d 1371 . . . . . . . . . . . 12
288 oveq1 6315 . . . . . . . . . . . . . 14
289288oveq2d 6324 . . . . . . . . . . . . 13
290289eleq1d 2533 . . . . . . . . . . . 12
291287, 290imbi12d 327 . . . . . . . . . . 11
292 ovex 6336 . . . . . . . . . . . 12
293 eleq1 2537 . . . . . . . . . . . . . 14
2942933anbi2d 1370 . . . . . . . . . . . . 13
295 oveq1 6315 . . . . . . . . . . . . . 14
296295eleq1d 2533 . . . . . . . . . . . . 13
297294, 296imbi12d 327 . . . . . . . . . . . 12
298 fourierdlem41.dper . . . . . . . . . . . 12
299292, 297, 298vtocl 3086 . . . . . . . . . . 11
300285, 291, 299vtocl 3086 . . . . . . . . . 10
301240, 281, 284, 300syl3anc 1292 . . . . . . . . 9 ..^
302239, 301eqeltrd 2549 . . . . . . . 8 ..^
303302ralrimiva 2809 . . . . . . 7 ..^
304 dfss3 3408 . . . . . . 7
305303, 304sylibr 217 . . . . . 6 ..^
306 breq1 4398 . . . . . . . 8
307 oveq1 6315 . . . . . . . . 9
308307sseq1d 3445 . . . . . . . 8
309306, 308anbi12d 725 . . . . . . 7
310309rspcev 3136 . . . . . 6
311203, 221, 305, 310syl12anc 1290 . . . . 5 ..^
3123113exp 1230 . . . 4 ..^
313312rexlimdv 2870 . . 3 ..^
314196, 313mpd 15 . 2
315 0zd 10973 . . . . . . . . . 10
3163nnzd 11062 . . . . . . . . . 10
317 1zzd 10992 . . . . . . . . . 10
318315, 316, 3173jca 1210 . . . . . . . . 9
319 0le1 10158 . . . . . . . . . 10
320319a1i 11 . . . . . . . . 9
3213nnge1d 10674 . . . . . . . . 9
322318, 320, 321jca32 544 . . . . . . . 8
323 elfz2 11817 . . . . . . . 8
324322, 323sylibr 217 . . . . . . 7
325101, 324ffvelrnd 6038 . . . . . 6
326136, 52resubcld 10068 . . . . . 6
327325, 326resubcld 10068 . . . . 5
328327adantr 472 . . . 4
32938recnd 9687 . . . . . . . . . 10
330329, 225pncand 10006 . . . . . . . . 9
331330adantr 472 . . . . . . . 8
33243oveq2i 6319 . . . . . . . . . . 11
333332a1i 11 . . . . . . . . . 10
33440recnd 9687 . . . . . . . . . . . 12
335329, 334pncan3d 10008 . . . . . . . . . . 11
336335adantr 472 . . . . . . . . . 10
337 id 22 . . . . . . . . . . . 12
338337eqcomd 2477 . . . . . . . . . . 11
339338adantl 473 . . . . . . . . . 10
340333, 336, 3393eqtrrd 2510 . . . . . . . . 9
341340oveq1d 6323 . . . . . . . 8
34233adantr 472 . . . . . . . 8
343331, 341, 3423eqtr4rd 2516 . . . . . . 7
344343oveq1d 6323 . . . . . 6
345139recnd 9687 . . . . . . . 8
346345, 217, 225nnncan2d 10040 . . . . . . 7
347346adantr 472 . . . . . 6
348219adantr 472 . . . . . 6
349344, 347, 3483eqtrrd 2510 . . . . 5
35033, 38eqeltrd 2549 . . . . . . 7
3513nngt0d 10675 . . . . . . . . . 10
352 fzolb 11953 . . . . . . . . . 10 ..^
353315, 316, 351, 352syl3anbrc 1214 . . . . . . . . 9 ..^
354 0re 9661 . . . . . . . . . 10
355 eleq1 2537 . . . . . . . . . . . . 13 ..^ ..^
356355anbi2d 718 . . . . . . . . . . . 12 ..^ ..^
357 fveq2 5879 . . . . . . . . . . . . 13
358 oveq1 6315 . . . . . . . . . . . . . 14
359358fveq2d 5883 . . . . . . . . . . . . 13
360357, 359breq12d 4408 . . . . . . . . . . . 12
361356, 360imbi12d 327 . . . . . . . . . . 11 ..^ ..^
362361, 152vtoclg 3093 . . . . . . . . . 10 ..^
363354, 362ax-mp 5 . . . . . . . . 9 ..^
364353, 363mpdan 681 . . . . . . . 8
365 0p1e1 10743 . . . . . . . . . 10
366365fveq2i 5882 . . . . . . . . 9
367366a1i 11 . . . . . . . 8
368364, 367breqtrd 4420 . . . . . . 7
369350, 325, 326, 368ltsub1dd 10246 . . . . . 6
370369adantr 472 . . . . 5
371349, 370eqbrtrd 4416 . . . 4
372 elioore 11691 . . . . . . . . 9
373135eqcomd 2477 . . . . . . . . . . . . . . . 16
374373negeqd 9889 . . . . . . . . . . . . . . 15
375226, 374eqtrd 2505 . . . . . . . . . . . . . 14
376225mulid2d 9679 . . . . . . . . . . . . . 14
377375, 376oveq12d 6326 . . . . . . . . . . . . 13
378224negcld 9992 . . . . . . . . . . . . . 14
379 1cnd 9677 . . . . . . . . . . . . . 14
380378, 379, 225adddird 9686 . . . . . . . . . . . . 13
381217, 225negsubdid 10020 . . . . . . . . . . . . 13
382377, 380, 3813eqtr4d 2515 . . . . . . . . . . . 12
383382oveq2d 6324 . . . . . . . . . . 11
384383adantr 472 . . . . . . . . . 10
385326adantr 472 . . . . . . . . . . . . 13
386229, 385readdcld 9688 . . . . . . . . . . . 12
387386recnd 9687 . . . . . . . . . . 11
388385recnd 9687 . . . . . . . . . . 11
389387, 388negsubd 10011 . . . . . . . . . 10
390235, 388pncand 10006 . . . . . . . . . 10
391384, 389, 3903eqtrrd 2510 . . . . . . . . 9
392372, 391sylan2 482 . . . . . . . 8
393392adantlr 729 . . . . . . 7
394 simpll 768 . . . . . . . 8
395367eqcomd 2477 . . . . . . . . . . . 12
396395oveq2d 6324 . . . . . . . . . . 11
397357, 359oveq12d 6326 . . . . . . . . . . . . . . . 16
398397sseq1d 3445 . . . . . . . . . . . . . . 15
399356, 398imbi12d 327 . . . . . . . . . . . . . 14 ..^ ..^
400399, 241vtoclg 3093 . . . . . . . . . . . . 13 ..^
401354, 400ax-mp 5 . . . . . . . . . . . 12 ..^
402353, 401mpdan 681 . . . . . . . . . . 11
403396, 402eqsstrd 3452 . . . . . . . . . 10
404403ad2antrr 740 . . . . . . . . 9
40533, 39eqeltrd 2549 . . . . . . . . . . 11
406405ad2antrr 740 . . . . . . . . . 10
407325rexrd 9708 . . . . . . . . . . 11
408407ad2antrr 740 . . . . . . . . . 10
409372, 386sylan2 482 . . . . . . . . . . 11
410409adantlr 729 . . . . . . . . . 10
411345, 216, 217subaddd 10023 . . . . . . . . . . . . . . . . 17
412272, 411mpbird 240 . . . . . . . . . . . . . . . 16
413 oveq1 6315 . . . . . . . . . . . . . . . 16
414412, 413sylan9req 2526 . . . . . . . . . . . . . . 15
415414oveq1d 6323 . . . . . . . . . . . . . 14
416415oveq2d 6324 . . . . . . . . . . . . 13
417130recnd 9687 . . . . . . . . . . . . . . . 16
418216, 417, 225addsubassd 10025 . . . . . . . . . . . . . . 15
419418eqcomd 2477 . . . . . . . . . . . . . 14
420419adantr 472 . . . . . . . . . . . . 13
421334, 225, 329subsub23d 37589 . . . . . . . . . . . . . . . 16
42258, 421mpbird 240 . . . . . . . . . . . . . . 15
423216, 334pncan3d 10008 . . . . . . . . . . . . . . . 16
424423oveq1d 6323 . . . . . . . . . . . . . . 15
425422, 424, 333eqtr4d 2515 . . . . . . . . . . . . . 14
426425adantr 472 . . . . . . . . . . . . 13
427416, 420, 4263eqtrrd 2510 . . . . . . . . . . . 12
428427adantr 472 . . . . . . . . . . 11
42974adantr 472 . . . . . . . . . . . . 13
430372adantl 473 . . . . . . . . . . . . 13
431326adantr 472 . . . . . . . . . . . . 13
432254adantr 472 . . . . . . . . . . . . . 14
433327rexrd 9708 . . . . . . . . . . . . . . 15
434433adantr 472 . . . . . . . . . . . . . 14
435 simpr 468 . . . . . . . . . . . . . 14