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

Theorem fourierdlem64 38146
 Description: The partition is finer than , when is moved on the same interval where lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem64.t
fourierdlem64.p ..^
fourierdlem64.m
fourierdlem64.q
fourierdlem64.c
fourierdlem64.d
fourierdlem64.cltd
fourierdlem64.h
fourierdlem64.n
fourierdlem64.v
fourierdlem64.j ..^
fourierdlem64.l
fourierdlem64.i ..^
Assertion
Ref Expression
fourierdlem64 ..^ ..^
Distinct variable groups:   ,,,   ,,,   ,,   ,   ,,   ,   ,   ,   ,   ,,,   ,,   ,,   ,,   ,,   ,,   ,   ,   ,,   ,,,   ,   ,,,   ,   ,   ,,   ,,   ,   ,   ,,   ,,   ,   ,,   ,   ,,   ,   ,   ,   ,,   ,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,,,,)   (,)   (,,)   (,,,,)   (,,)   (,,,)   (,,,)   (,,)   (,)   ()

Proof of Theorem fourierdlem64
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem64.i . . 3 ..^
2 ssrab2 3500 . . . 4 ..^ ..^
3 fzossfz 11965 . . . . . . . 8 ..^
4 fzssz 11827 . . . . . . . 8
53, 4sstri 3427 . . . . . . 7 ..^
62, 5sstri 3427 . . . . . 6 ..^
76a1i 11 . . . . 5 ..^
8 0zd 10973 . . . . . . . 8
9 fourierdlem64.m . . . . . . . . 9
109nnzd 11062 . . . . . . . 8
119nngt0d 10675 . . . . . . . 8
12 fzolb 11953 . . . . . . . 8 ..^
138, 10, 11, 12syl3anbrc 1214 . . . . . . 7 ..^
14 fourierdlem64.l . . . . . . . . . 10
15 ssrab2 3500 . . . . . . . . . . . 12
1615a1i 11 . . . . . . . . . . 11
17 fourierdlem64.h . . . . . . . . . . . . . . . . . . 19
18 fourierdlem64.c . . . . . . . . . . . . . . . . . . . . 21
19 fourierdlem64.d . . . . . . . . . . . . . . . . . . . . 21
20 prssi 4119 . . . . . . . . . . . . . . . . . . . . 21
2118, 19, 20syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
22 ssrab2 3500 . . . . . . . . . . . . . . . . . . . . . 22
2322a1i 11 . . . . . . . . . . . . . . . . . . . . 21
2418, 19iccssred 37698 . . . . . . . . . . . . . . . . . . . . 21
2523, 24sstrd 3428 . . . . . . . . . . . . . . . . . . . 20
2621, 25unssd 3601 . . . . . . . . . . . . . . . . . . 19
2717, 26syl5eqss 3462 . . . . . . . . . . . . . . . . . 18
28 fourierdlem64.t . . . . . . . . . . . . . . . . . . . . . 22
29 fourierdlem64.p . . . . . . . . . . . . . . . . . . . . . 22 ..^
30 fourierdlem64.q . . . . . . . . . . . . . . . . . . . . . 22
31 fourierdlem64.cltd . . . . . . . . . . . . . . . . . . . . . 22
32 eqid 2471 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
33 fourierdlem64.n . . . . . . . . . . . . . . . . . . . . . 22
34 fourierdlem64.v . . . . . . . . . . . . . . . . . . . . . 22
3528, 29, 9, 30, 18, 19, 31, 32, 17, 33, 34fourierdlem54 38136 . . . . . . . . . . . . . . . . . . . . 21 ..^
3635simprd 470 . . . . . . . . . . . . . . . . . . . 20
37 isof1o 6234 . . . . . . . . . . . . . . . . . . . 20
38 f1of 5828 . . . . . . . . . . . . . . . . . . . 20
3936, 37, 383syl 18 . . . . . . . . . . . . . . . . . . 19
40 fourierdlem64.j . . . . . . . . . . . . . . . . . . . 20 ..^
41 elfzofz 11962 . . . . . . . . . . . . . . . . . . . 20 ..^
4240, 41syl 17 . . . . . . . . . . . . . . . . . . 19
4339, 42ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18
4427, 43sseldd 3419 . . . . . . . . . . . . . . . . 17
4529fourierdlem2 38083 . . . . . . . . . . . . . . . . . . . . . 22 ..^
469, 45syl 17 . . . . . . . . . . . . . . . . . . . . 21 ..^
4730, 46mpbid 215 . . . . . . . . . . . . . . . . . . . 20 ..^
4847simpld 466 . . . . . . . . . . . . . . . . . . 19
49 elmapi 7511 . . . . . . . . . . . . . . . . . . 19
5048, 49syl 17 . . . . . . . . . . . . . . . . . 18
519nnnn0d 10949 . . . . . . . . . . . . . . . . . . . 20
52 nn0uz 11217 . . . . . . . . . . . . . . . . . . . 20
5351, 52syl6eleq 2559 . . . . . . . . . . . . . . . . . . 19
54 eluzfz1 11832 . . . . . . . . . . . . . . . . . . 19
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18
5650, 55ffvelrnd 6038 . . . . . . . . . . . . . . . . 17
5744, 56resubcld 10068 . . . . . . . . . . . . . . . 16
5829, 9, 30fourierdlem11 38092 . . . . . . . . . . . . . . . . . . 19
5958simp2d 1043 . . . . . . . . . . . . . . . . . 18
6058simp1d 1042 . . . . . . . . . . . . . . . . . 18
6159, 60resubcld 10068 . . . . . . . . . . . . . . . . 17
6228, 61syl5eqel 2553 . . . . . . . . . . . . . . . 16
6358simp3d 1044 . . . . . . . . . . . . . . . . . . 19
6460, 59posdifd 10221 . . . . . . . . . . . . . . . . . . 19
6563, 64mpbid 215 . . . . . . . . . . . . . . . . . 18
6665, 28syl6breqr 4436 . . . . . . . . . . . . . . . . 17
6766gt0ne0d 10199 . . . . . . . . . . . . . . . 16
6857, 62, 67redivcld 10457 . . . . . . . . . . . . . . 15
69 btwnz 11060 . . . . . . . . . . . . . . 15
7068, 69syl 17 . . . . . . . . . . . . . 14
7170simpld 466 . . . . . . . . . . . . 13
72 zre 10965 . . . . . . . . . . . . . . 15
7356ad2antrr 740 . . . . . . . . . . . . . . . . . 18
74 simplr 770 . . . . . . . . . . . . . . . . . . 19
7562ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
7674, 75remulcld 9689 . . . . . . . . . . . . . . . . . 18
7773, 76readdcld 9688 . . . . . . . . . . . . . . . . 17
7844ad2antrr 740 . . . . . . . . . . . . . . . . 17
79 simpr 468 . . . . . . . . . . . . . . . . . . 19
8057ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
8162, 66elrpd 11361 . . . . . . . . . . . . . . . . . . . . 21
8281ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
8374, 80, 82ltmuldivd 11408 . . . . . . . . . . . . . . . . . . 19
8479, 83mpbird 240 . . . . . . . . . . . . . . . . . 18
8556adantr 472 . . . . . . . . . . . . . . . . . . . 20
86 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
8762adantr 472 . . . . . . . . . . . . . . . . . . . . 21
8886, 87remulcld 9689 . . . . . . . . . . . . . . . . . . . 20
8944adantr 472 . . . . . . . . . . . . . . . . . . . 20
9085, 88, 89ltaddsub2d 10235 . . . . . . . . . . . . . . . . . . 19
9190adantr 472 . . . . . . . . . . . . . . . . . 18
9284, 91mpbird 240 . . . . . . . . . . . . . . . . 17
9377, 78, 92ltled 9800 . . . . . . . . . . . . . . . 16
9493ex 441 . . . . . . . . . . . . . . 15
9572, 94sylan2 482 . . . . . . . . . . . . . 14
9695reximdva 2858 . . . . . . . . . . . . 13
9771, 96mpd 15 . . . . . . . . . . . 12
98 rabn0 3755 . . . . . . . . . . . 12
9997, 98sylibr 217 . . . . . . . . . . 11
100 simpl 464 . . . . . . . . . . . . . 14
10116sselda 3418 . . . . . . . . . . . . . 14
102 oveq1 6315 . . . . . . . . . . . . . . . . . . 19
103102oveq2d 6324 . . . . . . . . . . . . . . . . . 18
104103breq1d 4405 . . . . . . . . . . . . . . . . 17
105104elrab 3184 . . . . . . . . . . . . . . . 16
106105simprbi 471 . . . . . . . . . . . . . . 15
107106adantl 473 . . . . . . . . . . . . . 14
108 zre 10965 . . . . . . . . . . . . . . 15
109 simpr 468 . . . . . . . . . . . . . . . . 17
11056ad2antrr 740 . . . . . . . . . . . . . . . . . 18
111 simpr 468 . . . . . . . . . . . . . . . . . . . 20
11262adantr 472 . . . . . . . . . . . . . . . . . . . 20
113111, 112remulcld 9689 . . . . . . . . . . . . . . . . . . 19
114113adantr 472 . . . . . . . . . . . . . . . . . 18
11544ad2antrr 740 . . . . . . . . . . . . . . . . . 18
116110, 114, 115leaddsub2d 10236 . . . . . . . . . . . . . . . . 17
117109, 116mpbid 215 . . . . . . . . . . . . . . . 16
118 simplr 770 . . . . . . . . . . . . . . . . 17
11957ad2antrr 740 . . . . . . . . . . . . . . . . 17
12081ad2antrr 740 . . . . . . . . . . . . . . . . 17
121118, 119, 120lemuldivd 11410 . . . . . . . . . . . . . . . 16
122117, 121mpbid 215 . . . . . . . . . . . . . . 15
123108, 122sylanl2 663 . . . . . . . . . . . . . 14
124100, 101, 107, 123syl21anc 1291 . . . . . . . . . . . . 13
125124ralrimiva 2809 . . . . . . . . . . . 12
126 breq2 4399 . . . . . . . . . . . . . 14
127126ralbidv 2829 . . . . . . . . . . . . 13
128127rspcev 3136 . . . . . . . . . . . 12
12968, 125, 128syl2anc 673 . . . . . . . . . . 11
130 suprzcl 11038 . . . . . . . . . . 11
13116, 99, 129, 130syl3anc 1292 . . . . . . . . . 10
13214, 131syl5eqel 2553 . . . . . . . . 9
133 oveq1 6315 . . . . . . . . . . . 12
134133oveq2d 6324 . . . . . . . . . . 11
135134breq1d 4405 . . . . . . . . . 10
136135elrab 3184 . . . . . . . . 9
137132, 136sylib 201 . . . . . . . 8
138137simprd 470 . . . . . . 7
139 fveq2 5879 . . . . . . . . . 10
140139oveq1d 6323 . . . . . . . . 9
141140breq1d 4405 . . . . . . . 8
142141elrab 3184 . . . . . . 7 ..^ ..^
14313, 138, 142sylanbrc 677 . . . . . 6 ..^
144 ne0i 3728 . . . . . 6 ..^ ..^
145143, 144syl 17 . . . . 5 ..^
1469nnred 10646 . . . . . 6
1472a1i 11 . . . . . . . . 9 ..^ ..^
148147sselda 3418 . . . . . . . 8 ..^ ..^
149 elfzoelz 11947 . . . . . . . . . . 11 ..^
150149zred 11063 . . . . . . . . . 10 ..^
151150adantl 473 . . . . . . . . 9 ..^
152146adantr 472 . . . . . . . . 9 ..^
153 elfzolt2 11956 . . . . . . . . . 10 ..^
154153adantl 473 . . . . . . . . 9 ..^
155151, 152, 154ltled 9800 . . . . . . . 8 ..^
156148, 155syldan 478 . . . . . . 7 ..^
157156ralrimiva 2809 . . . . . 6 ..^
158 breq2 4399 . . . . . . . 8
159158ralbidv 2829 . . . . . . 7 ..^ ..^
160159rspcev 3136 . . . . . 6 ..^ ..^
161146, 157, 160syl2anc 673 . . . . 5 ..^
162 suprzcl 11038 . . . . 5 ..^ ..^ ..^ ..^ ..^
1637, 145, 161, 162syl3anc 1292 . . . 4 ..^ ..^
1642, 163sseldi 3416 . . 3 ..^ ..^
1651, 164syl5eqel 2553 . 2 ..^
16615, 131sseldi 3416 . . 3
16714, 166syl5eqel 2553 . 2
1683, 165sseldi 3416 . . . . . . . . . 10
16950, 168ffvelrnd 6038 . . . . . . . . 9
170167zred 11063 . . . . . . . . . 10
171170, 62remulcld 9689 . . . . . . . . 9
172169, 171readdcld 9688 . . . . . . . 8
173172rexrd 9708 . . . . . . 7
174173adantr 472 . . . . . 6
175 fzofzp1 12037 . . . . . . . . . . 11 ..^
176165, 175syl 17 . . . . . . . . . 10
17750, 176ffvelrnd 6038 . . . . . . . . 9
178177, 171readdcld 9688 . . . . . . . 8
179178rexrd 9708 . . . . . . 7
180179adantr 472 . . . . . 6
181 elioore 11691 . . . . . . 7
182181adantl 473 . . . . . 6
183172adantr 472 . . . . . . 7
18444adantr 472 . . . . . . 7
1851, 163syl5eqel 2553 . . . . . . . . . 10 ..^
186 fveq2 5879 . . . . . . . . . . . . 13
187186oveq1d 6323 . . . . . . . . . . . 12
188187breq1d 4405 . . . . . . . . . . 11
189188elrab 3184 . . . . . . . . . 10 ..^ ..^
190185, 189sylib 201 . . . . . . . . 9 ..^
191190simprd 470 . . . . . . . 8
192191adantr 472 . . . . . . 7
193184rexrd 9708 . . . . . . . 8
194 fzofzp1 12037 . . . . . . . . . . . . 13 ..^
19540, 194syl 17 . . . . . . . . . . . 12
19639, 195ffvelrnd 6038 . . . . . . . . . . 11
19727, 196sseldd 3419 . . . . . . . . . 10
198197rexrd 9708 . . . . . . . . 9
199198adantr 472 . . . . . . . 8
200 simpr 468 . . . . . . . 8
201 ioogtlb 37688 . . . . . . . 8
202193, 199, 200, 201syl3anc 1292 . . . . . . 7
203183, 184, 182, 192, 202lelttrd 9810 . . . . . 6
204 zssre 10968 . . . . . . . . . . . . . . . 16
20515, 204sstri 3427 . . . . . . . . . . . . . . 15
206205a1i 11 . . . . . . . . . . . . . 14
20799ad2antrr 740 . . . . . . . . . . . . . 14
208129ad2antrr 740 . . . . . . . . . . . . . 14
209167peano2zd 11066 . . . . . . . . . . . . . . . 16
210209ad2antrr 740 . . . . . . . . . . . . . . 15
211 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23
212146recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . 24
213 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . 24
214212, 213npcand 10009 . . . . . . . . . . . . . . . . . . . . . . 23
215211, 214sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . . . 22
216215fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21
21747simprd 470 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
218217simpld 466 . . . . . . . . . . . . . . . . . . . . . . 23
219218simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
220219adantr 472 . . . . . . . . . . . . . . . . . . . . 21
22159recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . 25
22260recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . 25
223221, 222npcand 10009 . . . . . . . . . . . . . . . . . . . . . . . 24
224223eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . 23
22528eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . 25
226225a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
227226oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23
228218simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
229228eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24
230229oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23
231224, 227, 2303eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . 22
232231adantr 472 . . . . . . . . . . . . . . . . . . . . 21
233216, 220, 2323eqtrd 2509 . . . . . . . . . . . . . . . . . . . 20
23462recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22
235228, 222eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . 22
236234, 235addcomd 9853 . . . . . . . . . . . . . . . . . . . . 21
237236adantr 472 . . . . . . . . . . . . . . . . . . . 20
238233, 237eqtrd 2505 . . . . . . . . . . . . . . . . . . 19
239238oveq1d 6323 . . . . . . . . . . . . . . . . . 18
240171recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
241235, 234, 240addassd 9683 . . . . . . . . . . . . . . . . . . . 20
242234mulid2d 9679 . . . . . . . . . . . . . . . . . . . . . . . 24
243242, 234eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . 23
244243, 240addcomd 9853 . . . . . . . . . . . . . . . . . . . . . 22
245242eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . 23
246245oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 22
247170recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
248247, 213, 234adddird 9686 . . . . . . . . . . . . . . . . . . . . . 22
249244, 246, 2483eqtr4d 2515 . . . . . . . . . . . . . . . . . . . . 21
250249oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20
251241, 250eqtrd 2505 . . . . . . . . . . . . . . . . . . 19
252251adantr 472 . . . . . . . . . . . . . . . . . 18
253239, 252eqtr2d 2506 . . . . . . . . . . . . . . . . 17
254253adantr 472 . . . . . . . . . . . . . . . 16
255 simpr 468 . . . . . . . . . . . . . . . 16
256254, 255eqbrtrd 4416 . . . . . . . . . . . . . . 15
257 oveq1 6315 . . . . . . . . . . . . . . . . . 18
258257oveq2d 6324 . . . . . . . . . . . . . . . . 17
259258breq1d 4405 . . . . . . . . . . . . . . . 16
260259elrab 3184 . . . . . . . . . . . . . . 15
261210, 256, 260sylanbrc 677 . . . . . . . . . . . . . 14
262 suprub 10592 . . . . . . . . . . . . . 14
263206, 207, 208, 261, 262syl31anc 1295 . . . . . . . . . . . . 13
264263, 14syl6breqr 4436 . . . . . . . . . . . 12
265170ltp1d 10559 . . . . . . . . . . . . . 14
266 peano2re 9824 . . . . . . . . . . . . . . . 16
267170, 266syl 17 . . . . . . . . . . . . . . 15
268170, 267ltnled 9799 . . . . . . . . . . . . . 14
269265, 268mpbid 215 . . . . . . . . . . . . 13
270269ad2antrr 740 . . . . . . . . . . . 12
271264, 270pm2.65da 586 . . . . . . . . . . 11
2725, 165sseldi 3416 . . . . . . . . . . . . . . 15
273272zred 11063 . . . . . . . . . . . . . 14
274273adantr 472 . . . . . . . . . . . . 13
275 peano2rem 9961 . . . . . . . . . . . . . . 15
276146, 275syl 17 . . . . . . . . . . . . . 14
277276adantr 472 . . . . . . . . . . . . 13
278 elfzolt2 11956 . . . . . . . . . . . . . . . 16 ..^
279 elfzoelz 11947 . . . . . . . . . . . . . . . . 17 ..^
280 elfzoel2 11946 . . . . . . . . . . . . . . . . 17 ..^
281 zltlem1 11013 . . . . . . . . . . . . . . . . 17
282279, 280, 281syl2anc 673 . . . . . . . . . . . . . . . 16 ..^
283278, 282mpbid 215 . . . . . . . . . . . . . . 15 ..^
284165, 283syl 17 . . . . . . . . . . . . . 14
285284adantr 472 . . . . . . . . . . . . 13
286 neqne 2651 . . . . . . . . . . . . . . 15
287286necomd 2698 . . . . . . . . . . . . . 14
288287adantl 473 . . . . . . . . . . . . 13
289274, 277, 285, 288leneltd 9806 . . . . . . . . . . . 12
2906, 204sstri 3427 . . . . . . . . . . . . . . . 16 ..^
291290a1i 11 . . . . . . . . . . . . . . 15 ..^
292145ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
293161ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
294176adantr 472 . . . . . . . . . . . . . . . . . 18
295273adantr 472 . . . . . . . . . . . . . . . . . . . 20
296276adantr 472 . . . . . . . . . . . . . . . . . . . 20
297 1red 9676 . . . . . . . . . . . . . . . . . . . 20
298 simpr 468 . . . . . . . . . . . . . . . . . . . 20
299295, 296, 297, 298ltadd1dd 10245 . . . . . . . . . . . . . . . . . . 19
300214adantr 472 . . . . . . . . . . . . . . . . . . 19
301299, 300breqtrd 4420 . . . . . . . . . . . . . . . . . 18
302 elfzfzo 37576 . . . . . . . . . . . . . . . . . 18 ..^
303294, 301, 302sylanbrc 677 . . . . . . . . . . . . . . . . 17 ..^
304303anim1i 578 . . . . . . . . . . . . . . . 16 ..^
305 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
306305oveq1d 6323 . . . . . . . . . . . . . . . . . 18
307306breq1d 4405 . . . . . . . . . . . . . . . . 17
308307elrab 3184 . . . . . . . . . . . . . . . 16 ..^ ..^
309304, 308sylibr 217 . . . . . . . . . . . . . . 15 ..^
310 suprub 10592 . . . . . . . . . . . . . . 15 ..^ ..^ ..^ ..^ ..^
311291, 292, 293, 309, 310syl31anc 1295 . . . . . . . . . . . . . 14 ..^
312311, 1syl6breqr 4436 . . . . . . . . . . . . 13
313273ltp1d 10559 . . . . . . . . . . . . . . 15
314 peano2re 9824 . . . . . . . . . . . . . . . . 17
315273, 314syl 17 . . . . . . . . . . . . . . . 16
316273, 315ltnled 9799 . . . . . . . . . . . . . . 15
317313, 316mpbid 215 . . . . . . . . . . . . . 14
318317ad2antrr 740 . . . . . . . . . . . . 13
319312, 318pm2.65da 586 . . . . . . . . . . . 12
320289, 319syldan 478 . . . . . . . . . . 11
321271, 320pm2.61dan 808 . . . . . . . . . 10
32244, 178ltnled 9799 . . . . . . . . . 10
323321, 322mpbird 240 . . . . . . . . 9
324197adantr 472 . . . . . . . . . . . 12
32519adantr 472 . . . . . . . . . . . 12
326178adantr 472 . . . . . . . . . . . 12
32718rexrd 9708 . . . . . . . . . . . . . 14
32819rexrd 9708 . . . . . . . . . . . . . 14
32918, 19, 31ltled 9800 . . . . . . . . . . . . . . . . . . . 20
330 lbicc2 11774 . . . . . . . . . . . . . . . . . . . 20
331327, 328, 329, 330syl3anc 1292 . . . . . . . . . . . . . . . . . . 19
332 ubicc2 11775 . . . . . . . . . . . . . . . . . . . 20
333327, 328, 329, 332syl3anc 1292 . . . . . . . . . . . . . . . . . . 19
334331, 333jca 541 . . . . . . . . . . . . . . . . . 18
335 prssg 4118 . . . . . . . . . . . . . . . . . . 19
33618, 19, 335syl2anc 673 . . . . . . . . . . . . . . . . . 18
337334, 336mpbid 215 . . . . . . . . . . . . . . . . 17
338337, 23unssd 3601 . . . . . . . . . . . . . . . 16
33917, 338syl5eqss 3462 . . . . . . . . . . . . . . 15
340339, 196sseldd 3419 . . . . . . . . . . . . . 14
341 iccleub 11715 . . . . . . . . . . . . . 14
342327, 328, 340, 341syl3anc 1292 . . . . . . . . . . . . 13
343342adantr 472 . . . . . . . . . . . 12
344 simpr 468 . . . . . . . . . . . 12
345324, 325, 326, 343, 344letrd 9809 . . . . . . . . . . 11
346345adantlr 729 . . . . . . . . . 10
347 simpr 468 . . . . . . . . . . . . 13
348178adantr 472 . . . . . . . . . . . . . 14
34919adantr 472 . . . . . . . . . . . . . 14
350348, 349ltnled 9799 . . . . . . . . . . . . 13
351347, 350mpbird 240 . . . . . . . . . . . 12
352351adantlr 729 . . . . . . . . . . 11
353 simpll 768 . . . . . . . . . . . . 13
354 simpr 468 . . . . . . . . . . . . . . 15
355178adantr 472 . . . . . . . . . . . . . . . 16
356197adantr 472 . . . . . . . . . . . . . . . 16
357355, 356ltnled 9799 . . . . . . . . . . . . . . 15
358354, 357mpbird 240 . . . . . . . . . . . . . 14
359358adant423 37430 . . . . . . . . . . . . 13
36018ad2antrr 740 . . . . . . . . . . . . . . . . . 18
36119ad2antrr 740 . . . . . . . . . . . . . . . . . 18
362178ad2antrr 740 . . . . . . . . . . . . . . . . . 18
36318adantr 472 . . . . . . . . . . . . . . . . . . . 20
364178adantr 472 . . . . . . . . . . . . . . . . . . . 20
36544adantr 472 . . . . . . . . . . . . . . . . . . . . 21
366339, 43sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . 23
367 iccgelb 11716 . . . . . . . . . . . . . . . . . . . . . . 23
368327, 328, 366, 367syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22
369368adantr 472 . . . . . . . . . . . . . . . . . . . . 21
370 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
371363, 365, 364, 369, 370lelttrd 9810 . . . . . . . . . . . . . . . . . . . 20
372363, 364, 371ltled 9800 . . . . . . . . . . . . . . . . . . 19
373372adantr 472 . . . . . . . . . . . . . . . . . 18
374178adantr 472 . . . . . . . . . . . . . . . . . . . 20
37519adantr 472 . . . . . . . . . . . . . . . . . . . 20
376 simpr 468 . . . . . . . . . . . . . . . . . . . 20
377374, 375, 376ltled 9800 . . . . . . . . . . . . . . . . . . 19
378377adantlr 729 . . . . . . . . . . . . . . . . . 18
379360, 361, 362, 373, 378eliccd 37697 . . . . . . . . . . . . . . . . 17
380167znegcld 11065 . . . . . . . . . . . . . . . . . . 19
381247, 234mulneg1d 10092 . . . . . . . . . . . . . . . . . . . . . 22
382381oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
383178recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22
384383, 240negsubd 10011 . . . . . . . . . . . . . . . . . . . . 21
385177recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22
386385, 240pncand 10006 . . . . . . . . . . . . . . . . . . . . 21
387382, 384, 3863eqtrd 2509 . . . . . . . . . . . . . . . . . . . 20
388 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
38950, 388syl 17 . . . . . . . . . . . . . . . . . . . . 21
390 fnfvelrn 6034 . . . . . . . . . . . . . . . . . . . . 21
391389, 176, 390syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
392387, 391eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19
393 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22
394393oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
395394eleq1d 2533 . . . . . . . . . . . . . . . . . . . 20
396395rspcev 3136 . . . . . . . . . . . . . . . . . . 19
397380, 392, 396syl2anc 673 . . . . . . . . . . . . . . . . . 18
398397ad2antrr 740 . . . . . . . . . . . . . . . . 17
399 oveq1 6315 . . . . . . . . . . . . . . . . . . . 20
400399eleq1d 2533 . . . . . . . . . . . . . . . . . . 19
401400rexbidv 2892 . . . . . . . . . . . . . . . . . 18
402401elrab 3184 . . . . . . . . . . . . . . . . 17
403379, 398, 402sylanbrc 677 . . . . . . . . . . . . . . . 16
404 elun2 3593 . . . . . . . . . . . . . . . 16
405403, 404syl 17 . . . . . . . . . . . . . . 15
40617eqcomi 2480 . . . . . . . . . . . . . . 15
407405, 406syl6eleq 2559 . . . . . . . . . . . . . 14
408407adantr 472 . . . . . . . . . . . . 13
409 f1ofo 5835 . . . . . . . . . . . . . . . . . 18
41036, 37, 4093syl 18 . . . . . . . . . . . . . . . . 17
411 foelrn 6056 . . . . . . . . . . . . . . . . 17
412410, 411sylan 479 . . . . . . . . . . . . . . . 16
413 id 22 . . . . . . . . . . . . . . . . . . 19
414413eqcomd 2477 . . . . . . . . . . . . . . . . . 18
415414a1i 11 . . . . . . . . . . . . . . . . 17