Step | Hyp | Ref
| Expression |
1 | | fzofi 12773 |
. . . . . 6
..^ |
2 | 1 | a1i 11 |
. . . . 5
..^ |
3 | | dvfsumabs.x |
. . . . 5
..^ |
4 | | dvfsumabs.m |
. . . . . . . . . . . . 13
|
5 | | eluzel2 11692 |
. . . . . . . . . . . . 13
|
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
|
7 | | eluzelz 11697 |
. . . . . . . . . . . . 13
|
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
|
9 | | fzval2 12329 |
. . . . . . . . . . . 12
|
10 | 6, 8, 9 | syl2anc 693 |
. . . . . . . . . . 11
|
11 | | inss1 3833 |
. . . . . . . . . . 11
|
12 | 10, 11 | syl6eqss 3655 |
. . . . . . . . . 10
|
13 | 12 | sselda 3603 |
. . . . . . . . 9
|
14 | | dvfsumabs.a |
. . . . . . . . . . . 12
|
15 | | cncff 22696 |
. . . . . . . . . . . 12
|
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
|
17 | | eqid 2622 |
. . . . . . . . . . . 12
|
18 | 17 | fmpt 6381 |
. . . . . . . . . . 11
|
19 | 16, 18 | sylibr 224 |
. . . . . . . . . 10
|
20 | | nfcsb1v 3549 |
. . . . . . . . . . . 12
|
21 | 20 | nfel1 2779 |
. . . . . . . . . . 11
|
22 | | csbeq1a 3542 |
. . . . . . . . . . . 12
|
23 | 22 | eleq1d 2686 |
. . . . . . . . . . 11
|
24 | 21, 23 | rspc 3303 |
. . . . . . . . . 10
|
25 | 19, 24 | mpan9 486 |
. . . . . . . . 9
|
26 | 13, 25 | syldan 487 |
. . . . . . . 8
|
27 | 26 | ralrimiva 2966 |
. . . . . . 7
|
28 | | fzofzp1 12565 |
. . . . . . 7
..^
|
29 | | csbeq1 3536 |
. . . . . . . . 9
|
30 | 29 | eleq1d 2686 |
. . . . . . . 8
|
31 | 30 | rspccva 3308 |
. . . . . . 7
|
32 | 27, 28, 31 | syl2an 494 |
. . . . . 6
..^
|
33 | | elfzofz 12485 |
. . . . . . 7
..^
|
34 | | csbeq1 3536 |
. . . . . . . . 9
|
35 | 34 | eleq1d 2686 |
. . . . . . . 8
|
36 | 35 | rspccva 3308 |
. . . . . . 7
|
37 | 27, 33, 36 | syl2an 494 |
. . . . . 6
..^
|
38 | 32, 37 | subcld 10392 |
. . . . 5
..^ |
39 | 2, 3, 38 | fsumsub 14520 |
. . . 4
..^
..^ ..^ |
40 | | vex 3203 |
. . . . . . . 8
|
41 | 40 | a1i 11 |
. . . . . . 7
|
42 | | eqeq2 2633 |
. . . . . . . . 9
|
43 | 42 | biimpa 501 |
. . . . . . . 8
|
44 | | dvfsumabs.c |
. . . . . . . 8
|
45 | 43, 44 | syl 17 |
. . . . . . 7
|
46 | 41, 45 | csbied 3560 |
. . . . . 6
|
47 | 40 | a1i 11 |
. . . . . . 7
|
48 | | eqeq2 2633 |
. . . . . . . . 9
|
49 | 48 | biimpa 501 |
. . . . . . . 8
|
50 | | dvfsumabs.d |
. . . . . . . 8
|
51 | 49, 50 | syl 17 |
. . . . . . 7
|
52 | 47, 51 | csbied 3560 |
. . . . . 6
|
53 | 34, 29, 46, 52, 4, 26 | telfsumo2 14535 |
. . . . 5
..^
|
54 | 53 | oveq2d 6666 |
. . . 4
..^ ..^
..^
|
55 | 39, 54 | eqtrd 2656 |
. . 3
..^
..^ |
56 | 55 | fveq2d 6195 |
. 2
..^ ..^
|
57 | 3, 38 | subcld 10392 |
. . . . 5
..^
|
58 | 2, 57 | fsumcl 14464 |
. . . 4
..^
|
59 | 58 | abscld 14175 |
. . 3
..^ |
60 | 57 | abscld 14175 |
. . . 4
..^
|
61 | 2, 60 | fsumrecl 14465 |
. . 3
..^ |
62 | | dvfsumabs.y |
. . . 4
..^ |
63 | 2, 62 | fsumrecl 14465 |
. . 3
..^ |
64 | 2, 57 | fsumabs 14533 |
. . 3
..^ ..^ |
65 | | elfzoelz 12470 |
. . . . . . . . . 10
..^
|
66 | 65 | adantl 482 |
. . . . . . . . 9
..^ |
67 | 66 | zred 11482 |
. . . . . . . 8
..^ |
68 | 67 | rexrd 10089 |
. . . . . . 7
..^ |
69 | | peano2re 10209 |
. . . . . . . . 9
|
70 | 67, 69 | syl 17 |
. . . . . . . 8
..^ |
71 | 70 | rexrd 10089 |
. . . . . . 7
..^ |
72 | 67 | lep1d 10955 |
. . . . . . 7
..^ |
73 | | ubicc2 12289 |
. . . . . . 7
|
74 | 68, 71, 72, 73 | syl3anc 1326 |
. . . . . 6
..^ |
75 | | lbicc2 12288 |
. . . . . . 7
|
76 | 68, 71, 72, 75 | syl3anc 1326 |
. . . . . 6
..^ |
77 | 6 | zred 11482 |
. . . . . . . . . . . 12
|
78 | 77 | adantr 481 |
. . . . . . . . . . 11
..^ |
79 | 8 | zred 11482 |
. . . . . . . . . . . 12
|
80 | 79 | adantr 481 |
. . . . . . . . . . 11
..^ |
81 | | elfzole1 12478 |
. . . . . . . . . . . 12
..^
|
82 | 81 | adantl 482 |
. . . . . . . . . . 11
..^ |
83 | 28 | adantl 482 |
. . . . . . . . . . . 12
..^ |
84 | | elfzle2 12345 |
. . . . . . . . . . . 12
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
..^ |
86 | | iccss 12241 |
. . . . . . . . . . 11
|
87 | 78, 80, 82, 85, 86 | syl22anc 1327 |
. . . . . . . . . 10
..^ |
88 | 87 | resmptd 5452 |
. . . . . . . . 9
..^ |
89 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
90 | 89 | subcn 22669 |
. . . . . . . . . . . 12
ℂfld ℂfld ℂfld |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
..^ ℂfld
ℂfld ℂfld |
92 | | iccssre 12255 |
. . . . . . . . . . . . . . . 16
|
93 | 77, 79, 92 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
94 | 93 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
95 | | ax-resscn 9993 |
. . . . . . . . . . . . . 14
|
96 | 94, 95 | syl6ss 3615 |
. . . . . . . . . . . . 13
..^ |
97 | | ssid 3624 |
. . . . . . . . . . . . . 14
|
98 | 97 | a1i 11 |
. . . . . . . . . . . . 13
..^ |
99 | | cncfmptc 22714 |
. . . . . . . . . . . . 13
|
100 | 3, 96, 98, 99 | syl3anc 1326 |
. . . . . . . . . . . 12
..^ |
101 | | cncfmptid 22715 |
. . . . . . . . . . . . 13
|
102 | 96, 97, 101 | sylancl 694 |
. . . . . . . . . . . 12
..^ |
103 | 100, 102 | mulcncf 23215 |
. . . . . . . . . . 11
..^ |
104 | 14 | adantr 481 |
. . . . . . . . . . 11
..^ |
105 | 89, 91, 103, 104 | cncfmpt2f 22717 |
. . . . . . . . . 10
..^ |
106 | | rescncf 22700 |
. . . . . . . . . 10
|
107 | 87, 105, 106 | sylc 65 |
. . . . . . . . 9
..^ |
108 | 88, 107 | eqeltrrd 2702 |
. . . . . . . 8
..^ |
109 | 95 | a1i 11 |
. . . . . . . . . . . 12
..^ |
110 | 87, 94 | sstrd 3613 |
. . . . . . . . . . . 12
..^ |
111 | 87 | sselda 3603 |
. . . . . . . . . . . . 13
..^ |
112 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
..^ |
113 | 96 | sselda 3603 |
. . . . . . . . . . . . . . 15
..^ |
114 | 112, 113 | mulcld 10060 |
. . . . . . . . . . . . . 14
..^
|
115 | 19 | r19.21bi 2932 |
. . . . . . . . . . . . . . 15
|
116 | 115 | adantlr 751 |
. . . . . . . . . . . . . 14
..^ |
117 | 114, 116 | subcld 10392 |
. . . . . . . . . . . . 13
..^ |
118 | 111, 117 | syldan 487 |
. . . . . . . . . . . 12
..^ |
119 | 89 | tgioo2 22606 |
. . . . . . . . . . . 12
ℂfld
↾t |
120 | | iccntr 22624 |
. . . . . . . . . . . . 13
|
121 | 67, 70, 120 | syl2anc 693 |
. . . . . . . . . . . 12
..^ |
122 | 109, 110,
118, 119, 89, 121 | dvmptntr 23734 |
. . . . . . . . . . 11
..^
|
123 | | reelprrecn 10028 |
. . . . . . . . . . . . 13
|
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
..^
|
125 | | ioossicc 12259 |
. . . . . . . . . . . . . 14
|
126 | 125 | sseli 3599 |
. . . . . . . . . . . . 13
|
127 | 126, 117 | sylan2 491 |
. . . . . . . . . . . 12
..^ |
128 | | ovex 6678 |
. . . . . . . . . . . . 13
|
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
..^
|
130 | 126, 114 | sylan2 491 |
. . . . . . . . . . . . 13
..^
|
131 | 3 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
132 | 125, 96 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
..^ |
133 | 132 | sselda 3603 |
. . . . . . . . . . . . . . 15
..^ |
134 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
..^ |
135 | 109 | sselda 3603 |
. . . . . . . . . . . . . . . 16
..^ |
136 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
..^ |
137 | 124 | dvmptid 23720 |
. . . . . . . . . . . . . . . 16
..^
|
138 | 125, 94 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
..^ |
139 | | iooretop 22569 |
. . . . . . . . . . . . . . . . 17
|
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^ |
141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 23726 |
. . . . . . . . . . . . . . 15
..^
|
142 | 124, 133,
134, 141, 3 | dvmptcmul 23727 |
. . . . . . . . . . . . . 14
..^
|
143 | 3 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
..^ |
144 | 143 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
..^ |
145 | 142, 144 | eqtrd 2656 |
. . . . . . . . . . . . 13
..^
|
146 | 126, 116 | sylan2 491 |
. . . . . . . . . . . . 13
..^ |
147 | | dvfsumabs.v |
. . . . . . . . . . . . . 14
|
148 | 147 | adantlr 751 |
. . . . . . . . . . . . 13
..^ |
149 | | dvfsumabs.b |
. . . . . . . . . . . . . 14
|
150 | 149 | adantr 481 |
. . . . . . . . . . . . 13
..^
|
151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 23730 |
. . . . . . . . . . . 12
..^
|
152 | 78 | rexrd 10089 |
. . . . . . . . . . . . . 14
..^ |
153 | | iooss1 12210 |
. . . . . . . . . . . . . 14
|
154 | 152, 82, 153 | syl2anc 693 |
. . . . . . . . . . . . 13
..^ |
155 | 80 | rexrd 10089 |
. . . . . . . . . . . . . 14
..^ |
156 | | iooss2 12211 |
. . . . . . . . . . . . . 14
|
157 | 155, 85, 156 | syl2anc 693 |
. . . . . . . . . . . . 13
..^ |
158 | 154, 157 | sstrd 3613 |
. . . . . . . . . . . 12
..^ |
159 | | iooretop 22569 |
. . . . . . . . . . . . 13
|
160 | 159 | a1i 11 |
. . . . . . . . . . . 12
..^ |
161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 23726 |
. . . . . . . . . . 11
..^
|
162 | 122, 161 | eqtrd 2656 |
. . . . . . . . . 10
..^
|
163 | 162 | dmeqd 5326 |
. . . . . . . . 9
..^
|
164 | | eqid 2622 |
. . . . . . . . . 10
|
165 | 128, 164 | dmmpti 6023 |
. . . . . . . . 9
|
166 | 163, 165 | syl6eq 2672 |
. . . . . . . 8
..^
|
167 | 162 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
168 | 167 | fveq1d 6193 |
. . . . . . . . . . . . 13
..^ |
169 | | simpr 477 |
. . . . . . . . . . . . . 14
..^ |
170 | 164 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
171 | 169, 128,
170 | sylancl 694 |
. . . . . . . . . . . . 13
..^ |
172 | 168, 171 | eqtrd 2656 |
. . . . . . . . . . . 12
..^ |
173 | 172 | fveq2d 6195 |
. . . . . . . . . . 11
..^
|
174 | | dvfsumabs.l |
. . . . . . . . . . . 12
..^ |
175 | 174 | anassrs 680 |
. . . . . . . . . . 11
..^ |
176 | 173, 175 | eqbrtrd 4675 |
. . . . . . . . . 10
..^ |
177 | 176 | ralrimiva 2966 |
. . . . . . . . 9
..^ |
178 | | nfcv 2764 |
. . . . . . . . . . . 12
|
179 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
180 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
181 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
|
182 | 179, 180,
181 | nfov 6676 |
. . . . . . . . . . . . 13
|
183 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
184 | 182, 183 | nffv 6198 |
. . . . . . . . . . . 12
|
185 | 178, 184 | nffv 6198 |
. . . . . . . . . . 11
|
186 | | nfcv 2764 |
. . . . . . . . . . 11
|
187 | | nfcv 2764 |
. . . . . . . . . . 11
|
188 | 185, 186,
187 | nfbr 4699 |
. . . . . . . . . 10
|
189 | | fveq2 6191 |
. . . . . . . . . . . 12
|
190 | 189 | fveq2d 6195 |
. . . . . . . . . . 11
|
191 | 190 | breq1d 4663 |
. . . . . . . . . 10
|
192 | 188, 191 | rspc 3303 |
. . . . . . . . 9
|
193 | 177, 192 | mpan9 486 |
. . . . . . . 8
..^ |
194 | 67, 70, 108, 166, 62, 193 | dvlip 23756 |
. . . . . . 7
..^ |
195 | 194 | ex 450 |
. . . . . 6
..^
|
196 | 74, 76, 195 | mp2and 715 |
. . . . 5
..^ |
197 | | ovex 6678 |
. . . . . . . . 9
|
198 | | nfcv 2764 |
. . . . . . . . . 10
|
199 | | nfcv 2764 |
. . . . . . . . . . 11
|
200 | | nfcv 2764 |
. . . . . . . . . . 11
|
201 | | nfcsb1v 3549 |
. . . . . . . . . . 11
|
202 | 199, 200,
201 | nfov 6676 |
. . . . . . . . . 10
|
203 | | oveq2 6658 |
. . . . . . . . . . 11
|
204 | | csbeq1a 3542 |
. . . . . . . . . . 11
|
205 | 203, 204 | oveq12d 6668 |
. . . . . . . . . 10
|
206 | | eqid 2622 |
. . . . . . . . . 10
|
207 | 198, 202,
205, 206 | fvmptf 6301 |
. . . . . . . . 9
|
208 | 74, 197, 207 | sylancl 694 |
. . . . . . . 8
..^ |
209 | 67 | recnd 10068 |
. . . . . . . . . . 11
..^ |
210 | 3, 209 | mulcld 10060 |
. . . . . . . . . 10
..^ |
211 | 210, 37 | subcld 10392 |
. . . . . . . . 9
..^ |
212 | | nfcv 2764 |
. . . . . . . . . 10
|
213 | | nfcv 2764 |
. . . . . . . . . . 11
|
214 | | nfcsb1v 3549 |
. . . . . . . . . . 11
|
215 | 213, 200,
214 | nfov 6676 |
. . . . . . . . . 10
|
216 | | oveq2 6658 |
. . . . . . . . . . 11
|
217 | | csbeq1a 3542 |
. . . . . . . . . . 11
|
218 | 216, 217 | oveq12d 6668 |
. . . . . . . . . 10
|
219 | 212, 215,
218, 206 | fvmptf 6301 |
. . . . . . . . 9
|
220 | 76, 211, 219 | syl2anc 693 |
. . . . . . . 8
..^ |
221 | 208, 220 | oveq12d 6668 |
. . . . . . 7
..^ |
222 | | peano2cn 10208 |
. . . . . . . . . 10
|
223 | 209, 222 | syl 17 |
. . . . . . . . 9
..^ |
224 | 3, 223 | mulcld 10060 |
. . . . . . . 8
..^ |
225 | 224, 210,
32, 37 | sub4d 10441 |
. . . . . . 7
..^
|
226 | | 1cnd 10056 |
. . . . . . . . . . 11
..^ |
227 | 209, 226 | pncan2d 10394 |
. . . . . . . . . 10
..^ |
228 | 227 | oveq2d 6666 |
. . . . . . . . 9
..^ |
229 | 3, 223, 209 | subdid 10486 |
. . . . . . . . 9
..^ |
230 | 228, 229,
143 | 3eqtr3d 2664 |
. . . . . . . 8
..^
|
231 | 230 | oveq1d 6665 |
. . . . . . 7
..^
|
232 | 221, 225,
231 | 3eqtr2rd 2663 |
. . . . . 6
..^
|
233 | 232 | fveq2d 6195 |
. . . . 5
..^
|
234 | 227 | fveq2d 6195 |
. . . . . . . 8
..^ |
235 | | abs1 14037 |
. . . . . . . 8
|
236 | 234, 235 | syl6eq 2672 |
. . . . . . 7
..^ |
237 | 236 | oveq2d 6666 |
. . . . . 6
..^ |
238 | 62 | recnd 10068 |
. . . . . . 7
..^ |
239 | 238 | mulid1d 10057 |
. . . . . 6
..^ |
240 | 237, 239 | eqtr2d 2657 |
. . . . 5
..^ |
241 | 196, 233,
240 | 3brtr4d 4685 |
. . . 4
..^
|
242 | 2, 60, 62, 241 | fsumle 14531 |
. . 3
..^ ..^ |
243 | 59, 61, 63, 64, 242 | letrd 10194 |
. 2
..^ ..^ |
244 | 56, 243 | eqbrtrrd 4677 |
1
..^
..^ |