Metamath Proof Explorer

Theorem pserdv

Description: The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses pserf.g ⊒ 𝐺 = ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
pserf.f ⊒ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) )
pserf.a ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
pserf.r ⊒ 𝑅 = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s ⊒ 𝑆 = ( β—‘ abs β€œ ( 0 [,) 𝑅 ) )
psercn.m ⊒ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs β€˜ π‘Ž ) + 𝑅 ) / 2 ) , ( ( abs β€˜ π‘Ž ) + 1 ) )
pserdv.b ⊒ 𝐡 = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
Assertion pserdv ( πœ‘ β†’ ( β„‚ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )

Proof

Step Hyp Ref Expression
1 pserf.g ⊒ 𝐺 = ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
2 pserf.f ⊒ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) )
3 pserf.a ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
4 pserf.r ⊒ 𝑅 = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
5 psercn.s ⊒ 𝑆 = ( β—‘ abs β€œ ( 0 [,) 𝑅 ) )
6 psercn.m ⊒ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs β€˜ π‘Ž ) + 𝑅 ) / 2 ) , ( ( abs β€˜ π‘Ž ) + 1 ) )
7 pserdv.b ⊒ 𝐡 = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
8 dvfcn ⊒ ( β„‚ D 𝐹 ) : dom ( β„‚ D 𝐹 ) ⟢ β„‚
9 ssidd ⊒ ( πœ‘ β†’ β„‚ βŠ† β„‚ )
10 1 2 3 4 5 6 psercn ⊒ ( πœ‘ β†’ 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) )
11 cncff ⊒ ( 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
12 10 11 syl ⊒ ( πœ‘ β†’ 𝐹 : 𝑆 ⟢ β„‚ )
13 cnvimass ⊒ ( β—‘ abs β€œ ( 0 [,) 𝑅 ) ) βŠ† dom abs
14 absf ⊒ abs : β„‚ ⟢ ℝ
15 14 fdmi ⊒ dom abs = β„‚
16 13 15 sseqtri ⊒ ( β—‘ abs β€œ ( 0 [,) 𝑅 ) ) βŠ† β„‚
17 5 16 eqsstri ⊒ 𝑆 βŠ† β„‚
18 17 a1i ⊒ ( πœ‘ β†’ 𝑆 βŠ† β„‚ )
19 9 12 18 dvbss ⊒ ( πœ‘ β†’ dom ( β„‚ D 𝐹 ) βŠ† 𝑆 )
20 ssidd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ β„‚ βŠ† β„‚ )
21 12 adantr ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
22 17 a1i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑆 βŠ† β„‚ )
23 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
24 0cnd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ∈ β„‚ )
25 18 sselda ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ β„‚ )
26 25 abscld ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ π‘Ž ) ∈ ℝ )
27 1 2 3 4 5 6 psercnlem1 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑀 ∈ ℝ+ ∧ ( abs β€˜ π‘Ž ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
28 27 simp1d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ ℝ+ )
29 28 rpred ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ ℝ )
30 26 29 readdcld ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( abs β€˜ π‘Ž ) + 𝑀 ) ∈ ℝ )
31 0red ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ∈ ℝ )
32 25 absge0d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ≀ ( abs β€˜ π‘Ž ) )
33 26 28 ltaddrpd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ π‘Ž ) < ( ( abs β€˜ π‘Ž ) + 𝑀 ) )
34 31 26 30 32 33 lelttrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 < ( ( abs β€˜ π‘Ž ) + 𝑀 ) )
35 30 34 elrpd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( abs β€˜ π‘Ž ) + 𝑀 ) ∈ ℝ+ )
36 35 rphalfcld ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ+ )
37 36 rpxrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* )
38 blssm ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† β„‚ )
39 23 24 37 38 mp3an2i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† β„‚ )
40 7 39 eqsstrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐡 βŠ† β„‚ )
41 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
42 41 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
43 42 toponrestid ⊒ ( TopOpen β€˜ β„‚fld ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt β„‚ )
44 41 43 dvres ⊒ ( ( ( β„‚ βŠ† β„‚ ∧ 𝐹 : 𝑆 ⟢ β„‚ ) ∧ ( 𝑆 βŠ† β„‚ ∧ 𝐡 βŠ† β„‚ ) ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = ( ( β„‚ D 𝐹 ) β†Ύ ( ( int β€˜ ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝐡 ) ) )
45 20 21 22 40 44 syl22anc ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = ( ( β„‚ D 𝐹 ) β†Ύ ( ( int β€˜ ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝐡 ) ) )
46 resss ⊒ ( ( β„‚ D 𝐹 ) β†Ύ ( ( int β€˜ ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝐡 ) ) βŠ† ( β„‚ D 𝐹 )
47 45 46 eqsstrdi ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) βŠ† ( β„‚ D 𝐹 ) )
48 dmss ⊒ ( ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) βŠ† ( β„‚ D 𝐹 ) β†’ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) βŠ† dom ( β„‚ D 𝐹 ) )
49 47 48 syl ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) βŠ† dom ( β„‚ D 𝐹 ) )
50 1 2 3 4 5 6 pserdvlem1 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ+ ∧ ( abs β€˜ π‘Ž ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑅 ) )
51 1 2 3 4 5 50 psercnlem2 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘Ž ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ∧ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) ∧ ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) βŠ† 𝑆 ) )
52 51 simp1d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) )
53 52 7 eleqtrrdi ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ 𝐡 )
54 1 2 3 4 5 6 7 pserdvlem2 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
55 54 dmeqd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = dom ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
56 dmmptg ⊒ ( βˆ€ 𝑦 ∈ 𝐡 Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ∈ V β†’ dom ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) = 𝐡 )
57 sumex ⊒ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ∈ V
58 57 a1i ⊒ ( 𝑦 ∈ 𝐡 β†’ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ∈ V )
59 56 58 mprg ⊒ dom ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) = 𝐡
60 55 59 eqtrdi ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = 𝐡 )
61 53 60 eleqtrrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) )
62 49 61 sseldd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ dom ( β„‚ D 𝐹 ) )
63 19 62 eqelssd ⊒ ( πœ‘ β†’ dom ( β„‚ D 𝐹 ) = 𝑆 )
64 63 feq2d ⊒ ( πœ‘ β†’ ( ( β„‚ D 𝐹 ) : dom ( β„‚ D 𝐹 ) ⟢ β„‚ ↔ ( β„‚ D 𝐹 ) : 𝑆 ⟢ β„‚ ) )
65 8 64 mpbii ⊒ ( πœ‘ β†’ ( β„‚ D 𝐹 ) : 𝑆 ⟢ β„‚ )
66 65 feqmptd ⊒ ( πœ‘ β†’ ( β„‚ D 𝐹 ) = ( π‘Ž ∈ 𝑆 ↦ ( ( β„‚ D 𝐹 ) β€˜ π‘Ž ) ) )
67 ffun ⊒ ( ( β„‚ D 𝐹 ) : dom ( β„‚ D 𝐹 ) ⟢ β„‚ β†’ Fun ( β„‚ D 𝐹 ) )
68 8 67 mp1i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ Fun ( β„‚ D 𝐹 ) )
69 funssfv ⊒ ( ( Fun ( β„‚ D 𝐹 ) ∧ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) βŠ† ( β„‚ D 𝐹 ) ∧ π‘Ž ∈ dom ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) ) β†’ ( ( β„‚ D 𝐹 ) β€˜ π‘Ž ) = ( ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) β€˜ π‘Ž ) )
70 68 47 61 69 syl3anc ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( β„‚ D 𝐹 ) β€˜ π‘Ž ) = ( ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) β€˜ π‘Ž ) )
71 54 fveq1d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) β€˜ π‘Ž ) = ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) β€˜ π‘Ž ) )
72 oveq1 ⊒ ( 𝑦 = π‘Ž β†’ ( 𝑦 ↑ π‘˜ ) = ( π‘Ž ↑ π‘˜ ) )
73 72 oveq2d ⊒ ( 𝑦 = π‘Ž β†’ ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) )
74 73 sumeq2sdv ⊒ ( 𝑦 = π‘Ž β†’ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) )
75 eqid ⊒ ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
76 sumex ⊒ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) ∈ V
77 74 75 76 fvmpt ⊒ ( π‘Ž ∈ 𝐡 β†’ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) β€˜ π‘Ž ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) )
78 53 77 syl ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) β€˜ π‘Ž ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) )
79 70 71 78 3eqtrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( β„‚ D 𝐹 ) β€˜ π‘Ž ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) )
80 79 mpteq2dva ⊒ ( πœ‘ β†’ ( π‘Ž ∈ 𝑆 ↦ ( ( β„‚ D 𝐹 ) β€˜ π‘Ž ) ) = ( π‘Ž ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) ) )
81 66 80 eqtrd ⊒ ( πœ‘ β†’ ( β„‚ D 𝐹 ) = ( π‘Ž ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) ) )
82 oveq1 ⊒ ( π‘Ž = 𝑦 β†’ ( π‘Ž ↑ π‘˜ ) = ( 𝑦 ↑ π‘˜ ) )
83 82 oveq2d ⊒ ( π‘Ž = 𝑦 β†’ ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
84 83 sumeq2sdv ⊒ ( π‘Ž = 𝑦 β†’ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
85 84 cbvmptv ⊒ ( π‘Ž ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( π‘Ž ↑ π‘˜ ) ) ) = ( 𝑦 ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
86 81 85 eqtrdi ⊒ ( πœ‘ β†’ ( β„‚ D 𝐹 ) = ( 𝑦 ∈ 𝑆 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )