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

Theorem fourierdlem41 31771
 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 461 . . . . . 6
2 fourierdlem41.q . . . . . . . . . . 11
3 fourierdlem41.m . . . . . . . . . . . 12
4 fourierdlem41.p . . . . . . . . . . . . 13 ..^
54fourierdlem2 31732 . . . . . . . . . . . 12 ..^
63, 5syl 16 . . . . . . . . . . 11 ..^
72, 6mpbid 210 . . . . . . . . . 10 ..^
87simpld 459 . . . . . . . . 9
9 elmapi 7452 . . . . . . . . 9
10 ffn 5737 . . . . . . . . 9
118, 9, 103syl 20 . . . . . . . 8
1211adantr 465 . . . . . . 7
13 fvelrnb 5921 . . . . . . 7
1412, 13syl 16 . . . . . 6
151, 14mpbid 210 . . . . 5
16 0zd 10888 . . . . . . . . . . . . 13
17 elfzelz 11700 . . . . . . . . . . . . . . 15
18173ad2ant2 1018 . . . . . . . . . . . . . 14
19 1zzd 10907 . . . . . . . . . . . . . 14
2018, 19zsubcld 10983 . . . . . . . . . . . . 13
21 simpll 753 . . . . . . . . . . . . . . . . 17
22 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . 21
2322anim1i 568 . . . . . . . . . . . . . . . . . . . 20
24 0red 9609 . . . . . . . . . . . . . . . . . . . . 21
2517zred 10978 . . . . . . . . . . . . . . . . . . . . . 22
2625adantr 465 . . . . . . . . . . . . . . . . . . . . 21
2724, 26eqleltd 9740 . . . . . . . . . . . . . . . . . . . 20
2823, 27mpbird 232 . . . . . . . . . . . . . . . . . . 19
2928eqcomd 2475 . . . . . . . . . . . . . . . . . 18
3029adantll 713 . . . . . . . . . . . . . . . . 17
31 fveq2 5872 . . . . . . . . . . . . . . . . . . 19
3231adantl 466 . . . . . . . . . . . . . . . . . 18
337simprld 31320 . . . . . . . . . . . . . . . . . . . 20
3433simpld 459 . . . . . . . . . . . . . . . . . . 19
3534adantr 465 . . . . . . . . . . . . . . . . . 18
36 eqidd 2468 . . . . . . . . . . . . . . . . . 18
3732, 35, 363eqtrd 2512 . . . . . . . . . . . . . . . . 17
3821, 30, 37syl2anc 661 . . . . . . . . . . . . . . . 16
39383adantl3 1154 . . . . . . . . . . . . . . 15
40 simpr 461 . . . . . . . . . . . . . . . . . . 19
41 fourierdlem41.a . . . . . . . . . . . . . . . . . . . . 21
4241rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22
43 fourierdlem41.b . . . . . . . . . . . . . . . . . . . . . . 23
4443rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22
45 fourierdlem41.altb . . . . . . . . . . . . . . . . . . . . . . . . 25
46 fourierdlem41.t . . . . . . . . . . . . . . . . . . . . . . . . 25
47 eqid 2467 . . . . . . . . . . . . . . . . . . . . . . . . 25
4841, 43, 45, 46, 47fourierdlem4 31734 . . . . . . . . . . . . . . . . . . . . . . . 24
49 fourierdlem41.e . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5049a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
51 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5243adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5352, 51resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5443, 41resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5546, 54syl5eqel 2559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5655adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
57 0red 9609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5841, 43posdifd 10151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
5945, 58mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6046eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6259, 61breqtrd 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6357, 62gtned 9731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6463adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6553, 56, 64redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6665flcld 11915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6766zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6867, 56remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
69 fourierdlem41.z . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7069fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7151, 68, 70syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7271oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7372mpteq2dva 4539 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7450, 73eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . 25
7574feq1d 5723 . . . . . . . . . . . . . . . . . . . . . . . 24
7648, 75mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23
77 fourierdlem41.x . . . . . . . . . . . . . . . . . . . . . . 23
7876, 77ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22
79 iocgtlb 31422 . . . . . . . . . . . . . . . . . . . . . 22
8042, 44, 78, 79syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21
8141, 80gtned 9731 . . . . . . . . . . . . . . . . . . . 20
8281adantr 465 . . . . . . . . . . . . . . . . . . 19
8340, 82eqnetrd 2760 . . . . . . . . . . . . . . . . . 18
8483adantr 465 . . . . . . . . . . . . . . . . 17
85843adantl2 1153 . . . . . . . . . . . . . . . 16
8685neneqd 2669 . . . . . . . . . . . . . . 15
8739, 86condan 792 . . . . . . . . . . . . . 14
88 zltlem1 10927 . . . . . . . . . . . . . . 15
8916, 18, 88syl2anc 661 . . . . . . . . . . . . . 14
9087, 89mpbid 210 . . . . . . . . . . . . 13
9116, 20, 903jca 1176 . . . . . . . . . . . 12
92 eluz2 11100 . . . . . . . . . . . 12
9391, 92sylibr 212 . . . . . . . . . . 11
94 elfzel2 11698 . . . . . . . . . . . 12
95943ad2ant2 1018 . . . . . . . . . . 11
96 1red 9623 . . . . . . . . . . . . . 14
9725, 96resubcld 9999 . . . . . . . . . . . . 13
9894zred 10978 . . . . . . . . . . . . 13
9925ltm1d 10490 . . . . . . . . . . . . 13
100 elfzle2 11702 . . . . . . . . . . . . 13
10197, 25, 98, 99, 100ltletrd 9753 . . . . . . . . . . . 12
1021013ad2ant2 1018 . . . . . . . . . . 11
10393, 95, 1023jca 1176 . . . . . . . . . 10
104 elfzo2 11812 . . . . . . . . . 10 ..^
105103, 104sylibr 212 . . . . . . . . 9 ..^
1068, 9syl 16 . . . . . . . . . . . . 13
1071063ad2ant1 1017 . . . . . . . . . . . 12
10816, 95, 203jca 1176 . . . . . . . . . . . . . 14
10997, 98, 101ltled 9744 . . . . . . . . . . . . . . 15
1101093ad2ant2 1018 . . . . . . . . . . . . . 14
111108, 90, 110jca32 535 . . . . . . . . . . . . 13
112 elfz2 11691 . . . . . . . . . . . . 13
113111, 112sylibr 212 . . . . . . . . . . . 12
114107, 113ffvelrnd 6033 . . . . . . . . . . 11
115114rexrd 9655 . . . . . . . . . 10
11625recnd 9634 . . . . . . . . . . . . . . 15
117 1cnd 9624 . . . . . . . . . . . . . . 15
118116, 117npcand 9946 . . . . . . . . . . . . . 14
119118fveq2d 5876 . . . . . . . . . . . . 13
120119adantl 466 . . . . . . . . . . . 12
121106ffvelrnda 6032 . . . . . . . . . . . . 13
122121rexrd 9655 . . . . . . . . . . . 12
123120, 122eqeltrd 2555 . . . . . . . . . . 11
1241233adant3 1016 . . . . . . . . . 10
125 id 22 . . . . . . . . . . . . . . . 16
126 fveq2 5872 . . . . . . . . . . . . . . . 16
127125, 126oveq12d 6313 . . . . . . . . . . . . . . 15
128127adantl 466 . . . . . . . . . . . . . 14
12969a1i 11 . . . . . . . . . . . . . . . . 17
130 oveq2 6303 . . . . . . . . . . . . . . . . . . . . 21
131130oveq1d 6310 . . . . . . . . . . . . . . . . . . . 20
132131fveq2d 5876 . . . . . . . . . . . . . . . . . . 19
133132oveq1d 6310 . . . . . . . . . . . . . . . . . 18
134133adantl 466 . . . . . . . . . . . . . . . . 17
13543, 77resubcld 9999 . . . . . . . . . . . . . . . . . . . . 21
136135, 55, 63redivcld 10384 . . . . . . . . . . . . . . . . . . . 20
137136flcld 11915 . . . . . . . . . . . . . . . . . . 19
138137zred 10978 . . . . . . . . . . . . . . . . . 18
139138, 55remulcld 9636 . . . . . . . . . . . . . . . . 17
140129, 134, 77, 139fvmptd 5962 . . . . . . . . . . . . . . . 16
141140, 139eqeltrd 2555 . . . . . . . . . . . . . . 15
14277, 141readdcld 9635 . . . . . . . . . . . . . 14
14350, 128, 77, 142fvmptd 5962 . . . . . . . . . . . . 13
144143, 142eqeltrd 2555 . . . . . . . . . . . 12
145144rexrd 9655 . . . . . . . . . . 11
1461453ad2ant1 1017 . . . . . . . . . 10
147 simp1 996 . . . . . . . . . . . . 13
148 ovex 6320 . . . . . . . . . . . . . 14
149 eleq1 2539 . . . . . . . . . . . . . . . . 17 ..^ ..^
150149anbi2d 703 . . . . . . . . . . . . . . . 16 ..^ ..^
151 fveq2 5872 . . . . . . . . . . . . . . . . 17
152 oveq1 6302 . . . . . . . . . . . . . . . . . 18
153152fveq2d 5876 . . . . . . . . . . . . . . . . 17
154151, 153breq12d 4466 . . . . . . . . . . . . . . . 16
155150, 154imbi12d 320 . . . . . . . . . . . . . . 15 ..^ ..^
1567simprrd 31328 . . . . . . . . . . . . . . . 16 ..^
157156r19.21bi 2836 . . . . . . . . . . . . . . 15 ..^
158155, 157vtoclg 3176 . . . . . . . . . . . . . 14 ..^
159148, 158ax-mp 5 . . . . . . . . . . . . 13 ..^
160147, 105, 159syl2anc 661 . . . . . . . . . . . 12
1611193ad2ant2 1018 . . . . . . . . . . . 12
162160, 161breqtrd 4477 . . . . . . . . . . 11
163 simp3 998 . . . . . . . . . . 11
164162, 163breqtrd 4477 . . . . . . . . . 10
165144leidd 10131 . . . . . . . . . . . . . 14
166165adantr 465 . . . . . . . . . . . . 13
16740eqcomd 2475 . . . . . . . . . . . . 13
168166, 167breqtrd 4477 . . . . . . . . . . . 12
1691683adant2 1015 . . . . . . . . . . 11
170118eqcomd 2475 . . . . . . . . . . . . 13
171170fveq2d 5876 . . . . . . . . . . . 12
1721713ad2ant2 1018 . . . . . . . . . . 11
173169, 172breqtrd 4477 . . . . . . . . . 10
174115, 124, 146, 164, 173eliocd 31430 . . . . . . . . 9
175151, 153oveq12d 6313 . . . . . . . . . . 11
176175eleq2d 2537 . . . . . . . . . 10
177176rspcev 3219 . . . . . . . . 9 ..^ ..^
178105, 174, 177syl2anc 661 . . . . . . . 8 ..^
1791783exp 1195 . . . . . . 7 ..^
180179adantr 465 . . . . . 6 ..^
181180rexlimdv 2957 . . . . 5 ..^
18215, 181mpd 15 . . . 4 ..^
1833adantr 465 . . . . . 6
184106adantr 465 . . . . . 6
185 iocssicc 11624 . . . . . . . 8
18633simprd 463 . . . . . . . . . . 11
18734, 186oveq12d 6313 . . . . . . . . . 10
188187eqcomd 2475 . . . . . . . . 9
18978, 188eleqtrd 2557 . . . . . . . 8
190185, 189sseldi 3507 . . . . . . 7
191190adantr 465 . . . . . 6
192 simpr 461 . . . . . 6
193 fveq2 5872 . . . . . . . . 9
194193breq1d 4463 . . . . . . . 8
195194cbvrabv 3117 . . . . . . 7 ..^ ..^
196195supeq1i 7919 . . . . . 6 ..^ ..^
197183, 184, 191, 192, 196fourierdlem25 31755 . . . . 5 ..^
198 ioossioc 31411 . . . . . . . 8
199198a1i 11 . . . . . . 7 ..^
200199sseld 3508 . . . . . 6 ..^
201200reximdva 2942 . . . . 5 ..^ ..^
202197, 201mpd 15 . . . 4 ..^
203182, 202pm2.61dan 789 . . 3 ..^
204106adantr 465 . . . . . . . . 9 ..^
205 elfzofz 11823 . . . . . . . . . 10 ..^
206205adantl 466 . . . . . . . . 9 ..^
207204, 206ffvelrnd 6033 . . . . . . . 8 ..^
2082073adant3 1016 . . . . . . 7 ..^
2091413ad2ant1 1017 . . . . . . 7 ..^
210208, 209resubcld 9999 . . . . . 6 ..^
2111443ad2ant1 1017 . . . . . . . . 9 ..^
212208rexrd 9655 . . . . . . . . . 10 ..^
213 fzofzp1 11889 . . . . . . . . . . . . . 14 ..^
214213adantl 466 . . . . . . . . . . . . 13 ..^
215204, 214ffvelrnd 6033 . . . . . . . . . . . 12 ..^
216215rexrd 9655 . . . . . . . . . . 11 ..^
2172163adant3 1016 . . . . . . . . . 10 ..^
218 simp3 998 . . . . . . . . . 10 ..^
219 iocgtlb 31422 . . . . . . . . . 10
220212, 217, 218, 219syl3anc 1228 . . . . . . . . 9 ..^
221208, 211, 209, 220ltsub1dd 10176 . . . . . . . 8 ..^
222143oveq1d 6310 . . . . . . . . . 10
22377recnd 9634 . . . . . . . . . . 11
224141recnd 9634 . . . . . . . . . . 11
225223, 224pncand 9943 . . . . . . . . . 10
226222, 225eqtrd 2508 . . . . . . . . 9
2272263ad2ant1 1017 . . . . . . . 8 ..^
228221, 227breqtrd 4477 . . . . . . 7 ..^
229 simpl 457 . . . . . . . . . . . 12
230 elioore 11571 . . . . . . . . . . . . 13
231230adantl 466 . . . . . . . . . . . 12
232140oveq2d 6311 . . . . . . . . . . . . . . 15
233138recnd 9634 . . . . . . . . . . . . . . . 16
23455recnd 9634 . . . . . . . . . . . . . . . 16
235233, 234mulneg1d 10021 . . . . . . . . . . . . . . 15
236232, 235oveq12d 6313 . . . . . . . . . . . . . 14
237236adantr 465 . . . . . . . . . . . . 13
238 simpr 461 . . . . . . . . . . . . . . . 16
239139adantr 465 . . . . . . . . . . . . . . . 16
240238, 239readdcld 9635 . . . . . . . . . . . . . . 15
241240recnd 9634 . . . . . . . . . . . . . 14
242239recnd 9634 . . . . . . . . . . . . . 14
243241, 242negsubd 9948 . . . . . . . . . . . . 13
244238recnd 9634 . . . . . . . . . . . . . 14
245244, 242pncand 9943 . . . . . . . . . . . . 13
246237, 243, 2453eqtrrd 2513 . . . . . . . . . . . 12
247229, 231, 246syl2anc 661 . . . . . . . . . . 11
2482473ad2antl1 1158 . . . . . . . . . 10 ..^
249 simpl1 999 . . . . . . . . . . 11 ..^
250 fourierdlem41.qssd . . . . . . . . . . . . . 14 ..^
2512503adant3 1016 . . . . . . . . . . . . 13 ..^
252251adantr 465 . . . . . . . . . . . 12 ..^
253212adantr 465 . . . . . . . . . . . . 13 ..^
254217adantr 465 . . . . . . . . . . . . 13 ..^
255141adantr 465 . . . . . . . . . . . . . . 15
256231, 255readdcld 9635 . . . . . . . . . . . . . 14
2572563ad2antl1 1158 . . . . . . . . . . . . 13 ..^
258141adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
259207, 258resubcld 9999 . . . . . . . . . . . . . . . . . 18 ..^
260259rexrd 9655 . . . . . . . . . . . . . . . . 17 ..^
261260adantr 465 . . . . . . . . . . . . . . . 16 ..^
26277rexrd 9655 . . . . . . . . . . . . . . . . 17
263262ad2antrr 725 . . . . . . . . . . . . . . . 16 ..^
264 simpr 461 . . . . . . . . . . . . . . . 16 ..^
265 ioogtlb 31415 . . . . . . . . . . . . . . . 16
266261, 263, 264, 265syl3anc 1228 . . . . . . . . . . . . . . 15 ..^
267207adantr 465 . . . . . . . . . . . . . . . 16 ..^
268255adantlr 714 . . . . . . . . . . . . . . . 16 ..^
269230adantl 466 . . . . . . . . . . . . . . . 16 ..^
270267, 268, 269ltsubaddd 10160 . . . . . . . . . . . . . . 15 ..^
271266, 270mpbid 210 . . . . . . . . . . . . . 14 ..^
2722713adantl3 1154 . . . . . . . . . . . . 13 ..^
273249, 144syl 16 . . . . . . . . . . . . . 14 ..^
274215adantr 465 . . . . . . . . . . . . . . 15 ..^
2752743adantl3 1154 . . . . . . . . . . . . . 14 ..^
27677ad2antrr 725 . . . . . . . . . . . . . . . . 17 ..^
277 iooltub 31435 . . . . . . . . . . . . . . . . . 18
278261, 263, 264, 277syl3anc 1228 . . . . . . . . . . . . . . . . 17 ..^
279269, 276, 268, 278ltadd1dd 10175 . . . . . . . . . . . . . . . 16 ..^
280143eqcomd 2475 . . . . . . . . . . . . . . . . 17
281280ad2antrr 725 . . . . . . . . . . . . . . . 16 ..^
282279, 281breqtrd 4477 . . . . . . . . . . . . . . 15 ..^
2832823adantl3 1154 . . . . . . . . . . . . . 14 ..^
284 iocleub 31423 . . . . . . . . . . . . . . . 16
285212, 217, 218, 284syl3anc 1228 . . . . . . . . . . . . . . 15 ..^
286285adantr 465 . . . . . . . . . . . . . 14 ..^
287257, 273, 275, 283, 286ltletrd 9753 . . . . . . . . . . . . 13 ..^
288253, 254, 257, 272, 287eliood 31418 . . . . . . . . . . . 12 ..^
289252, 288sseldd 3510 . . . . . . . . . . 11 ..^
290249, 136syl 16 . . . . . . . . . . . . 13 ..^
291290flcld 11915 . . . . . . . . . . . 12 ..^
292291znegcld 10980 . . . . . . . . . . 11 ..^
293 negex 9830 . . . . . . . . . . . 12
294 eleq1 2539 . . . . . . . . . . . . . . 15
2952943anbi3d 1305 . . . . . . . . . . . . . 14
296 oveq1 6302 . . . . . . . . . . . . . . . 16
297296oveq2d 6311 . . . . . . . . . . . . . . 15
298297eleq1d 2536 . . . . . . . . . . . . . 14
299295, 298imbi12d 320 . . . . . . . . . . . . 13
300 ovex 6320 . . . . . . . . . . . . . 14
301 eleq1 2539 . . . . . . . . . . . . . . . . 17
3023013anbi2d 1304 . . . . . . . . . . . . . . . 16
303 oveq1 6302 . . . . . . . . . . . . . . . . 17
304303eleq1d 2536 . . . . . . . . . . . . . . . 16
305302, 304imbi12d 320 . . . . . . . . . . . . . . 15
306 fourierdlem41.dper . . . . . . . . . . . . . . 15
307305, 306vtoclg 3176 . . . . . . . . . . . . . 14
308300, 307ax-mp 5 . . . . . . . . . . . . 13
309299, 308vtoclg 3176 . . . . . . . . . . . 12
310293, 309ax-mp 5 . . . . . . . . . . 11
311249, 289, 292, 310syl3anc 1228 . . . . . . . . . 10 ..^
312248, 311eqeltrd 2555 . . . . . . . . 9 ..^
313312ralrimiva 2881 . . . . . . . 8 ..^
314 dfss3 3499 . . . . . . . 8
315313, 314sylibr 212 . . . . . . 7 ..^
316228, 315jca 532 . . . . . 6 ..^
317 breq1 4456 . . . . . . . 8
318 oveq1 6302 . . . . . . . . 9
319318sseq1d 3536 . . . . . . . 8
320317, 319anbi12d 710 . . . . . . 7
321320rspcev 3219 . . . . . 6
322210, 316, 321syl2anc 661 . . . . 5 ..^
3233223exp 1195 . . . 4 ..^
324323rexlimdv 2957 . . 3 ..^
325203, 324mpd 15 . 2
326 0zd 10888 . . . . . . . . . 10
3273nnzd 10977 . . . . . . . . . 10
328 1zzd 10907 . . . . . . . . . 10
329326, 327, 3283jca 1176 . . . . . . . . 9
330 0le1 10088 . . . . . . . . . 10
331330a1i 11 . . . . . . . . 9
3323nnge1d 10590 . . . . . . . . 9
333329, 331, 332jca32 535 . . . . . . . 8
334 elfz2 11691 . . . . . . . 8
335333, 334sylibr 212 . . . . . . 7
336106, 335ffvelrnd 6033 . . . . . 6
337141, 55resubcld 9999 . . . . . 6
338336, 337resubcld 9999 . . . . 5
339338adantr 465 . . . 4
34034adantr 465 . . . . . . . . 9
34146oveq2i 6306 . . . . . . . . . . . . 13
342341a1i 11 . . . . . . . . . . . 12
34341recnd 9634 . . . . . . . . . . . . . 14
34443recnd 9634 . . . . . . . . . . . . . 14
345343, 344pncan3d 9945 . . . . . . . . . . . . 13
346345adantr 465 . . . . . . . . . . . 12
347 id 22 . . . . . . . . . . . . . 14
348347eqcomd 2475 . . . . . . . . . . . . 13
349348adantl 466 . . . . . . . . . . . 12
350342, 346, 3493eqtrrd 2513 . . . . . . . . . . 11
351350oveq1d 6310 . . . . . . . . . 10
352343, 234pncand 9943 . . . . . . . . . . 11
353352adantr 465 . . . . . . . . . 10
354351, 353eqtr2d 2509 . . . . . . . . 9
355 eqidd 2468 . . . . . . . . 9
356340, 354, 3553eqtrd 2512 . . . . . . . 8
357356oveq1d 6310 . . . . . . 7
358144recnd 9634 . . . . . . . . 9
359358, 224, 234nnncan2d 9977 . . . . . . . 8
360359adantr 465 . . . . . . 7
361226adantr 465 . . . . . . 7
362357, 360, 3613eqtrrd 2513 . . . . . 6
36334, 41eqeltrd 2555 . . . . . . . 8
364 id 22 . . . . . . . . . 10
3653nngt0d 10591 . . . . . . . . . . . 12
366326, 327, 3653jca 1176 . . . . . . . . . . 11
367 fzolb 11814 . . . . . . . . . . 11 ..^
368366, 367sylibr 212 . . . . . . . . . 10 ..^
369 0re 9608 . . . . . . . . . . 11
370 eleq1 2539 . . . . . . . . . . . . . 14 ..^ ..^
371370anbi2d 703 . . . . . . . . . . . . 13 ..^ ..^
372 fveq2 5872 . . . . . . . . . . . . . 14
373 oveq1 6302 . . . . . . . . . . . . . . 15
374373fveq2d 5876 . . . . . . . . . . . . . 14
375372, 374breq12d 4466 . . . . . . . . . . . . 13
376371, 375imbi12d 320 . . . . . . . . . . . 12 ..^ ..^
377376, 157vtoclg 3176 . . . . . . . . . . 11 ..^
378369, 377ax-mp 5 . . . . . . . . . 10 ..^
379364, 368, 378syl2anc 661 . . . . . . . . 9
380 0p1e1 10659 . . . . . . . . . . 11
381380fveq2i 5875 . . . . . . . . . 10
382381a1i 11 . . . . . . . . 9
383379, 382breqtrd 4477 . . . . . . . 8
384363, 336, 337, 383ltsub1dd 10176 . . . . . . 7
385384adantr 465 . . . . . 6
386362, 385eqbrtrd 4473 . . . . 5
387 simpl 457 . . . . . . . . . 10
388 elioore 11571 . . . . . . . . . . 11
389388adantl 466 . . . . . . . . . 10
390233negcld 9929 . . . . . . . . . . . . . . 15
391 1cnd 9624 . . . . . . . . . . . . . . 15
392390, 391, 234adddird 9633 . . . . . . . . . . . . . 14
393140eqcomd 2475 . . . . . . . . . . . . . . . . 17
394393negeqd 9826 . . . . . . . . . . . . . . . 16
395235, 394eqtrd 2508 . . . . . . . . . . . . . . 15
396234mulid2d 9626 . . . . . . . . . . . . . . 15
397395, 396oveq12d 6313 . . . . . . . . . . . . . 14
398224, 234negsubdid 9957 . . . . . . . . . . . . . . 15
399398eqcomd 2475 . . . . . . . . . . . . . 14
400392, 397, 3993eqtrd 2512 . . . . . . . . . . . . 13
401400oveq2d 6311 . . . . . . . . . . . 12
402401adantr 465 . . . . . . . . . . 11
403337adantr 465 . . . . . . . . . . . . . 14
404238, 403readdcld 9635 . . . . . . . . . . . . 13
405404recnd 9634 . . . . . . . . . . . 12
406403recnd 9634 . . . . . . . . . . . 12
407405, 406negsubd 9948 . . . . . . . . . . 11
408244, 406pncand 9943 . . . . . . . . . . 11
409402, 407, 4083eqtrrd 2513 . . . . . . . . . 10
410387, 389, 409syl2anc 661 . . . . . . . . 9
411410adantlr 714 . . . . . . . 8
412364ad2antrr 725 . . . . . . . . 9
413382eqcomd 2475 . . . . . . . . . . . . 13
414413oveq2d 6311 . . . . . . . . . . . 12
415372, 374oveq12d 6313 . . . . . . . . . . . . . . . . 17
416415sseq1d 3536 . . . . . . . . . . . . . . . 16
417371, 416imbi12d 320 . . . . . . . . . . . . . . 15 ..^ ..^
418417, 250vtoclg 3176 . . . . . . . . . . . . . 14 ..^
419369, 418ax-mp 5 . . . . . . . . . . . . 13 ..^
420364, 368, 419syl2anc 661 . . . . . . . . . . . 12
421414, 420eqsstrd 3543 . . . . . . . . . . 11
422421ad2antrr 725 . . . . . . . . . 10
42334, 42eqeltrd 2555 . . . . . . . . . . . 12
424423ad2antrr 725 . . . . . . . . . . 11
425336rexrd 9655 . . . . . . . . . . . 12
426425ad2antrr 725 . . . . . . . . . . 11
427389, 404syldan 470 . . . . . . . . . . . 12
428427adantlr 714 . . . . . . . . . . 11
429358, 223, 224subaddd 9960 . . . . . . . . . . . . . . . . . . . 20
430280, 429mpbird 232 . . . . . . . . . . . . . . . . . . 19
431430eqcomd 2475 . . . . . . . . . . . . . . . . . 18
432431adantr 465 . . . . . . . . . . . . . . . . 17
433 oveq1 6302 . . . . . . . . . . . . . . . . . 18