Step | Hyp | Ref
| Expression |
1 | | arch 11289 |
. . . . 5
|
2 | 1 | ad2antlr 763 |
. . . 4
|
3 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
|
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
|
5 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . 21
|
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
|
7 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . 21
|
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
|
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
|
10 | 5, 6, 7, 8, 9 | algrf 15286 |
. . . . . . . . . . . . . . . . . . . 20
|
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
|
12 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 11, 12 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . 20
|
15 | 10, 13, 14 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
16 | | fco 6058 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 4, 15, 16 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
18 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
|
19 | 18 | ssriv 3607 |
. . . . . . . . . . . . . . . . . 18
|
20 | | fssres 6070 |
. . . . . . . . . . . . . . . . . 18
|
21 | 17, 19, 20 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
22 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
|
24 | 3, 23 | syl5eqss 3649 |
. . . . . . . . . . . . . . 15
|
25 | | nnssre 11024 |
. . . . . . . . . . . . . . 15
|
26 | 24, 25 | syl6ss 3615 |
. . . . . . . . . . . . . 14
|
27 | 26 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
28 | | simpr 477 |
. . . . . . . . . . . . 13
|
29 | 27, 28 | sseldd 3604 |
. . . . . . . . . . . 12
|
30 | | simpllr 799 |
. . . . . . . . . . . 12
|
31 | | nnre 11027 |
. . . . . . . . . . . . 13
|
32 | 31 | ad2antlr 763 |
. . . . . . . . . . . 12
|
33 | | lelttr 10128 |
. . . . . . . . . . . 12
|
34 | 29, 30, 32, 33 | syl3anc 1326 |
. . . . . . . . . . 11
|
35 | 34 | ancomsd 470 |
. . . . . . . . . 10
|
36 | 35 | expdimp 453 |
. . . . . . . . 9
|
37 | 36 | an32s 846 |
. . . . . . . 8
|
38 | 37 | ralimdva 2962 |
. . . . . . 7
|
39 | 38 | impancom 456 |
. . . . . 6
|
40 | 39 | an32s 846 |
. . . . 5
|
41 | 40 | reximdva 3017 |
. . . 4
|
42 | 2, 41 | mpd 15 |
. . 3
|
43 | | fzfid 12772 |
. . . . 5
|
44 | | fvres 6207 |
. . . . . . . . . . . . . . 15
|
45 | 44 | adantl 482 |
. . . . . . . . . . . . . 14
|
46 | | fvco3 6275 |
. . . . . . . . . . . . . . 15
|
47 | 10, 18, 46 | syl2an 494 |
. . . . . . . . . . . . . 14
|
48 | 45, 47 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
49 | 48 | adantrr 753 |
. . . . . . . . . . . 12
|
50 | | fvres 6207 |
. . . . . . . . . . . . . 14
|
51 | 50 | ad2antll 765 |
. . . . . . . . . . . . 13
|
52 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . 14
|
54 | | fvco3 6275 |
. . . . . . . . . . . . . 14
|
55 | 10, 53, 54 | syl2an 494 |
. . . . . . . . . . . . 13
|
56 | 51, 55 | eqtrd 2656 |
. . . . . . . . . . . 12
|
57 | 49, 56 | eqeq12d 2637 |
. . . . . . . . . . 11
|
58 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . 12
|
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
61 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 62 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
64 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | 64, 65 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . . 22
|
67 | 66, 25 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . 21
|
68 | | ovolicc2.17 |
. . . . . . . . . . . . . . . . . . . . . 22
inf |
69 | 66, 5 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
71 | 5 | uzinf 12764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
73 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
74 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
75 | 73, 74 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
76 | 75 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
77 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
78 | 76, 13, 77 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
80 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
82 | 81 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
84 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
85 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
86 | | ral0 4076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
87 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
88 | 87 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
89 | 86, 88 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
90 | 89 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
91 | | rabid2 3118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
92 | 90, 91 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
93 | 85, 92 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
94 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
95 | 94, 92 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
96 | | ovolicc.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
97 | | ovolicc.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
98 | | ovolicc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
99 | | ovolicc2.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
100 | | ovolicc2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
101 | | ovolicc2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
102 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
103 | | ovolicc2.12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
104 | | ovolicc2.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
105 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem3 23287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
106 | 84, 93, 95, 105 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
107 | 83, 106 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
108 | 107 | ralrimivva 2971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
109 | | dff13 6512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
110 | 80, 108, 109 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
111 | | f1domg 7975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
112 | 79, 110, 111 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
113 | | domfi 8181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
114 | 79, 112, 113 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
115 | 114 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
116 | 115 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
117 | 72, 116 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
118 | | infssuzcl 11772 |
. . . . . . . . . . . . . . . . . . . . . . 23
inf |
119 | 69, 117, 118 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
inf |
120 | 68, 119 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | 67, 120 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
123 | 67 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
124 | 123 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
125 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 125 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
127 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . . . . 22
inf |
128 | 69, 127 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
inf |
129 | 68, 128 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . 20
|
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
131 | 63, 122, 124, 126, 130 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
132 | 131 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
133 | 60, 132 | ssrabdv 3681 |
. . . . . . . . . . . . . . . 16
|
134 | 133 | adantr 481 |
. . . . . . . . . . . . . . 15
|
135 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
136 | 134, 135 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
137 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
138 | 134, 137 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
139 | 136, 138 | jca 554 |
. . . . . . . . . . . . 13
|
140 | 139, 105 | syldan 487 |
. . . . . . . . . . . 12
|
141 | 59, 140 | syl5ibr 236 |
. . . . . . . . . . 11
|
142 | 57, 141 | sylbid 230 |
. . . . . . . . . 10
|
143 | 142 | ralrimivva 2971 |
. . . . . . . . 9
|
144 | | dff13 6512 |
. . . . . . . . 9
|
145 | 21, 143, 144 | sylanbrc 698 |
. . . . . . . 8
|
146 | | f1f1orn 6148 |
. . . . . . . 8
|
147 | 145, 146 | syl 17 |
. . . . . . 7
|
148 | | f1oeq3 6129 |
. . . . . . . 8
|
149 | 3, 148 | ax-mp 5 |
. . . . . . 7
|
150 | 147, 149 | sylibr 224 |
. . . . . 6
|
151 | | f1ofo 6144 |
. . . . . 6
|
152 | 150, 151 | syl 17 |
. . . . 5
|
153 | | fofi 8252 |
. . . . 5
|
154 | 43, 152, 153 | syl2anc 693 |
. . . 4
|
155 | | fimaxre2 10969 |
. . . 4
|
156 | 26, 154, 155 | syl2anc 693 |
. . 3
|
157 | 42, 156 | r19.29a 3078 |
. 2
|
158 | 97, 96 | resubcld 10458 |
. . . . 5
|
159 | 158 | rexrd 10089 |
. . . 4
|
160 | 159 | adantr 481 |
. . 3
|
161 | | fzfid 12772 |
. . . . . 6
|
162 | | elfznn 12370 |
. . . . . . . . 9
|
163 | | eqid 2622 |
. . . . . . . . . . . 12
|
164 | 163 | ovolfsf 23240 |
. . . . . . . . . . 11
|
165 | 100, 164 | syl 17 |
. . . . . . . . . 10
|
166 | 165 | ffvelrnda 6359 |
. . . . . . . . 9
|
167 | 162, 166 | sylan2 491 |
. . . . . . . 8
|
168 | | elrege0 12278 |
. . . . . . . 8
|
169 | 167, 168 | sylib 208 |
. . . . . . 7
|
170 | 169 | simpld 475 |
. . . . . 6
|
171 | 161, 170 | fsumrecl 14465 |
. . . . 5
|
172 | 171 | adantr 481 |
. . . 4
|
173 | 172 | rexrd 10089 |
. . 3
|
174 | 163, 99 | ovolsf 23241 |
. . . . . . . . 9
|
175 | 100, 174 | syl 17 |
. . . . . . . 8
|
176 | | frn 6053 |
. . . . . . . 8
|
177 | 175, 176 | syl 17 |
. . . . . . 7
|
178 | | rge0ssre 12280 |
. . . . . . 7
|
179 | 177, 178 | syl6ss 3615 |
. . . . . 6
|
180 | | ressxr 10083 |
. . . . . 6
|
181 | 179, 180 | syl6ss 3615 |
. . . . 5
|
182 | | supxrcl 12145 |
. . . . 5
|
183 | 181, 182 | syl 17 |
. . . 4
|
184 | 183 | adantr 481 |
. . 3
|
185 | 158 | adantr 481 |
. . . 4
|
186 | 24 | sselda 3603 |
. . . . . . 7
|
187 | 178, 166 | sseldi 3601 |
. . . . . . 7
|
188 | 186, 187 | syldan 487 |
. . . . . 6
|
189 | 154, 188 | fsumrecl 14465 |
. . . . 5
|
190 | 189 | adantr 481 |
. . . 4
|
191 | | inss2 3834 |
. . . . . . . . . . 11
|
192 | | fss 6056 |
. . . . . . . . . . 11
|
193 | 100, 191,
192 | sylancl 694 |
. . . . . . . . . 10
|
194 | 66, 120 | sseldi 3601 |
. . . . . . . . . . . 12
|
195 | 15, 194 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
196 | 4, 195 | ffvelrnd 6360 |
. . . . . . . . . 10
|
197 | 193, 196 | ffvelrnd 6360 |
. . . . . . . . 9
|
198 | | xp2nd 7199 |
. . . . . . . . 9
|
199 | 197, 198 | syl 17 |
. . . . . . . 8
|
200 | 13, 8 | sseldi 3601 |
. . . . . . . . . . 11
|
201 | 4, 200 | ffvelrnd 6360 |
. . . . . . . . . 10
|
202 | 193, 201 | ffvelrnd 6360 |
. . . . . . . . 9
|
203 | | xp1st 7198 |
. . . . . . . . 9
|
204 | 202, 203 | syl 17 |
. . . . . . . 8
|
205 | 199, 204 | resubcld 10458 |
. . . . . . 7
|
206 | | fveq2 6191 |
. . . . . . . . . 10
|
207 | 187 | recnd 10068 |
. . . . . . . . . . 11
|
208 | 186, 207 | syldan 487 |
. . . . . . . . . 10
|
209 | 206, 43, 150, 48, 208 | fsumf1o 14454 |
. . . . . . . . 9
|
210 | 100 | adantr 481 |
. . . . . . . . . . 11
|
211 | 4 | adantr 481 |
. . . . . . . . . . . 12
|
212 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
213 | 15, 18, 212 | syl2an 494 |
. . . . . . . . . . . 12
|
214 | 211, 213 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
215 | 163 | ovolfsval 23239 |
. . . . . . . . . . 11
|
216 | 210, 214,
215 | syl2anc 693 |
. . . . . . . . . 10
|
217 | 216 | sumeq2dv 14433 |
. . . . . . . . 9
|
218 | 193 | adantr 481 |
. . . . . . . . . . . . . . 15
|
219 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
220 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
221 | 219, 220 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
|
222 | 218, 221 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
223 | | xp2nd 7199 |
. . . . . . . . . . . . . 14
|
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . 13
|
225 | 18, 224 | sylan2 491 |
. . . . . . . . . . . 12
|
226 | 225 | recnd 10068 |
. . . . . . . . . . 11
|
227 | 193 | adantr 481 |
. . . . . . . . . . . . . 14
|
228 | 227, 214 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
229 | | xp1st 7198 |
. . . . . . . . . . . . 13
|
230 | 228, 229 | syl 17 |
. . . . . . . . . . . 12
|
231 | 230 | recnd 10068 |
. . . . . . . . . . 11
|
232 | 43, 226, 231 | fsumsub 14520 |
. . . . . . . . . 10
|
233 | 69, 120 | sseldi 3601 |
. . . . . . . . . . . . 13
|
234 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
235 | 234 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
236 | 235 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
237 | 236 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
238 | 233, 226,
237 | fsumm1 14480 |
. . . . . . . . . . . 12
|
239 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
240 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
|
241 | 240, 224 | sylan2 491 |
. . . . . . . . . . . . . . 15
|
242 | 239, 241 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
|
243 | 242 | recnd 10068 |
. . . . . . . . . . . . 13
|
244 | 199 | recnd 10068 |
. . . . . . . . . . . . 13
|
245 | 243, 244 | addcomd 10238 |
. . . . . . . . . . . 12
|
246 | 238, 245 | eqtrd 2656 |
. . . . . . . . . . 11
|
247 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
248 | 247 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
249 | 248 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
250 | 249 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
251 | 233, 231,
250 | fsum1p 14482 |
. . . . . . . . . . . 12
|
252 | 5, 6, 7, 8 | algr0 15285 |
. . . . . . . . . . . . . . . 16
|
253 | 252 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
254 | 253 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
255 | 254 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
256 | 7 | peano2zd 11485 |
. . . . . . . . . . . . . . 15
|
257 | 194 | nnzd 11481 |
. . . . . . . . . . . . . . 15
|
258 | | fzp1ss 12392 |
. . . . . . . . . . . . . . . . . 18
|
259 | 70, 258 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
|
260 | 259 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
261 | 260, 231 | syldan 487 |
. . . . . . . . . . . . . . 15
|
262 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
263 | 262 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
264 | 263 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
265 | 264 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
266 | 7, 256, 257, 261, 265 | fsumshftm 14513 |
. . . . . . . . . . . . . 14
|
267 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . 18
|
268 | 267, 267 | pncan3oi 10297 |
. . . . . . . . . . . . . . . . 17
|
269 | 268 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
270 | 269 | sumeq1i 14428 |
. . . . . . . . . . . . . . 15
|
271 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
272 | 271 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
273 | 272 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
274 | 273 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
275 | 274 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
276 | 275 | cbvsumv 14426 |
. . . . . . . . . . . . . . 15
|
277 | 270, 276 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
278 | 266, 277 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
279 | 255, 278 | oveq12d 6668 |
. . . . . . . . . . . 12
|
280 | 251, 279 | eqtrd 2656 |
. . . . . . . . . . 11
|
281 | 246, 280 | oveq12d 6668 |
. . . . . . . . . 10
|
282 | 204 | recnd 10068 |
. . . . . . . . . . 11
|
283 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . 18
|
284 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . 18
|
285 | 15, 283, 284 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
286 | 219, 285 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
287 | 218, 286 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
|
288 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
|
289 | 287, 288 | syl 17 |
. . . . . . . . . . . . . 14
|
290 | 240, 289 | sylan2 491 |
. . . . . . . . . . . . 13
|
291 | 239, 290 | fsumrecl 14465 |
. . . . . . . . . . . 12
|
292 | 291 | recnd 10068 |
. . . . . . . . . . 11
|
293 | 244, 243,
282, 292 | addsub4d 10439 |
. . . . . . . . . 10
|
294 | 232, 281,
293 | 3eqtrd 2660 |
. . . . . . . . 9
|
295 | 209, 217,
294 | 3eqtrd 2660 |
. . . . . . . 8
|
296 | 295, 189 | eqeltrrd 2702 |
. . . . . . 7
|
297 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
298 | 297 | eleq2d 2687 |
. . . . . . . . . . . . . 14
|
299 | 298, 64 | elrab2 3366 |
. . . . . . . . . . . . 13
|
300 | 120, 299 | sylib 208 |
. . . . . . . . . . . 12
|
301 | 300 | simprd 479 |
. . . . . . . . . . 11
|
302 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . 12
|
303 | 195, 302 | mpdan 702 |
. . . . . . . . . . 11
|
304 | 301, 303 | mpbid 222 |
. . . . . . . . . 10
|
305 | 304 | simp3d 1075 |
. . . . . . . . 9
|
306 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . 12
|
307 | 200, 306 | mpdan 702 |
. . . . . . . . . . 11
|
308 | 104, 307 | mpbid 222 |
. . . . . . . . . 10
|
309 | 308 | simp2d 1074 |
. . . . . . . . 9
|
310 | 97, 204, 199, 96, 305, 309 | lt2subd 10651 |
. . . . . . . 8
|
311 | 158, 205,
310 | ltled 10185 |
. . . . . . 7
|
312 | 240 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
313 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
314 | 257 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
315 | | elfzm11 12411 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
316 | 70, 314, 315 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
|
317 | 313, 316 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
318 | 317 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . 20
|
319 | 312 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . 21
|
320 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
321 | 319, 320 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . 20
|
322 | 318, 321 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
323 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . . . 21
inf |
324 | 69, 323 | mpan 706 |
. . . . . . . . . . . . . . . . . . . 20
inf |
325 | 68, 324 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . 19
|
326 | 322, 325 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
|
327 | 312, 326 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
328 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem2 23286 |
. . . . . . . . . . . . . . . . 17
|
329 | 327, 328 | syldan 487 |
. . . . . . . . . . . . . . . 16
|
330 | 329 | iftrued 4094 |
. . . . . . . . . . . . . . 15
|
331 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
|
332 | 10, 240, 331 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
333 | 103 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
|
334 | 333 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
335 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
336 | 335 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
337 | 336 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
338 | 337 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
|
339 | 338, 337 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . 18
|
340 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
341 | 339, 340 | eleq12d 2695 |
. . . . . . . . . . . . . . . . 17
|
342 | 341 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
|
343 | 332, 334,
342 | sylc 65 |
. . . . . . . . . . . . . . 15
|
344 | 330, 343 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
|
345 | 5, 6, 7, 8, 9 | algrp1 15287 |
. . . . . . . . . . . . . . 15
|
346 | 240, 345 | sylan2 491 |
. . . . . . . . . . . . . 14
|
347 | 344, 346 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
|
348 | 240, 285 | sylan2 491 |
. . . . . . . . . . . . . 14
|
349 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . . . 14
|
350 | 348, 349 | syldan 487 |
. . . . . . . . . . . . 13
|
351 | 347, 350 | mpbid 222 |
. . . . . . . . . . . 12
|
352 | 351 | simp2d 1074 |
. . . . . . . . . . 11
|
353 | 290, 241,
352 | ltled 10185 |
. . . . . . . . . 10
|
354 | 239, 290,
241, 353 | fsumle 14531 |
. . . . . . . . 9
|
355 | 242, 291 | subge0d 10617 |
. . . . . . . . 9
|
356 | 354, 355 | mpbird 247 |
. . . . . . . 8
|
357 | 242, 291 | resubcld 10458 |
. . . . . . . . 9
|
358 | 205, 357 | addge01d 10615 |
. . . . . . . 8
|
359 | 356, 358 | mpbid 222 |
. . . . . . 7
|
360 | 158, 205,
296, 311, 359 | letrd 10194 |
. . . . . 6
|
361 | 360, 295 | breqtrrd 4681 |
. . . . 5
|
362 | 361 | adantr 481 |
. . . 4
|
363 | | fzfid 12772 |
. . . . 5
|
364 | 170 | adantlr 751 |
. . . . 5
|
365 | 169 | simprd 479 |
. . . . . 6
|
366 | 365 | adantlr 751 |
. . . . 5
|
367 | 24 | adantr 481 |
. . . . . . . . . . . 12
|
368 | 367 | sselda 3603 |
. . . . . . . . . . 11
|
369 | 368 | nnred 11035 |
. . . . . . . . . 10
|
370 | 31 | ad2antlr 763 |
. . . . . . . . . 10
|
371 | | ltle 10126 |
. . . . . . . . . 10
|
372 | 369, 370,
371 | syl2anc 693 |
. . . . . . . . 9
|
373 | 368, 5 | syl6eleq 2711 |
. . . . . . . . . 10
|
374 | | nnz 11399 |
. . . . . . . . . . 11
|
375 | 374 | ad2antlr 763 |
. . . . . . . . . 10
|
376 | | elfz5 12334 |
. . . . . . . . . 10
|
377 | 373, 375,
376 | syl2anc 693 |
. . . . . . . . 9
|
378 | 372, 377 | sylibrd 249 |
. . . . . . . 8
|
379 | 378 | ralimdva 2962 |
. . . . . . 7
|
380 | 379 | impr 649 |
. . . . . 6
|
381 | | dfss3 3592 |
. . . . . 6
|
382 | 380, 381 | sylibr 224 |
. . . . 5
|
383 | 363, 364,
366, 382 | fsumless 14528 |
. . . 4
|
384 | 185, 190,
172, 362, 383 | letrd 10194 |
. . 3
|
385 | | eqidd 2623 |
. . . . . 6
|
386 | | simprl 794 |
. . . . . . 7
|
387 | 386, 5 | syl6eleq 2711 |
. . . . . 6
|
388 | 364 | recnd 10068 |
. . . . . 6
|
389 | 385, 387,
388 | fsumser 14461 |
. . . . 5
|
390 | 99 | fveq1i 6192 |
. . . . 5
|
391 | 389, 390 | syl6eqr 2674 |
. . . 4
|
392 | 181 | adantr 481 |
. . . . 5
|
393 | | ffn 6045 |
. . . . . . . 8
|
394 | 175, 393 | syl 17 |
. . . . . . 7
|
395 | 394 | adantr 481 |
. . . . . 6
|
396 | | fnfvelrn 6356 |
. . . . . 6
|
397 | 395, 386,
396 | syl2anc 693 |
. . . . 5
|
398 | | supxrub 12154 |
. . . . 5
|
399 | 392, 397,
398 | syl2anc 693 |
. . . 4
|
400 | 391, 399 | eqbrtrd 4675 |
. . 3
|
401 | 160, 173,
184, 384, 400 | xrletrd 11993 |
. 2
|
402 | 157, 401 | rexlimddv 3035 |
1
|