# Metamath Proof Explorer

## Theorem binomcxplemdvsum

Description: Lemma for binomcxp . The derivative of the generalized sum in binomcxplemnn0 . Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
binomcxp.b ${⊢}{\phi }\to {B}\in ℝ$
binomcxp.lt ${⊢}{\phi }\to \left|{B}\right|<\left|{A}\right|$
binomcxp.c ${⊢}{\phi }\to {C}\in ℂ$
binomcxplem.f ${⊢}{F}=\left({j}\in {ℕ}_{0}⟼{C}{C}_{𝑐}{j}\right)$
binomcxplem.s ${⊢}{S}=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
binomcxplem.r ${⊢}{R}=sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
binomcxplem.e ${⊢}{E}=\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
binomcxplem.d ${⊢}{D}={\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]$
binomcxplem.p ${⊢}{P}=\left({b}\in {D}⟼\sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)\right)$
Assertion binomcxplemdvsum ${⊢}{\phi }\to ℂ\mathrm{D}{P}=\left({b}\in {D}⟼\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)\right)$

### Proof

Step Hyp Ref Expression
1 binomcxp.a ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
2 binomcxp.b ${⊢}{\phi }\to {B}\in ℝ$
3 binomcxp.lt ${⊢}{\phi }\to \left|{B}\right|<\left|{A}\right|$
4 binomcxp.c ${⊢}{\phi }\to {C}\in ℂ$
5 binomcxplem.f ${⊢}{F}=\left({j}\in {ℕ}_{0}⟼{C}{C}_{𝑐}{j}\right)$
6 binomcxplem.s ${⊢}{S}=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
7 binomcxplem.r ${⊢}{R}=sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
8 binomcxplem.e ${⊢}{E}=\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
9 binomcxplem.d ${⊢}{D}={\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]$
10 binomcxplem.p ${⊢}{P}=\left({b}\in {D}⟼\sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)\right)$
11 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{\mathrm{abs}}^{-1}$
12 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}0$
13 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left[.\right)$
14 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}+$
15 nfmpt1 ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
16 6 15 nfcxfr ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{S}$
17 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{r}$
18 16 17 nffv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{S}\left({r}\right)$
19 12 14 18 nfseq ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}seq0\left(+,{S}\left({r}\right)\right)$
20 19 nfel1 ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝$
21 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}ℝ$
22 20 21 nfrabw ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\}$
23 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{ℝ}^{*}$
24 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}<$
25 22 23 24 nfsup ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
26 7 25 nfcxfr ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{R}$
27 12 13 26 nfov ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left[0,{R}\right)$
28 11 27 nfima ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]$
29 9 28 nfcxfr ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{D}$
30 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{D}$
31 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)$
32 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{ℕ}_{0}$
33 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{y}$
34 16 33 nffv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{S}\left({y}\right)$
35 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{m}$
36 34 35 nffv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{S}\left({y}\right)\left({m}\right)$
37 32 36 nfsumw ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\sum _{{m}\in {ℕ}_{0}}{S}\left({y}\right)\left({m}\right)$
38 simpl ${⊢}\left({b}={y}\wedge {k}\in {ℕ}_{0}\right)\to {b}={y}$
39 38 fveq2d ${⊢}\left({b}={y}\wedge {k}\in {ℕ}_{0}\right)\to {S}\left({b}\right)={S}\left({y}\right)$
40 39 fveq1d ${⊢}\left({b}={y}\wedge {k}\in {ℕ}_{0}\right)\to {S}\left({b}\right)\left({k}\right)={S}\left({y}\right)\left({k}\right)$
41 40 sumeq2dv ${⊢}{b}={y}\to \sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)=\sum _{{k}\in {ℕ}_{0}}{S}\left({y}\right)\left({k}\right)$
42 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{S}\left({y}\right)\left({k}\right)$
43 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}ℂ$
44 nfmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)$
45 43 44 nfmpt ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
46 6 45 nfcxfr ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{S}$
47 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{y}$
48 46 47 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{S}\left({y}\right)$
49 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{m}$
50 48 49 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{S}\left({y}\right)\left({m}\right)$
51 fveq2 ${⊢}{k}={m}\to {S}\left({y}\right)\left({k}\right)={S}\left({y}\right)\left({m}\right)$
52 42 50 51 cbvsumi ${⊢}\sum _{{k}\in {ℕ}_{0}}{S}\left({y}\right)\left({k}\right)=\sum _{{m}\in {ℕ}_{0}}{S}\left({y}\right)\left({m}\right)$
53 41 52 syl6eq ${⊢}{b}={y}\to \sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)=\sum _{{m}\in {ℕ}_{0}}{S}\left({y}\right)\left({m}\right)$
54 29 30 31 37 53 cbvmptf ${⊢}\left({b}\in {D}⟼\sum _{{k}\in {ℕ}_{0}}{S}\left({b}\right)\left({k}\right)\right)=\left({y}\in {D}⟼\sum _{{m}\in {ℕ}_{0}}{S}\left({y}\right)\left({m}\right)\right)$
55 10 54 eqtri ${⊢}{P}=\left({y}\in {D}⟼\sum _{{m}\in {ℕ}_{0}}{S}\left({y}\right)\left({m}\right)\right)$
56 ovexd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {C}{C}_{𝑐}{j}\in \mathrm{V}$
57 5 a1i ${⊢}{\phi }\to {F}=\left({j}\in {ℕ}_{0}⟼{C}{C}_{𝑐}{j}\right)$
58 5 a1i ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}=\left({j}\in {ℕ}_{0}⟼{C}{C}_{𝑐}{j}\right)$
59 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\wedge {j}={k}\right)\to {j}={k}$
60 59 oveq2d ${⊢}\left(\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\wedge {j}={k}\right)\to {C}{C}_{𝑐}{j}={C}{C}_{𝑐}{k}$
61 simpr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
62 4 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {C}\in ℂ$
63 62 61 bcccl ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {C}{C}_{𝑐}{k}\in ℂ$
64 58 60 61 63 fvmptd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)={C}{C}_{𝑐}{k}$
65 64 63 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)\in ℂ$
66 56 57 65 fmpt2d ${⊢}{\phi }\to {F}:{ℕ}_{0}⟶ℂ$
67 nfcv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}ℝ$
68 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}ℝ$
69 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝$
70 nfcv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}0$
71 nfcv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}+$
72 nfcv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
73 6 72 nfcxfr ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}{S}$
74 nfcv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}{z}$
75 73 74 nffv ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}{S}\left({z}\right)$
76 70 71 75 nfseq ${⊢}\underset{_}{Ⅎ}{r}\phantom{\rule{.4em}{0ex}}seq0\left(+,{S}\left({z}\right)\right)$
77 76 nfel1 ${⊢}Ⅎ{r}\phantom{\rule{.4em}{0ex}}seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝$
78 fveq2 ${⊢}{r}={z}\to {S}\left({r}\right)={S}\left({z}\right)$
79 78 seqeq3d ${⊢}{r}={z}\to seq0\left(+,{S}\left({r}\right)\right)=seq0\left(+,{S}\left({z}\right)\right)$
80 79 eleq1d ${⊢}{r}={z}\to \left(seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝↔seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right)$
81 67 68 69 77 80 cbvrabw ${⊢}\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{z}\in ℝ|seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right\}$
82 81 supeq1i ${⊢}sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=sup\left(\left\{{z}\in ℝ|seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
83 7 82 eqtri ${⊢}{R}=sup\left(\left\{{z}\in ℝ|seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
84 6 fveq1i ${⊢}{S}\left({z}\right)=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)$
85 seqeq3 ${⊢}{S}\left({z}\right)=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\to seq0\left(+,{S}\left({z}\right)\right)=seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)$
86 84 85 ax-mp ${⊢}seq0\left(+,{S}\left({z}\right)\right)=seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)$
87 86 eleq1i ${⊢}seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝↔seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝$
88 87 rabbii ${⊢}\left\{{z}\in ℝ|seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\}$
89 88 supeq1i ${⊢}sup\left(\left\{{z}\in ℝ|seq0\left(+,{S}\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
90 7 82 89 3eqtrri ${⊢}sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)={R}$
91 90 eleq1i ${⊢}sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ↔{R}\in ℝ$
92 90 oveq2i ${⊢}\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=\left|{x}\right|+{R}$
93 92 oveq1i ${⊢}\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2}=\frac{\left|{x}\right|+{R}}{2}$
94 eqid ${⊢}\left|{x}\right|+1=\left|{x}\right|+1$
95 91 93 94 ifbieq12i ${⊢}if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)=if\left({R}\in ℝ,\frac{\left|{x}\right|+{R}}{2},\left|{x}\right|+1\right)$
96 oveq1 ${⊢}{w}={b}\to {{w}}^{{k}}={{b}}^{{k}}$
97 96 oveq2d ${⊢}{w}={b}\to {F}\left({k}\right){{w}}^{{k}}={F}\left({k}\right){{b}}^{{k}}$
98 97 mpteq2dv ${⊢}{w}={b}\to \left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)=\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)$
99 98 cbvmptv ${⊢}\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)$
100 99 fveq1i ${⊢}\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)$
101 seqeq3 ${⊢}\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)=\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\to seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)=seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)$
102 100 101 ax-mp ${⊢}seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)=seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)$
103 102 eleq1i ${⊢}seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝↔seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝$
104 103 rabbii ${⊢}\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\}=\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\}$
105 104 supeq1i ${⊢}sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
106 105 eleq1i ${⊢}sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ↔sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ$
107 105 oveq2i ${⊢}\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)=\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$
108 107 oveq1i ${⊢}\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2}=\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2}$
109 106 108 94 ifbieq12i ${⊢}if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)=if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)$
110 109 oveq2i ${⊢}\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)=\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)$
111 110 oveq1i ${⊢}\frac{\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)}{2}=\frac{\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)}{2}$
112 111 oveq2i ${⊢}0\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({w}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{w}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)}{2}\right)=0\mathrm{ball}\left(\mathrm{abs}\circ -\right)\left(\frac{\left|{x}\right|+if\left(sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in ℝ,\frac{\left|{x}\right|+sup\left(\left\{{z}\in ℝ|seq0\left(+,\left({b}\in ℂ⟼\left({k}\in {ℕ}_{0}⟼{F}\left({k}\right){{b}}^{{k}}\right)\right)\left({z}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)}{2},\left|{x}\right|+1\right)}{2}\right)$
113 6 55 66 83 9 95 112 pserdv2 ${⊢}{\phi }\to ℂ\mathrm{D}{P}=\left({y}\in {D}⟼\sum _{{n}\in ℕ}{n}{F}\left({n}\right){{y}}^{{n}-1}\right)$
114 cnvimass ${⊢}{\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]\subseteq \mathrm{dom}\mathrm{abs}$
115 9 114 eqsstri ${⊢}{D}\subseteq \mathrm{dom}\mathrm{abs}$
116 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
117 116 fdmi ${⊢}\mathrm{dom}\mathrm{abs}=ℂ$
118 115 117 sseqtri ${⊢}{D}\subseteq ℂ$
119 118 sseli ${⊢}{y}\in {D}\to {y}\in ℂ$
120 8 a1i ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to {E}=\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
121 simplr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {b}={y}\right)\wedge {k}\in ℕ\right)\to {b}={y}$
122 121 oveq1d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {b}={y}\right)\wedge {k}\in ℕ\right)\to {{b}}^{{k}-1}={{y}}^{{k}-1}$
123 122 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {b}={y}\right)\wedge {k}\in ℕ\right)\to {k}{F}\left({k}\right){{b}}^{{k}-1}={k}{F}\left({k}\right){{y}}^{{k}-1}$
124 123 mpteq2dva ${⊢}\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {b}={y}\right)\to \left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{y}}^{{k}-1}\right)$
125 simpr ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to {y}\in ℂ$
126 nnex ${⊢}ℕ\in \mathrm{V}$
127 126 mptex ${⊢}\left({k}\in ℕ⟼{k}{F}\left({k}\right){{y}}^{{k}-1}\right)\in \mathrm{V}$
128 127 a1i ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to \left({k}\in ℕ⟼{k}{F}\left({k}\right){{y}}^{{k}-1}\right)\in \mathrm{V}$
129 120 124 125 128 fvmptd ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to {E}\left({y}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{y}}^{{k}-1}\right)$
130 129 adantr ${⊢}\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\to {E}\left({y}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{y}}^{{k}-1}\right)$
131 simpr ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {k}={n}$
132 131 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {F}\left({k}\right)={F}\left({n}\right)$
133 131 132 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {k}{F}\left({k}\right)={n}{F}\left({n}\right)$
134 131 oveq1d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {k}-1={n}-1$
135 134 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {{y}}^{{k}-1}={{y}}^{{n}-1}$
136 133 135 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to {k}{F}\left({k}\right){{y}}^{{k}-1}={n}{F}\left({n}\right){{y}}^{{n}-1}$
137 simpr ${⊢}\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\to {n}\in ℕ$
138 ovexd ${⊢}\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\to {n}{F}\left({n}\right){{y}}^{{n}-1}\in \mathrm{V}$
139 130 136 137 138 fvmptd ${⊢}\left(\left({\phi }\wedge {y}\in ℂ\right)\wedge {n}\in ℕ\right)\to {E}\left({y}\right)\left({n}\right)={n}{F}\left({n}\right){{y}}^{{n}-1}$
140 139 sumeq2dv ${⊢}\left({\phi }\wedge {y}\in ℂ\right)\to \sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)=\sum _{{n}\in ℕ}{n}{F}\left({n}\right){{y}}^{{n}-1}$
141 119 140 sylan2 ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to \sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)=\sum _{{n}\in ℕ}{n}{F}\left({n}\right){{y}}^{{n}-1}$
142 141 mpteq2dva ${⊢}{\phi }\to \left({y}\in {D}⟼\sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)\right)=\left({y}\in {D}⟼\sum _{{n}\in ℕ}{n}{F}\left({n}\right){{y}}^{{n}-1}\right)$
143 113 142 eqtr4d ${⊢}{\phi }\to ℂ\mathrm{D}{P}=\left({y}\in {D}⟼\sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)\right)$
144 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}ℕ$
145 nfmpt1 ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
146 8 145 nfcxfr ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{E}$
147 146 33 nffv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{E}\left({y}\right)$
148 nfcv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{n}$
149 147 148 nffv ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}{E}\left({y}\right)\left({n}\right)$
150 144 149 nfsumw ${⊢}\underset{_}{Ⅎ}{b}\phantom{\rule{.4em}{0ex}}\sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)$
151 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)$
152 simpl ${⊢}\left({y}={b}\wedge {n}\in ℕ\right)\to {y}={b}$
153 152 fveq2d ${⊢}\left({y}={b}\wedge {n}\in ℕ\right)\to {E}\left({y}\right)={E}\left({b}\right)$
154 153 fveq1d ${⊢}\left({y}={b}\wedge {n}\in ℕ\right)\to {E}\left({y}\right)\left({n}\right)={E}\left({b}\right)\left({n}\right)$
155 154 sumeq2dv ${⊢}{y}={b}\to \sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)=\sum _{{n}\in ℕ}{E}\left({b}\right)\left({n}\right)$
156 nfmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)$
157 43 156 nfmpt ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
158 8 157 nfcxfr ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{E}$
159 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{b}$
160 158 159 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{E}\left({b}\right)$
161 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{n}$
162 160 161 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{E}\left({b}\right)\left({n}\right)$
163 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{E}\left({b}\right)\left({k}\right)$
164 fveq2 ${⊢}{n}={k}\to {E}\left({b}\right)\left({n}\right)={E}\left({b}\right)\left({k}\right)$
165 162 163 164 cbvsumi ${⊢}\sum _{{n}\in ℕ}{E}\left({b}\right)\left({n}\right)=\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)$
166 155 165 syl6eq ${⊢}{y}={b}\to \sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)=\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)$
167 30 29 150 151 166 cbvmptf ${⊢}\left({y}\in {D}⟼\sum _{{n}\in ℕ}{E}\left({y}\right)\left({n}\right)\right)=\left({b}\in {D}⟼\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)\right)$
168 143 167 syl6eq ${⊢}{\phi }\to ℂ\mathrm{D}{P}=\left({b}\in {D}⟼\sum _{{k}\in ℕ}{E}\left({b}\right)\left({k}\right)\right)$