Metamath Proof Explorer

Theorem binomcxplemcvg

Description: Lemma for binomcxp . The sum in binomcxplemnn0 and its derivative (see the next theorem, binomcxplemdvsum ) converge, as long as their base J is within the disk of convergence. 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]$
Assertion binomcxplemcvg ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to \left(seq0\left(+,{S}\left({J}\right)\right)\in \mathrm{dom}⇝\wedge seq1\left(+,{E}\left({J}\right)\right)\in \mathrm{dom}⇝\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 4 adantr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {C}\in ℂ$
11 simpr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}\in {ℕ}_{0}$
12 10 11 bcccl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {C}{C}_{𝑐}{j}\in ℂ$
13 12 5 fmptd ${⊢}{\phi }\to {F}:{ℕ}_{0}⟶ℂ$
14 13 adantr ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to {F}:{ℕ}_{0}⟶ℂ$
15 9 eleq2i ${⊢}{J}\in {D}↔{J}\in {\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]$
16 absf ${⊢}\mathrm{abs}:ℂ⟶ℝ$
17 ffn ${⊢}\mathrm{abs}:ℂ⟶ℝ\to \mathrm{abs}Fnℂ$
18 elpreima ${⊢}\mathrm{abs}Fnℂ\to \left({J}\in {\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]↔\left({J}\in ℂ\wedge \left|{J}\right|\in \left[0,{R}\right)\right)\right)$
19 16 17 18 mp2b ${⊢}{J}\in {\mathrm{abs}}^{-1}\left[\left[0,{R}\right)\right]↔\left({J}\in ℂ\wedge \left|{J}\right|\in \left[0,{R}\right)\right)$
20 15 19 bitri ${⊢}{J}\in {D}↔\left({J}\in ℂ\wedge \left|{J}\right|\in \left[0,{R}\right)\right)$
21 20 simplbi ${⊢}{J}\in {D}\to {J}\in ℂ$
22 21 adantl ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to {J}\in ℂ$
23 20 simprbi ${⊢}{J}\in {D}\to \left|{J}\right|\in \left[0,{R}\right)$
24 0re ${⊢}0\in ℝ$
25 ssrab2 ${⊢}\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq ℝ$
26 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
27 25 26 sstri ${⊢}\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq {ℝ}^{*}$
28 supxrcl ${⊢}\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\}\subseteq {ℝ}^{*}\to sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in {ℝ}^{*}$
29 27 28 ax-mp ${⊢}sup\left(\left\{{r}\in ℝ|seq0\left(+,{S}\left({r}\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)\in {ℝ}^{*}$
30 7 29 eqeltri ${⊢}{R}\in {ℝ}^{*}$
31 elico2 ${⊢}\left(0\in ℝ\wedge {R}\in {ℝ}^{*}\right)\to \left(\left|{J}\right|\in \left[0,{R}\right)↔\left(\left|{J}\right|\in ℝ\wedge 0\le \left|{J}\right|\wedge \left|{J}\right|<{R}\right)\right)$
32 24 30 31 mp2an ${⊢}\left|{J}\right|\in \left[0,{R}\right)↔\left(\left|{J}\right|\in ℝ\wedge 0\le \left|{J}\right|\wedge \left|{J}\right|<{R}\right)$
33 32 simp3bi ${⊢}\left|{J}\right|\in \left[0,{R}\right)\to \left|{J}\right|<{R}$
34 23 33 syl ${⊢}{J}\in {D}\to \left|{J}\right|<{R}$
35 34 adantl ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to \left|{J}\right|<{R}$
36 6 14 7 22 35 radcnvlt2 ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to seq0\left(+,{S}\left({J}\right)\right)\in \mathrm{dom}⇝$
37 8 a1i ${⊢}\left({\phi }\wedge {J}\in ℂ\right)\to {E}=\left({b}\in ℂ⟼\left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)\right)$
38 simplr ${⊢}\left(\left(\left({\phi }\wedge {J}\in ℂ\right)\wedge {b}={J}\right)\wedge {k}\in ℕ\right)\to {b}={J}$
39 38 oveq1d ${⊢}\left(\left(\left({\phi }\wedge {J}\in ℂ\right)\wedge {b}={J}\right)\wedge {k}\in ℕ\right)\to {{b}}^{{k}-1}={{J}}^{{k}-1}$
40 39 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {J}\in ℂ\right)\wedge {b}={J}\right)\wedge {k}\in ℕ\right)\to {k}{F}\left({k}\right){{b}}^{{k}-1}={k}{F}\left({k}\right){{J}}^{{k}-1}$
41 40 mpteq2dva ${⊢}\left(\left({\phi }\wedge {J}\in ℂ\right)\wedge {b}={J}\right)\to \left({k}\in ℕ⟼{k}{F}\left({k}\right){{b}}^{{k}-1}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)$
42 simpr ${⊢}\left({\phi }\wedge {J}\in ℂ\right)\to {J}\in ℂ$
43 nnex ${⊢}ℕ\in \mathrm{V}$
44 43 mptex ${⊢}\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)\in \mathrm{V}$
45 44 a1i ${⊢}\left({\phi }\wedge {J}\in ℂ\right)\to \left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)\in \mathrm{V}$
46 37 41 42 45 fvmptd ${⊢}\left({\phi }\wedge {J}\in ℂ\right)\to {E}\left({J}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)$
47 21 46 sylan2 ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to {E}\left({J}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)$
48 47 seqeq3d ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to seq1\left(+,{E}\left({J}\right)\right)=seq1\left(+,\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)\right)$
49 eqid ${⊢}\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)=\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)$
50 6 7 49 14 22 35 dvradcnv2 ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to seq1\left(+,\left({k}\in ℕ⟼{k}{F}\left({k}\right){{J}}^{{k}-1}\right)\right)\in \mathrm{dom}⇝$
51 48 50 eqeltrd ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to seq1\left(+,{E}\left({J}\right)\right)\in \mathrm{dom}⇝$
52 36 51 jca ${⊢}\left({\phi }\wedge {J}\in {D}\right)\to \left(seq0\left(+,{S}\left({J}\right)\right)\in \mathrm{dom}⇝\wedge seq1\left(+,{E}\left({J}\right)\right)\in \mathrm{dom}⇝\right)$