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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
binomcxplem.f ⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
binomcxplem.s ⊢ 𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
binomcxplem.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
binomcxplem.e ⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
binomcxplem.d ⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
binomcxplem.p ⊢ 𝑃 = ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) )
Assertion binomcxplemdvsum ( 𝜑 → ( ℂ D 𝑃 ) = ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 binomcxp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4 binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 binomcxplem.f ⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
6 binomcxplem.s ⊢ 𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
7 binomcxplem.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
8 binomcxplem.e ⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
9 binomcxplem.d ⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
10 binomcxplem.p ⊢ 𝑃 = ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) )
11 nfcv ⊢ Ⅎ 𝑏 ◡ abs
12 nfcv ⊢ Ⅎ 𝑏 0
13 nfcv ⊢ Ⅎ 𝑏 [,)
14 nfcv ⊢ Ⅎ 𝑏 +
15 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
16 6 15 nfcxfr ⊢ Ⅎ 𝑏 𝑆
17 nfcv ⊢ Ⅎ 𝑏 𝑟
18 16 17 nffv ⊢ Ⅎ 𝑏 ( 𝑆 ‘ 𝑟 )
19 12 14 18 nfseq ⊢ Ⅎ 𝑏 seq 0 ( + , ( 𝑆 ‘ 𝑟 ) )
20 19 nfel1 ⊢ Ⅎ 𝑏 seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝
21 nfcv ⊢ Ⅎ 𝑏 ℝ
22 20 21 nfrabw ⊢ Ⅎ 𝑏 { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ }
23 nfcv ⊢ Ⅎ 𝑏 ℝ*
24 nfcv ⊢ Ⅎ 𝑏 <
25 22 23 24 nfsup ⊢ Ⅎ 𝑏 sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
26 7 25 nfcxfr ⊢ Ⅎ 𝑏 𝑅
27 12 13 26 nfov ⊢ Ⅎ 𝑏 ( 0 [,) 𝑅 )
28 11 27 nfima ⊢ Ⅎ 𝑏 ( ◡ abs “ ( 0 [,) 𝑅 ) )
29 9 28 nfcxfr ⊢ Ⅎ 𝑏 𝐷
30 nfcv ⊢ Ⅎ 𝑦 𝐷
31 nfcv ⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 )
32 nfcv ⊢ Ⅎ 𝑏 ℕ0
33 nfcv ⊢ Ⅎ 𝑏 𝑦
34 16 33 nffv ⊢ Ⅎ 𝑏 ( 𝑆 ‘ 𝑦 )
35 nfcv ⊢ Ⅎ 𝑏 𝑚
36 34 35 nffv ⊢ Ⅎ 𝑏 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 )
37 32 36 nfsum ⊢ Ⅎ 𝑏 Σ 𝑚 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 )
38 simpl ⊢ ( ( 𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0 ) → 𝑏 = 𝑦 )
39 38 fveq2d ⊢ ( ( 𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ 𝑦 ) )
40 39 fveq1d ⊢ ( ( 𝑏 = 𝑦 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑘 ) )
41 40 sumeq2dv ⊢ ( 𝑏 = 𝑦 → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑘 ) )
42 nfcv ⊢ Ⅎ 𝑚 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑘 )
43 nfcv ⊢ Ⅎ 𝑘 ℂ
44 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) )
45 43 44 nfmpt ⊢ Ⅎ 𝑘 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
46 6 45 nfcxfr ⊢ Ⅎ 𝑘 𝑆
47 nfcv ⊢ Ⅎ 𝑘 𝑦
48 46 47 nffv ⊢ Ⅎ 𝑘 ( 𝑆 ‘ 𝑦 )
49 nfcv ⊢ Ⅎ 𝑘 𝑚
50 48 49 nffv ⊢ Ⅎ 𝑘 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 )
51 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 ) )
52 42 50 51 cbvsumi ⊢ Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑚 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 )
53 41 52 eqtrdi ⊢ ( 𝑏 = 𝑦 → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) = Σ 𝑚 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 ) )
54 29 30 31 37 53 cbvmptf ⊢ ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 𝑏 ) ‘ 𝑘 ) ) = ( 𝑦 ∈ 𝐷 ↦ Σ 𝑚 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 ) )
55 10 54 eqtri ⊢ 𝑃 = ( 𝑦 ∈ 𝐷 ↦ Σ 𝑚 ∈ ℕ0 ( ( 𝑆 ‘ 𝑦 ) ‘ 𝑚 ) )
56 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑗 ) ∈ V )
57 5 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
58 5 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
59 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
60 59 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 𝑘 ) )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
62 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
63 62 61 bcccl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
64 58 60 61 63 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
65 64 63 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
66 56 57 65 fmpt2d ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ℂ )
67 nfcv ⊢ Ⅎ 𝑟 ℝ
68 nfcv ⊢ Ⅎ 𝑧 ℝ
69 nfv ⊢ Ⅎ 𝑧 seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝
70 nfcv ⊢ Ⅎ 𝑟 0
71 nfcv ⊢ Ⅎ 𝑟 +
72 nfcv ⊢ Ⅎ 𝑟 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
73 6 72 nfcxfr ⊢ Ⅎ 𝑟 𝑆
74 nfcv ⊢ Ⅎ 𝑟 𝑧
75 73 74 nffv ⊢ Ⅎ 𝑟 ( 𝑆 ‘ 𝑧 )
76 70 71 75 nfseq ⊢ Ⅎ 𝑟 seq 0 ( + , ( 𝑆 ‘ 𝑧 ) )
77 76 nfel1 ⊢ Ⅎ 𝑟 seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝
78 fveq2 ⊢ ( 𝑟 = 𝑧 → ( 𝑆 ‘ 𝑟 ) = ( 𝑆 ‘ 𝑧 ) )
79 78 seqeq3d ⊢ ( 𝑟 = 𝑧 → seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) )
80 79 eleq1d ⊢ ( 𝑟 = 𝑧 → ( seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ ) )
81 67 68 69 77 80 cbvrabw ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ }
82 81 supeq1i ⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < )
83 7 82 eqtri ⊢ 𝑅 = sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < )
84 6 fveq1i ⊢ ( 𝑆 ‘ 𝑧 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 )
85 seqeq3 ⊢ ( ( 𝑆 ‘ 𝑧 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) → seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) )
86 84 85 ax-mp ⊢ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) )
87 86 eleq1i ⊢ ( seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ )
88 87 rabbii ⊢ { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ } = { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ }
89 88 supeq1i ⊢ sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < )
90 7 82 89 3eqtrri ⊢ sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) = 𝑅
91 90 eleq1i ⊢ ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ ↔ 𝑅 ∈ ℝ )
92 90 oveq2i ⊢ ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) = ( ( abs ‘ 𝑥 ) + 𝑅 )
93 92 oveq1i ⊢ ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) = ( ( ( abs ‘ 𝑥 ) + 𝑅 ) / 2 )
94 eqid ⊢ ( ( abs ‘ 𝑥 ) + 1 ) = ( ( abs ‘ 𝑥 ) + 1 )
95 91 93 94 ifbieq12i ⊢ if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) )
96 oveq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 ↑ 𝑘 ) = ( 𝑏 ↑ 𝑘 ) )
97 96 oveq2d ⊢ ( 𝑤 = 𝑏 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) )
98 97 mpteq2dv ⊢ ( 𝑤 = 𝑏 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
99 98 cbvmptv ⊢ ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
100 99 fveq1i ⊢ ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 )
101 seqeq3 ⊢ ( ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) = ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) → seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) )
102 100 101 ax-mp ⊢ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) = seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) )
103 102 eleq1i ⊢ ( seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ )
104 103 rabbii ⊢ { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } = { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ }
105 104 supeq1i ⊢ sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < )
106 105 eleq1i ⊢ ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ ↔ sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ )
107 105 oveq2i ⊢ ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) = ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) )
108 107 oveq1i ⊢ ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) = ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 )
109 106 108 94 ifbieq12i ⊢ if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) = if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) )
110 109 oveq2i ⊢ ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) ) = ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) )
111 110 oveq1i ⊢ ( ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) ) / 2 ) = ( ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) ) / 2 )
112 111 oveq2i ⊢ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑤 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑤 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑥 ) + if ( sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑥 ) + sup ( { 𝑧 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) ‘ 𝑧 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑥 ) + 1 ) ) ) / 2 ) )
113 6 55 66 83 9 95 112 pserdv2 ⊢ ( 𝜑 → ( ℂ D 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ) )
114 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
115 9 114 eqsstri ⊢ 𝐷 ⊆ dom abs
116 absf ⊢ abs : ℂ ⟶ ℝ
117 116 fdmi ⊢ dom abs = ℂ
118 115 117 sseqtri ⊢ 𝐷 ⊆ ℂ
119 118 sseli ⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ )
120 8 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ) )
121 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑏 = 𝑦 ) ∧ 𝑘 ∈ ℕ ) → 𝑏 = 𝑦 )
122 121 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑏 = 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 ↑ ( 𝑘 − 1 ) ) = ( 𝑦 ↑ ( 𝑘 − 1 ) ) )
123 122 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑏 = 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) )
124 123 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑏 = 𝑦 ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) )
125 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
126 nnex ⊢ ℕ ∈ V
127 126 mptex ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V
128 127 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V )
129 120 124 125 128 fvmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐸 ‘ 𝑦 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) )
130 129 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑦 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) ) )
131 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → 𝑘 = 𝑛 )
132 131 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
133 131 132 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) )
134 131 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝑘 − 1 ) = ( 𝑛 − 1 ) )
135 134 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝑦 ↑ ( 𝑘 − 1 ) ) = ( 𝑦 ↑ ( 𝑛 − 1 ) ) )
136 133 135 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑦 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) )
137 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
138 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ∈ V )
139 130 136 137 138 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) )
140 139 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) )
141 119 140 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) )
142 141 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) ) = ( 𝑦 ∈ 𝐷 ↦ Σ 𝑛 ∈ ℕ ( ( 𝑛 · ( 𝐹 ‘ 𝑛 ) ) · ( 𝑦 ↑ ( 𝑛 − 1 ) ) ) ) )
143 113 142 eqtr4d ⊢ ( 𝜑 → ( ℂ D 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) ) )
144 nfcv ⊢ Ⅎ 𝑏 ℕ
145 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
146 8 145 nfcxfr ⊢ Ⅎ 𝑏 𝐸
147 146 33 nffv ⊢ Ⅎ 𝑏 ( 𝐸 ‘ 𝑦 )
148 nfcv ⊢ Ⅎ 𝑏 𝑛
149 147 148 nffv ⊢ Ⅎ 𝑏 ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 )
150 144 149 nfsum ⊢ Ⅎ 𝑏 Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 )
151 nfcv ⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 )
152 simpl ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ ) → 𝑦 = 𝑏 )
153 152 fveq2d ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑦 ) = ( 𝐸 ‘ 𝑏 ) )
154 153 fveq1d ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑛 ) )
155 154 sumeq2dv ⊢ ( 𝑦 = 𝑏 → Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑛 ) )
156 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
157 43 156 nfmpt ⊢ Ⅎ 𝑘 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
158 8 157 nfcxfr ⊢ Ⅎ 𝑘 𝐸
159 nfcv ⊢ Ⅎ 𝑘 𝑏
160 158 159 nffv ⊢ Ⅎ 𝑘 ( 𝐸 ‘ 𝑏 )
161 nfcv ⊢ Ⅎ 𝑘 𝑛
162 160 161 nffv ⊢ Ⅎ 𝑘 ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑛 )
163 nfcv ⊢ Ⅎ 𝑛 ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 )
164 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 ) )
165 162 163 164 cbvsumi ⊢ Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑛 ) = Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 )
166 155 165 eqtrdi ⊢ ( 𝑦 = 𝑏 → Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) = Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 ) )
167 30 29 150 151 166 cbvmptf ⊢ ( 𝑦 ∈ 𝐷 ↦ Σ 𝑛 ∈ ℕ ( ( 𝐸 ‘ 𝑦 ) ‘ 𝑛 ) ) = ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 ) )
168 143 167 eqtrdi ⊢ ( 𝜑 → ( ℂ D 𝑃 ) = ( 𝑏 ∈ 𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸 ‘ 𝑏 ) ‘ 𝑘 ) ) )