Mathbox for Steve Rodriguez < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  binomcxplemnotnn0 Structured version   Visualization version   Unicode version

Theorem binomcxplemnotnn0 36775
 Description: Lemma for binomcxp 36776. When is not a nonnegative integer, the generalized sum in binomcxplemnn0 36768 —which we will call —is a convergent power series: its base is always of smaller absolute value than the radius of convergence. pserdv2 23464 gives the derivative of , which by dvradcnv 23455 also converges in that radius. When is fixed at one, times that derivative equals and fraction is always defined with derivative zero, so the fraction is a constant—specifically one, because . Thus . Finally, let be , and multiply both the binomial and the sum by to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.)
Hypotheses
Ref Expression
binomcxp.a
binomcxp.b
binomcxp.lt
binomcxp.c
binomcxplem.f C𝑐
binomcxplem.s
binomcxplem.r
binomcxplem.e
binomcxplem.d
binomcxplem.p
Assertion
Ref Expression
binomcxplemnotnn0 C𝑐
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   ()   ()   (,)   (,,,)   (,,,)   (,)   (,)   ()

Proof of Theorem binomcxplemnotnn0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 binomcxplem.p . . . . . . 7
2 binomcxplem.d . . . . . . . . 9
3 nfcv 2612 . . . . . . . . . 10
4 nfcv 2612 . . . . . . . . . . 11
5 nfcv 2612 . . . . . . . . . . 11
6 binomcxplem.r . . . . . . . . . . . 12
7 nfcv 2612 . . . . . . . . . . . . . . . 16
8 binomcxplem.s . . . . . . . . . . . . . . . . . 18
9 nfmpt1 4485 . . . . . . . . . . . . . . . . . 18
108, 9nfcxfr 2610 . . . . . . . . . . . . . . . . 17
11 nfcv 2612 . . . . . . . . . . . . . . . . 17
1210, 11nffv 5886 . . . . . . . . . . . . . . . 16
134, 7, 12nfseq 12261 . . . . . . . . . . . . . . 15
1413nfel1 2626 . . . . . . . . . . . . . 14
15 nfcv 2612 . . . . . . . . . . . . . 14
1614, 15nfrab 2958 . . . . . . . . . . . . 13
17 nfcv 2612 . . . . . . . . . . . . 13
18 nfcv 2612 . . . . . . . . . . . . 13
1916, 17, 18nfsup 7983 . . . . . . . . . . . 12
206, 19nfcxfr 2610 . . . . . . . . . . 11
214, 5, 20nfov 6334 . . . . . . . . . 10
223, 21nfima 5182 . . . . . . . . 9
232, 22nfcxfr 2610 . . . . . . . 8
24 nfcv 2612 . . . . . . . 8
25 nfcv 2612 . . . . . . . 8
26 nfcv 2612 . . . . . . . . 9
27 nfcv 2612 . . . . . . . . . . 11
2810, 27nffv 5886 . . . . . . . . . 10
29 nfcv 2612 . . . . . . . . . 10
3028, 29nffv 5886 . . . . . . . . 9
3126, 30nfsum 13834 . . . . . . . 8
32 simpl 464 . . . . . . . . . . 11
3332fveq2d 5883 . . . . . . . . . 10
3433fveq1d 5881 . . . . . . . . 9
3534sumeq2dv 13846 . . . . . . . 8
3623, 24, 25, 31, 35cbvmptf 4486 . . . . . . 7
371, 36eqtri 2493 . . . . . 6
3837a1i 11 . . . . 5
39 simplr 770 . . . . . . . 8
4039fveq2d 5883 . . . . . . 7
4140fveq1d 5881 . . . . . 6
4241sumeq2dv 13846 . . . . 5
43 binomcxp.b . . . . . . . . 9
4443recnd 9687 . . . . . . . 8
4544adantr 472 . . . . . . 7
46 binomcxp.a . . . . . . . . 9
4746rpcnd 11366 . . . . . . . 8
4847adantr 472 . . . . . . 7
49 0red 9662 . . . . . . . . . 10
5045abscld 13575 . . . . . . . . . 10
5148abscld 13575 . . . . . . . . . 10
5245absge0d 13583 . . . . . . . . . 10
53 binomcxp.lt . . . . . . . . . . 11
5453adantr 472 . . . . . . . . . 10
5549, 50, 51, 52, 54lelttrd 9810 . . . . . . . . 9
5655gt0ne0d 10199 . . . . . . . 8
5748abs00ad 13430 . . . . . . . . 9
5857necon3bid 2687 . . . . . . . 8
5956, 58mpbid 215 . . . . . . 7
6045, 48, 59divcld 10405 . . . . . 6
6160abscld 13575 . . . . . . 7
6260absge0d 13583 . . . . . . 7
6351recnd 9687 . . . . . . . . . . 11
6463mulid1d 9678 . . . . . . . . . 10
6554, 64breqtrrd 4422 . . . . . . . . 9
66 1red 9676 . . . . . . . . . 10
6751, 55elrpd 11361 . . . . . . . . . 10
6850, 66, 67ltdivmuld 11412 . . . . . . . . 9
6965, 68mpbird 240 . . . . . . . 8
7045, 48, 59absdivd 13594 . . . . . . . 8
71 binomcxp.c . . . . . . . . 9
72 binomcxplem.f . . . . . . . . 9 C𝑐
7346, 43, 53, 71, 72, 8, 6binomcxplemradcnv 36771 . . . . . . . 8
7469, 70, 733brtr4d 4426 . . . . . . 7
75 0re 9661 . . . . . . . 8
76 ssrab2 3500 . . . . . . . . . . 11
77 ressxr 9702 . . . . . . . . . . 11
7876, 77sstri 3427 . . . . . . . . . 10
79 supxrcl 11625 . . . . . . . . . 10
8078, 79ax-mp 5 . . . . . . . . 9
816, 80eqeltri 2545 . . . . . . . 8
82 elico2 11723 . . . . . . . 8
8375, 81, 82mp2an 686 . . . . . . 7
8461, 62, 74, 83syl3anbrc 1214 . . . . . 6
852eleq2i 2541 . . . . . . 7
86 absf 13477 . . . . . . . 8
87 ffn 5739 . . . . . . . 8
88 elpreima 6017 . . . . . . . 8
8986, 87, 88mp2b 10 . . . . . . 7
9085, 89bitri 257 . . . . . 6
9160, 84, 90sylanbrc 677 . . . . 5
92 sumex 13831 . . . . . 6
9392a1i 11 . . . . 5
9438, 42, 91, 93fvmptd 5969 . . . 4
95 eqid 2471 . . . . . . . . . . . . 13
9695cnbl0 21872 . . . . . . . . . . . 12
9781, 96ax-mp 5 . . . . . . . . . . 11
982, 97eqtri 2493 . . . . . . . . . 10
99 0cnd 9654 . . . . . . . . . 10
10081a1i 11 . . . . . . . . . 10
101 mulcl 9641 . . . . . . . . . . . 12
102101adantl 473 . . . . . . . . . . 11
103 nfv 1769 . . . . . . . . . . . . . . 15
10423nfcri 2606 . . . . . . . . . . . . . . 15
105103, 104nfan 2031 . . . . . . . . . . . . . 14
10631nfel1 2626 . . . . . . . . . . . . . 14
107105, 106nfim 2023 . . . . . . . . . . . . 13
108 eleq1 2537 . . . . . . . . . . . . . . 15
109108anbi2d 718 . . . . . . . . . . . . . 14
11035eleq1d 2533 . . . . . . . . . . . . . 14
111109, 110imbi12d 327 . . . . . . . . . . . . 13
112 nn0uz 11217 . . . . . . . . . . . . . 14
113 0zd 10973 . . . . . . . . . . . . . 14
114 eqidd 2472 . . . . . . . . . . . . . 14
115 cnvimass 5194 . . . . . . . . . . . . . . . . . . . 20
1162, 115eqsstri 3448 . . . . . . . . . . . . . . . . . . 19
11786fdmi 5746 . . . . . . . . . . . . . . . . . . 19
118116, 117sseqtri 3450 . . . . . . . . . . . . . . . . . 18
119118sseli 3414 . . . . . . . . . . . . . . . . 17
1208a1i 11 . . . . . . . . . . . . . . . . . . . 20
121 nn0ex 10899 . . . . . . . . . . . . . . . . . . . . . 22
122121mptex 6152 . . . . . . . . . . . . . . . . . . . . 21
123122a1i 11 . . . . . . . . . . . . . . . . . . . 20
124120, 123fvmpt2d 5974 . . . . . . . . . . . . . . . . . . 19
125 ovex 6336 . . . . . . . . . . . . . . . . . . . 20
126125a1i 11 . . . . . . . . . . . . . . . . . . 19
127124, 126fvmpt2d 5974 . . . . . . . . . . . . . . . . . 18
12872a1i 11 . . . . . . . . . . . . . . . . . . . . 21 C𝑐
129 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
130129oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21 C𝑐 C𝑐
131 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
132 ovex 6336 . . . . . . . . . . . . . . . . . . . . . 22 C𝑐
133132a1i 11 . . . . . . . . . . . . . . . . . . . . 21 C𝑐
134128, 130, 131, 133fvmptd 5969 . . . . . . . . . . . . . . . . . . . 20 C𝑐
135134oveq1d 6323 . . . . . . . . . . . . . . . . . . 19 C𝑐
136135adantlr 729 . . . . . . . . . . . . . . . . . 18 C𝑐
137127, 136eqtrd 2505 . . . . . . . . . . . . . . . . 17 C𝑐
138119, 137sylanl2 663 . . . . . . . . . . . . . . . 16 C𝑐
13971ad2antrr 740 . . . . . . . . . . . . . . . . . 18
140 simpr 468 . . . . . . . . . . . . . . . . . 18
141139, 140bcccl 36758 . . . . . . . . . . . . . . . . 17 C𝑐
142119ad2antlr 741 . . . . . . . . . . . . . . . . . 18
143142, 140expcld 12454 . . . . . . . . . . . . . . . . 17
144141, 143mulcld 9681 . . . . . . . . . . . . . . . 16 C𝑐
145138, 144eqeltrd 2549 . . . . . . . . . . . . . . 15
146145adantllr 733 . . . . . . . . . . . . . 14
147 eleq1 2537 . . . . . . . . . . . . . . . . . . 19
148147anbi2d 718 . . . . . . . . . . . . . . . . . 18
149 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
150149seqeq3d 12259 . . . . . . . . . . . . . . . . . . . 20
151150eleq1d 2533 . . . . . . . . . . . . . . . . . . 19
152 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
153152seqeq3d 12259 . . . . . . . . . . . . . . . . . . . 20
154153eleq1d 2533 . . . . . . . . . . . . . . . . . . 19
155151, 154anbi12d 725 . . . . . . . . . . . . . . . . . 18
156148, 155imbi12d 327 . . . . . . . . . . . . . . . . 17
157 binomcxplem.e . . . . . . . . . . . . . . . . . 18
15846, 43, 53, 71, 72, 8, 6, 157, 2binomcxplemcvg 36773 . . . . . . . . . . . . . . . . 17
159156, 158chvarv 2120 . . . . . . . . . . . . . . . 16
160159simpld 466 . . . . . . . . . . . . . . 15
161160adantlr 729 . . . . . . . . . . . . . 14
162112, 113, 114, 146, 161isumcl 13899 . . . . . . . . . . . . 13
163107, 111, 162chvar 2119 . . . . . . . . . . . 12
164163, 37fmptd 6061 . . . . . . . . . . 11
165 1cnd 9677 . . . . . . . . . . . . . 14
166118sseli 3414 . . . . . . . . . . . . . . 15
167166adantl 473 . . . . . . . . . . . . . 14
168165, 167addcld 9680 . . . . . . . . . . . . 13
16971ad2antrr 740 . . . . . . . . . . . . . 14
170169negcld 9992 . . . . . . . . . . . . 13
171168, 170cxpcld 23732 . . . . . . . . . . . 12
172 nfcv 2612 . . . . . . . . . . . . 13
173 nfcv 2612 . . . . . . . . . . . . 13
174 oveq2 6316 . . . . . . . . . . . . . 14
175174oveq1d 6323 . . . . . . . . . . . . 13
17623, 24, 172, 173, 175cbvmptf 4486 . . . . . . . . . . . 12
177171, 176fmptd 6061 . . . . . . . . . . 11
178 cnex 9638 . . . . . . . . . . . . . . . 16
179 fex 6155 . . . . . . . . . . . . . . . 16
18086, 178, 179mp2an 686 . . . . . . . . . . . . . . 15
181180cnvex 6759 . . . . . . . . . . . . . 14
182 imaexg 6749 . . . . . . . . . . . . . 14
183181, 182ax-mp 5 . . . . . . . . . . . . 13
1842, 183eqeltri 2545 . . . . . . . . . . . 12
185184a1i 11 . . . . . . . . . . 11
186 inidm 3632 . . . . . . . . . . 11
187102, 164, 177, 185, 185, 186off 6565 . . . . . . . . . 10
188 1ex 9656 . . . . . . . . . . . . . 14
189188fconst 5782 . . . . . . . . . . . . 13
190 fconstmpt 4883 . . . . . . . . . . . . . . 15
191 nfcv 2612 . . . . . . . . . . . . . . . 16
192 nfcv 2612 . . . . . . . . . . . . . . . 16
193 eqidd 2472 . . . . . . . . . . . . . . . 16
19424, 23, 191, 192, 193cbvmptf 4486 . . . . . . . . . . . . . . 15
195190, 194eqtri 2493 . . . . . . . . . . . . . 14
196195feq1i 5730 . . . . . . . . . . . . 13
197189, 196mpbi 213 . . . . . . . . . . . 12
198 ax-1cn 9615 . . . . . . . . . . . . 13
199 snssi 4107 . . . . . . . . . . . . 13
200198, 199ax-mp 5 . . . . . . . . . . . 12
201 fss 5749 . . . . . . . . . . . 12
202197, 200, 201mp2an 686 . . . . . . . . . . 11
203202a1i 11 . . . . . . . . . 10
204 cnelprrecn 9650 . . . . . . . . . . . . . . . . 17
205204a1i 11 . . . . . . . . . . . . . . . 16
20646, 43, 53, 71, 72, 8, 6, 157, 2, 1binomcxplemdvsum 36774 . . . . . . . . . . . . . . . . . . . 20
207206adantr 472 . . . . . . . . . . . . . . . . . . 19
208 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
209 nfcv 2612 . . . . . . . . . . . . . . . . . . . . 21
210 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . . . 24
211157, 210nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . . . 23
212211, 27nffv 5886 . . . . . . . . . . . . . . . . . . . . . 22
213212, 29nffv 5886 . . . . . . . . . . . . . . . . . . . . 21
214209, 213nfsum 13834 . . . . . . . . . . . . . . . . . . . 20
215 simpl 464 . . . . . . . . . . . . . . . . . . . . . . 23
216215fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22
217216fveq1d 5881 . . . . . . . . . . . . . . . . . . . . 21
218217sumeq2dv 13846 . . . . . . . . . . . . . . . . . . . 20
21923, 24, 208, 214, 218cbvmptf 4486 . . . . . . . . . . . . . . . . . . 19
220207, 219syl6eq 2521 . . . . . . . . . . . . . . . . . 18
221 sumex 13831 . . . . . . . . . . . . . . . . . . 19
222221a1i 11 . . . . . . . . . . . . . . . . . 18
223220, 222fmpt3d 6062 . . . . . . . . . . . . . . . . 17
224 fdm 5745 . . . . . . . . . . . . . . . . 17
225223, 224syl 17 . . . . . . . . . . . . . . . 16
22646, 43, 53, 71, 72, 8, 6, 157, 2binomcxplemdvbinom 36772 . . . . . . . . . . . . . . . . . . 19
227 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
228 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
229174oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21
230229oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20
23123, 24, 227, 228, 230cbvmptf 4486 . . . . . . . . . . . . . . . . . . 19
232226, 231syl6eq 2521 . . . . . . . . . . . . . . . . . 18
233170, 165subcld 10005 . . . . . . . . . . . . . . . . . . . 20
234168, 233cxpcld 23732 . . . . . . . . . . . . . . . . . . 19
235170, 234mulcld 9681 . . . . . . . . . . . . . . . . . 18
236232, 235fmpt3d 6062 . . . . . . . . . . . . . . . . 17
237 fdm 5745 . . . . . . . . . . . . . . . . 17
238236, 237syl 17 . . . . . . . . . . . . . . . 16
239205, 164, 177, 225, 238dvmulf 22976 . . . . . . . . . . . . . . 15
24071ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
241240mulid1d 9678 . . . . . . . . . . . . . . . . . . . . . . . 24
242241oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23 C𝑐 C𝑐
243 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . 24
244 nnuz 11218 . . . . . . . . . . . . . . . . . . . . . . . . 25
245 1zzd 10992 . . . . . . . . . . . . . . . . . . . . . . . . 25
246 nnnn0 10900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
247246, 138sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 C𝑐
248247adantllr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25 C𝑐
24971ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
250 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
251249, 250bcccl 36758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
252246, 251sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 C𝑐
253119adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254253adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
255254, 250expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
256246, 255sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26
257252, 256mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . 25 C𝑐
258 1nn0 10909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
259258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
260112, 259, 145iserex 13797 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
261160, 260mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26
262261adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25
263244, 245, 248, 257, 262isumcl 13899 . . . . . . . . . . . . . . . . . . . . . . . 24 C𝑐
264240, 243, 263adddid 9685 . . . . . . . . . . . . . . . . . . . . . . 23 C𝑐 C𝑐
265157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
266 nnex 10637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
267266mptex 6152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
268267a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
269265, 268fvmpt2d 5974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
270119, 269sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
271270adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
272 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
273272a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
274271, 273fmpt3d 6062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
275274feqmptd 5932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
276272a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
277269, 276fvmpt2d 5974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
278246, 134sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 C𝑐
279278oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C𝑐
280279oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 C𝑐
281280adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 C𝑐
282277, 281eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 C𝑐
28371adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
284 nnm1nn0 10935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
285284adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
286283, 285bccp1k 36760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 C𝑐 C𝑐
287246adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
288287nn0cnd 10951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
289 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
290288, 289npcand 10009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
291290oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 C𝑐 C𝑐
292290oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
293292oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 C𝑐 C𝑐
294286, 291, 2933eqtr3d 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 C𝑐 C𝑐
295294oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C𝑐 C𝑐
296283, 285bcccl 36758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 C𝑐
297288, 289subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
298283, 297subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
299 nnne0 10664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
300299adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
301296, 298, 288, 300divassd 10440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 C𝑐 C𝑐
302301oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C𝑐 C𝑐
303296, 298mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 C𝑐
304303, 288, 300divcan2d 10407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 C𝑐 C𝑐
305295, 302, 3043eqtr2d 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 C𝑐 C𝑐
306305oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 C𝑐 C𝑐
307306adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 C𝑐 C𝑐
308296adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 C𝑐
309298adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
310308, 309mulcomd 9682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 C𝑐 C𝑐
311310oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 C𝑐 C𝑐
312282, 307, 3113eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 C𝑐
313119, 312sylanl2 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 C𝑐
314313adantllr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C𝑐
315314mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C𝑐
316275, 315eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐
317316oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐
318 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
319 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐
320 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
321320oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
322320oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C𝑐 C𝑐
323321, 322oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C𝑐 C𝑐
324320oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
325323, 324oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
326 1pneg1e0 10740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
327326fveq2i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
328112, 327eqtr4i 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
329245znegcld 11065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
330318, 319, 325, 244, 328, 245, 329uzmptshftfval 36765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐 C𝑐
331 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
332331oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
333332oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
334332oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 C𝑐 C𝑐
335333, 334oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C𝑐 C𝑐
336332oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
337335, 336oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C𝑐 C𝑐
338337cbvmptv 4488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
339338a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐 C𝑐
340317, 330, 3393eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐
341 nn0cn 10903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
342 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
343341, 342subnegd 10012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
344343oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
345341, 342pncand 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
346344, 345eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
347346adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
348347oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
349347oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C𝑐 C𝑐
350348, 349oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
351347oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
352350, 351oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐 C𝑐
353352mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐 C𝑐
354340, 353eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
355 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐
356355a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
357354, 356fvmpt2d 5974 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
358246, 357sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
359341adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
360249, 359subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
361360, 251mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
362361, 255mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
363246, 362sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
364 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
365364oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
366365cbvmptv 4488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
367314oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐
368253adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
36971ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
370 nncn 10639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
371370adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
372 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
373371, 372subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
374369, 373subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
375284adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
376369, 375bcccl 36758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 C𝑐
377374, 376mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 C𝑐
378368, 375expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
379368, 377, 378mul12d 9860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
380368, 378mulcomd 9682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
381368, 375expp1d 12455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
382290adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
383382adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
384383oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
385380, 381, 3843eqtr2d 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
386385oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 C𝑐 C𝑐
387379, 386eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 C𝑐 C𝑐
388367, 387eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐
389388mpteq2dva 4482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
390366, 389syl5eqr 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
391 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
392391a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
393390, 392fvmpt2d 5974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
394377, 256mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
395 climrel 13633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
396159simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
397396adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
398 climdm 13695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
399397, 398sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
400 0z 10972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
401 neg1z 10997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
402 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
403402seqshft 13225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
404400, 401, 403mp2an 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
405 0cn 9653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
406405, 198subnegi 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
407 0p1e1 10743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
408406, 407eqtri 2493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
409 seqeq1 12254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
410408, 409ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
411410oveq1i 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
412404, 411eqtri 2493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
413412breq1i 4402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
414 seqex 12253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
415 climshft 13717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
416401, 414, 415mp2an 686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
417413, 416bitri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
418399, 417sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
419 releldm 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
420395, 418, 419sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
421258a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
422357, 362eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
423112, 421, 422iserex 13797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
424420, 423mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
425377, 378mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐
426314, 425eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
427393, 388eqtr4d 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
428244, 245, 253, 399, 426, 427isermulc2 13798 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
429 releldm 5073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
430395, 428, 429sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
431244, 245, 358, 363, 393, 394, 424, 430isumadd 13905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 C𝑐 C𝑐 C𝑐 C𝑐
432431oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25 C𝑐 C𝑐 C𝑐 C𝑐
433369, 371subcld 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
434433, 252mulcld 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
435434, 377, 256adddird 9686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐 C𝑐 C𝑐 C𝑐
436435sumeq2dv 13846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 C𝑐 C𝑐 C𝑐 C𝑐
437436oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . 25 C𝑐 C𝑐 C𝑐 C𝑐
438312sumeq2dv 13846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 C𝑐
439438oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐
440119, 439sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
441440adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐
442244, 245, 314, 425, 397isumcl 13899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐
443243, 253, 442adddird 9686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 C𝑐 C𝑐 C𝑐
444442mulid2d 9679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 C𝑐 C𝑐
445244, 245, 314, 425, 397, 253isummulc2 13900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 C𝑐 C𝑐