Metamath Proof Explorer

Theorem pserdvlem2

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-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 pserdvlem2 ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ℂ 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 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ℂ ∈ { ℝ , ℂ } )
11 0zd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℤ )
12 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 0 ... 𝑘 ) ∈ Fin )
13 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ℂ )
14 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
15 0cnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ∈ ℂ )
16 1 2 3 4 5 6 pserdvlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 ) )
17 16 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ+ )
18 17 rpxrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* )
19 blssm ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ℂ )
20 14 15 18 19 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ℂ )
21 7 20 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ⊆ ℂ )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℂ )
23 22 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
24 1 13 23 psergf ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) : ℕ0 ⟶ ℂ )
25 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑘 ) → 𝑖 ∈ ℕ0 )
26 ffvelcdm ⊢ ( ( ( 𝐺 ‘ 𝑦 ) : ℕ0 ⟶ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ∈ ℂ )
27 24 25 26 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ∈ ℂ )
28 12 27 fsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ∈ ℂ )
29 28 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) : 𝐵 ⟶ ℂ )
30 cnex ⊢ ℂ ∈ V
31 7 ovexi ⊢ 𝐵 ∈ V
32 30 31 elmap ⊢ ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) : 𝐵 ⟶ ℂ )
33 29 32 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝐵 ) )
34 33 fmpttd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) : ℕ0 ⟶ ( ℂ ↑m 𝐵 ) )
35 1 2 3 4 5 6 psercn ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )
36 cncff ⊢ ( 𝐹 ∈ ( 𝑆 –cn→ ℂ ) → 𝐹 : 𝑆 ⟶ ℂ )
37 35 36 syl ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
39 1 2 3 4 5 16 psercnlem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑎 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ∧ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) ∧ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) ⊆ 𝑆 ) )
40 39 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ⊆ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) )
41 7 40 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ⊆ ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) )
42 39 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ◡ abs “ ( 0 [,] ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ) ⊆ 𝑆 )
43 41 42 sstrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ⊆ 𝑆 )
44 38 43 fssresd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℂ )
45 0zd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 0 ∈ ℤ )
46 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
47 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ℂ )
48 21 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℂ )
49 1 47 48 psergf ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑧 ) : ℕ0 ⟶ ℂ )
50 49 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) ∈ ℂ )
51 48 abscld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ‘ 𝑧 ) ∈ ℝ )
52 51 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ‘ 𝑧 ) ∈ ℝ* )
53 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* )
54 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
55 1 3 4 radcnvcl ⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
56 54 55 sselid ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑅 ∈ ℝ* )
58 0cn ⊢ 0 ∈ ℂ
59 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
60 59 cnmetdval ⊢ ( ( 𝑧 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑧 − 0 ) ) )
61 48 58 60 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑧 − 0 ) ) )
62 48 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 − 0 ) = 𝑧 )
63 62 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ‘ ( 𝑧 − 0 ) ) = ( abs ‘ 𝑧 ) )
64 61 63 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑧 ) )
65 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
66 65 7 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
67 14 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
68 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 0 ∈ ℂ )
69 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ↔ ( 𝑧 ( abs ∘ − ) 0 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
70 67 53 68 48 69 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ↔ ( 𝑧 ( abs ∘ − ) 0 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) )
71 66 70 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ( abs ∘ − ) 0 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) )
72 64 71 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ‘ 𝑧 ) < ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) )
73 16 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑅 )
75 52 53 57 72 74 xrlttrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( abs ‘ 𝑧 ) < 𝑅 )
76 1 47 4 48 75 radcnvlt2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ∈ dom ⇝ )
77 8 45 46 50 76 isumclim2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ⇝ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
78 43 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝑆 )
79 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) )
80 79 fveq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
81 80 sumeq2sdv ⊢ ( 𝑦 = 𝑧 → Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
82 sumex ⊢ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) ∈ V
83 81 2 82 fvmpt ⊢ ( 𝑧 ∈ 𝑆 → ( 𝐹 ‘ 𝑧 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
84 78 83 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑗 ) )
85 77 84 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ⇝ ( 𝐹 ‘ 𝑧 ) )
86 oveq2 ⊢ ( 𝑘 = 𝑚 → ( 0 ... 𝑘 ) = ( 0 ... 𝑚 ) )
87 86 sumeq1d ⊢ ( 𝑘 = 𝑚 → Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) )
88 87 mpteq2dv ⊢ ( 𝑘 = 𝑚 → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) )
89 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) )
90 31 mptex ⊢ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ∈ V
91 88 89 90 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) )
92 91 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) )
93 92 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ‘ 𝑧 ) = ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ‘ 𝑧 ) )
94 79 fveq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) )
95 94 sumeq2sdv ⊢ ( 𝑦 = 𝑧 → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) )
96 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) )
97 sumex ⊢ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) ∈ V
98 95 96 97 fvmpt ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ‘ 𝑧 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) )
99 98 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ‘ 𝑧 ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) )
100 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) )
101 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
102 101 8 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
103 49 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑧 ) : ℕ0 ⟶ ℂ )
104 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → 𝑖 ∈ ℕ0 )
105 ffvelcdm ⊢ ( ( ( 𝐺 ‘ 𝑧 ) : ℕ0 ⟶ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) ∈ ℂ )
106 103 104 105 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) ∈ ℂ )
107 100 102 106 fsumser ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑖 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ‘ 𝑚 ) )
108 93 99 107 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ‘ 𝑧 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ‘ 𝑚 ) )
109 108 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
110 0z ⊢ 0 ∈ ℤ
111 seqfn ⊢ ( 0 ∈ ℤ → seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ( ℤ≥ ‘ 0 ) )
112 110 111 ax-mp ⊢ seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ( ℤ≥ ‘ 0 )
113 8 fneq2i ⊢ ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ℕ0 ↔ seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ( ℤ≥ ‘ 0 ) )
114 112 113 mpbir ⊢ seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ℕ0
115 dffn5 ⊢ ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) Fn ℕ0 ↔ seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
116 114 115 mpbi ⊢ seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) ‘ 𝑚 ) )
117 109 116 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ‘ 𝑧 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑧 ) ) )
118 fvres ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
119 118 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
120 85 117 119 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑚 ∈ ℕ0 ↦ ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ‘ 𝑧 ) ) ⇝ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) )
121 91 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) )
122 121 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ℂ D ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ) = ( ℂ D ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) )
123 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
124 123 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
125 124 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
126 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ℂ ∈ { ℝ , ℂ } )
127 123 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
128 127 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ∈ ( TopOpen ‘ ℂfld ) )
129 14 15 18 128 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 0 ( ball ‘ ( abs ∘ − ) ) ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ) ∈ ( TopOpen ‘ ℂfld ) )
130 7 129 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐵 ∈ ( TopOpen ‘ ℂfld ) )
131 130 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐵 ∈ ( TopOpen ‘ ℂfld ) )
132 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 0 ... 𝑚 ) ∈ Fin )
133 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
134 133 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ℂ )
135 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐵 ⊆ ℂ )
136 135 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
137 136 3adant2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
138 1 134 137 psergf ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) : ℕ0 ⟶ ℂ )
139 104 3ad2ant2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑖 ∈ ℕ0 )
140 138 139 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ∈ ℂ )
141 9 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ℂ ∈ { ℝ , ℂ } )
142 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
143 133 104 142 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
144 143 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
145 136 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
146 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
147 104 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → 𝑖 ∈ ℕ0 )
148 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑖 ) ∈ ℂ )
149 146 147 148 syl2anr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑖 ) ∈ ℂ )
150 145 149 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ↑ 𝑖 ) ∈ ℂ )
151 144 150 mulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ∈ ℂ )
152 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ V )
153 c0ex ⊢ 0 ∈ V
154 ovex ⊢ ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ∈ V
155 153 154 ifex ⊢ if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ∈ V
156 155 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ∈ V )
157 155 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ ℂ ) → if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ∈ V )
158 dvexp2 ⊢ ( 𝑖 ∈ ℕ0 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ ℂ ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) )
159 147 158 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ ℂ ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) )
160 21 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → 𝐵 ⊆ ℂ )
161 130 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → 𝐵 ∈ ( TopOpen ‘ ℂfld ) )
162 141 149 157 159 160 125 123 161 dvmptres ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ℂ D ( 𝑦 ∈ 𝐵 ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) )
163 141 150 156 162 143 dvmptcmul ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ℂ D ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) )
164 141 151 152 163 dvmptcl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ ℂ )
165 164 3impa ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ ℂ )
166 104 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑖 ∈ ℕ0 )
167 1 pserval2 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) )
168 145 166 167 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) )
169 168 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) )
170 169 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ℂ D ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) = ( ℂ D ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) ) )
171 170 163 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ℂ D ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) )
172 125 123 126 131 132 140 165 171 dvmptfsum ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ℂ D ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) )
173 122 172 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ℂ D ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) )
174 173 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ0 ↦ ( ℂ D ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) )
175 nnssnn0 ⊢ ℕ ⊆ ℕ0
176 resmpt ⊢ ( ℕ ⊆ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) )
177 175 176 ax-mp ⊢ ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) )
178 oveq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 ↑ 𝑖 ) = ( 𝑥 ↑ 𝑖 ) )
179 178 oveq2d ⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑥 ↑ 𝑖 ) ) )
180 179 mpteq2dv ⊢ ( 𝑎 = 𝑥 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑥 ↑ 𝑖 ) ) ) )
181 oveq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 + 1 ) = ( 𝑛 + 1 ) )
182 fvoveq1 ⊢ ( 𝑖 = 𝑛 → ( 𝐴 ‘ ( 𝑖 + 1 ) ) = ( 𝐴 ‘ ( 𝑛 + 1 ) ) )
183 181 182 oveq12d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
184 oveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝑥 ↑ 𝑖 ) = ( 𝑥 ↑ 𝑛 ) )
185 183 184 oveq12d ⊢ ( 𝑖 = 𝑛 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑥 ↑ 𝑖 ) ) = ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑥 ↑ 𝑛 ) ) )
186 185 cbvmptv ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑥 ↑ 𝑖 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑥 ↑ 𝑛 ) ) )
187 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
188 fvoveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝐴 ‘ ( 𝑚 + 1 ) ) = ( 𝐴 ‘ ( 𝑛 + 1 ) ) )
189 187 188 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) = ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
190 eqid ⊢ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) )
191 ovex ⊢ ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) ∈ V
192 189 190 191 fvmpt ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) = ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) )
193 192 oveq1d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑥 ↑ 𝑛 ) ) )
194 193 mpteq2ia ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑥 ↑ 𝑛 ) ) )
195 186 194 eqtr4i ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑥 ↑ 𝑖 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
196 180 195 eqtrdi ⊢ ( 𝑎 = 𝑥 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
197 196 cbvmptv ⊢ ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
198 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) )
199 198 fveq1d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ‘ 𝑘 ) )
200 199 sumeq2sdv ⊢ ( 𝑦 = 𝑧 → Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ‘ 𝑘 ) )
201 200 cbvmptv ⊢ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) ) = ( 𝑧 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ‘ 𝑘 ) )
202 peano2nn0 ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ0 )
203 202 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 + 1 ) ∈ ℕ0 )
204 203 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 + 1 ) ∈ ℂ )
205 133 203 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑚 + 1 ) ) ∈ ℂ )
206 204 205 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ∈ ℂ )
207 206 fmpttd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ0 ↦ ( ( 𝑚 + 1 ) · ( 𝐴 ‘ ( 𝑚 + 1 ) ) ) ) : ℕ0 ⟶ ℂ )
208 fveq2 ⊢ ( 𝑟 = 𝑗 → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) = ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑗 ) )
209 208 seqeq3d ⊢ ( 𝑟 = 𝑗 → seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) = seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑗 ) ) )
210 209 eleq1d ⊢ ( 𝑟 = 𝑗 → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑗 ) ) ∈ dom ⇝ ) )
211 210 cbvrabv ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑗 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑗 ) ) ∈ dom ⇝ }
212 211 supeq1i ⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑗 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑗 ) ) ∈ dom ⇝ } , ℝ* , < )
213 198 seqeq3d ⊢ ( 𝑦 = 𝑧 → seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) = seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) )
214 213 fveq1d ⊢ ( 𝑦 = 𝑧 → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑗 ) )
215 214 cbvmptv ⊢ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) = ( 𝑧 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑗 ) )
216 fveq2 ⊢ ( 𝑗 = 𝑚 → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑗 ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑚 ) )
217 216 mpteq2dv ⊢ ( 𝑗 = 𝑚 → ( 𝑧 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑗 ) ) = ( 𝑧 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
218 215 217 eqtrid ⊢ ( 𝑗 = 𝑚 → ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) = ( 𝑧 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
219 218 cbvmptv ⊢ ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
220 17 rpred ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) ∈ ℝ )
221 1 2 3 4 5 6 psercnlem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
222 221 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ+ )
223 222 rpxrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ* )
224 197 207 212 radcnvcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
225 54 224 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
226 221 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
227 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
228 absf ⊢ abs : ℂ ⟶ ℝ
229 228 fdmi ⊢ dom abs = ℂ
230 227 229 sseqtri ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
231 5 230 eqsstri ⊢ 𝑆 ⊆ ℂ
232 231 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
233 232 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ ℂ )
234 233 abscld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑎 ) ∈ ℝ )
235 222 rpred ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
236 avglt2 ⊢ ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 ) )
237 234 235 236 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( abs ‘ 𝑎 ) < 𝑀 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 ) )
238 226 237 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < 𝑀 )
239 222 rpge0d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 0 ≤ 𝑀 )
240 235 239 absidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑀 ) = 𝑀 )
241 222 rpcnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ∈ ℂ )
242 oveq1 ⊢ ( 𝑤 = 𝑀 → ( 𝑤 ↑ 𝑖 ) = ( 𝑀 ↑ 𝑖 ) )
243 242 oveq2d ⊢ ( 𝑤 = 𝑀 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑤 ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) )
244 243 mpteq2dv ⊢ ( 𝑤 = 𝑀 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑤 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) )
245 oveq1 ⊢ ( 𝑎 = 𝑤 → ( 𝑎 ↑ 𝑖 ) = ( 𝑤 ↑ 𝑖 ) )
246 245 oveq2d ⊢ ( 𝑎 = 𝑤 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑤 ↑ 𝑖 ) ) )
247 246 mpteq2dv ⊢ ( 𝑎 = 𝑤 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑤 ↑ 𝑖 ) ) ) )
248 247 cbvmptv ⊢ ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) = ( 𝑤 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑤 ↑ 𝑖 ) ) ) )
249 nn0ex ⊢ ℕ0 ∈ V
250 249 mptex ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) ∈ V
251 244 248 250 fvmpt ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑀 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) )
252 241 251 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑀 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) )
253 252 seqeq3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑀 ) ) = seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) ) )
254 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑖 ) )
255 oveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑖 ) )
256 254 255 oveq12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑥 ↑ 𝑖 ) ) )
257 256 cbvmptv ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑥 ↑ 𝑖 ) ) )
258 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝑖 ) = ( 𝑦 ↑ 𝑖 ) )
259 258 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ‘ 𝑖 ) · ( 𝑥 ↑ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) )
260 259 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑥 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) )
261 257 260 eqtrid ⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) )
262 261 cbvmptv ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) )
263 1 262 eqtri ⊢ 𝐺 = ( 𝑦 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑖 ) · ( 𝑦 ↑ 𝑖 ) ) ) )
264 fveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑠 ) )
265 264 seqeq3d ⊢ ( 𝑟 = 𝑠 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) )
266 265 eleq1d ⊢ ( 𝑟 = 𝑠 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ) )
267 266 cbvrabv ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ }
268 267 supeq1i ⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ } , ℝ* , < )
269 4 268 eqtri ⊢ 𝑅 = sup ( { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ } , ℝ* , < )
270 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) )
271 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
272 221 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 < 𝑅 )
273 240 272 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑀 ) < 𝑅 )
274 263 269 270 271 241 273 dvradcnv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑀 ↑ 𝑖 ) ) ) ) ∈ dom ⇝ )
275 253 274 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑀 ) ) ∈ dom ⇝ )
276 197 207 212 241 275 radcnvle ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( abs ‘ 𝑀 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
277 240 276 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑀 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
278 18 223 225 238 277 xrltletrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( abs ‘ 𝑎 ) + 𝑀 ) / 2 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
279 197 201 207 212 219 220 278 41 pserulm ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) ) )
280 21 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
281 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 ↑ 𝑖 ) = ( 𝑦 ↑ 𝑖 ) )
282 281 oveq2d ⊢ ( 𝑎 = 𝑦 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) )
283 282 mpteq2dv ⊢ ( 𝑎 = 𝑦 → ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) )
284 eqid ⊢ ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) = ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) )
285 249 mptex ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ∈ V
286 283 284 285 fvmpt ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) )
287 280 286 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) )
288 287 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) )
289 288 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ‘ 𝑘 ) )
290 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 + 1 ) = ( 𝑘 + 1 ) )
291 fvoveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝐴 ‘ ( 𝑖 + 1 ) ) = ( 𝐴 ‘ ( 𝑘 + 1 ) ) )
292 290 291 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
293 oveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑦 ↑ 𝑖 ) = ( 𝑦 ↑ 𝑘 ) )
294 292 293 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
295 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) )
296 ovex ⊢ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ∈ V
297 294 295 296 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
298 297 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
299 289 298 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
300 299 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
301 300 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
302 279 301 breqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
303 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
304 1e0p1 ⊢ 1 = ( 0 + 1 )
305 304 fveq2i ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ ( 0 + 1 ) )
306 303 305 eqtri ⊢ ℕ = ( ℤ≥ ‘ ( 0 + 1 ) )
307 1zzd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 1 ∈ ℤ )
308 0zd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → 0 ∈ ℤ )
309 peano2nn0 ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℕ0 )
310 309 nn0cnd ⊢ ( 𝑖 ∈ ℕ0 → ( 𝑖 + 1 ) ∈ ℂ )
311 310 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 + 1 ) ∈ ℂ )
312 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ℂ )
313 ffvelcdm ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ ( 𝑖 + 1 ) ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
314 312 309 313 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
315 311 314 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) ∈ ℂ )
316 280 148 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑖 ) ∈ ℂ )
317 315 316 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ∈ ℂ )
318 287 317 fmpt3d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) : ℕ0 ⟶ ℂ )
319 318 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑚 ) ∈ ℂ )
320 8 308 319 serf ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) : ℕ0 ⟶ ℂ )
321 320 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ∈ ℂ )
322 321 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ∈ ℂ )
323 322 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) : 𝐵 ⟶ ℂ )
324 30 31 elmap ⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ∈ ( ℂ ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) : 𝐵 ⟶ ℂ )
325 323 324 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ∈ ( ℂ ↑m 𝐵 ) )
326 325 fmpttd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) : ℕ0 ⟶ ( ℂ ↑m 𝐵 ) )
327 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → 𝑖 ∈ ℕ )
328 327 nnne0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → 𝑖 ≠ 0 )
329 328 neneqd ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → ¬ 𝑖 = 0 )
330 329 iffalsed ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) = ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) )
331 330 oveq2d ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) )
332 331 sumeq2i ⊢ Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) )
333 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → 1 ∈ ℤ )
334 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
335 334 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑚 ∈ ℤ )
336 271 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ℂ )
337 327 nnnn0d ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → 𝑖 ∈ ℕ0 )
338 336 337 142 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
339 327 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ℕ )
340 339 nncnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ℂ )
341 280 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℂ )
342 nnm1nn0 ⊢ ( 𝑖 ∈ ℕ → ( 𝑖 − 1 ) ∈ ℕ0 )
343 327 342 syl ⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) → ( 𝑖 − 1 ) ∈ ℕ0 )
344 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑖 − 1 ) ∈ ℕ0 ) → ( 𝑦 ↑ ( 𝑖 − 1 ) ) ∈ ℂ )
345 341 343 344 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑦 ↑ ( 𝑖 − 1 ) ) ∈ ℂ )
346 340 345 mulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ∈ ℂ )
347 338 346 mulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ∈ ℂ )
348 fveq2 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ ( 𝑘 + 1 ) ) )
349 id ⊢ ( 𝑖 = ( 𝑘 + 1 ) → 𝑖 = ( 𝑘 + 1 ) )
350 oveq1 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
351 350 oveq2d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑦 ↑ ( 𝑖 − 1 ) ) = ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) )
352 349 351 oveq12d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) )
353 348 352 oveq12d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
354 333 333 335 347 353 fsumshftm ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) = Σ 𝑘 ∈ ( ( 1 − 1 ) ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
355 332 354 eqtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( ( 1 − 1 ) ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
356 fz1ssfz0 ⊢ ( 1 ... 𝑚 ) ⊆ ( 0 ... 𝑚 )
357 356 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → ( 1 ... 𝑚 ) ⊆ ( 0 ... 𝑚 ) )
358 331 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = ( ( 𝐴 ‘ 𝑖 ) · ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) )
359 358 347 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ ℂ )
360 eldif ⊢ ( 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( ( 0 + 1 ) ... 𝑚 ) ) ↔ ( 𝑖 ∈ ( 0 ... 𝑚 ) ∧ ¬ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) )
361 elfzuz2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
362 elfzp12 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑖 ∈ ( 0 ... 𝑚 ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) ) )
363 361 362 syl ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → ( 𝑖 ∈ ( 0 ... 𝑚 ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) ) )
364 363 ibi ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) )
365 364 ord ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → ( ¬ 𝑖 = 0 → 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) )
366 365 con1d ⊢ ( 𝑖 ∈ ( 0 ... 𝑚 ) → ( ¬ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) → 𝑖 = 0 ) )
367 366 imp ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑚 ) ∧ ¬ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑚 ) ) → 𝑖 = 0 )
368 360 367 sylbi ⊢ ( 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( ( 0 + 1 ) ... 𝑚 ) ) → 𝑖 = 0 )
369 304 oveq1i ⊢ ( 1 ... 𝑚 ) = ( ( 0 + 1 ) ... 𝑚 )
370 369 difeq2i ⊢ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) = ( ( 0 ... 𝑚 ) ∖ ( ( 0 + 1 ) ... 𝑚 ) )
371 368 370 eleq2s ⊢ ( 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) → 𝑖 = 0 )
372 371 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → 𝑖 = 0 )
373 372 iftrued ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) = 0 )
374 373 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = ( ( 𝐴 ‘ 𝑖 ) · 0 ) )
375 eldifi ⊢ ( 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ( 0 ... 𝑚 ) )
376 375 104 syl ⊢ ( 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ℕ0 )
377 336 376 142 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
378 377 mul01d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → ( ( 𝐴 ‘ 𝑖 ) · 0 ) = 0 )
379 374 378 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 0 ... 𝑚 ) ∖ ( 1 ... 𝑚 ) ) ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = 0 )
380 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → ( 0 ... 𝑚 ) ∈ Fin )
381 357 359 379 380 fsumss ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) )
382 1m1e0 ⊢ ( 1 − 1 ) = 0
383 382 oveq1i ⊢ ( ( 1 − 1 ) ... ( 𝑚 − 1 ) ) = ( 0 ... ( 𝑚 − 1 ) )
384 383 sumeq1i ⊢ Σ 𝑘 ∈ ( ( 1 − 1 ) ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) )
385 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) → 𝑘 ∈ ℕ0 )
386 385 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
387 386 297 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
388 341 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → 𝑦 ∈ ℂ )
389 388 286 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) )
390 389 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑦 ↑ 𝑖 ) ) ) ‘ 𝑘 ) )
391 336 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → 𝐴 : ℕ0 ⟶ ℂ )
392 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
393 386 392 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
394 391 393 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
395 393 nn0cnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ℂ )
396 expcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
397 341 385 396 syl2an ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
398 394 395 397 mul12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
399 386 nn0cnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → 𝑘 ∈ ℂ )
400 ax-1cn ⊢ 1 ∈ ℂ
401 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
402 399 400 401 sylancl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
403 402 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( 𝑦 ↑ 𝑘 ) )
404 403 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝑦 ↑ 𝑘 ) ) )
405 404 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ 𝑘 ) ) ) )
406 395 394 397 mulassd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) = ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
407 398 405 406 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) )
408 387 390 407 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) )
409 nnm1nn0 ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 − 1 ) ∈ ℕ0 )
410 409 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 − 1 ) ∈ ℕ0 )
411 410 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑚 − 1 ) ∈ ℕ0 )
412 411 8 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑚 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
413 403 397 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ∈ ℂ )
414 395 413 mulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ∈ ℂ )
415 394 414 mulcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) ∈ ℂ )
416 408 412 415 fsumser ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) )
417 384 416 eqtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑘 ∈ ( ( 1 − 1 ) ... ( 𝑚 − 1 ) ) ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑘 + 1 ) · ( 𝑦 ↑ ( ( 𝑘 + 1 ) − 1 ) ) ) ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) )
418 355 381 417 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) )
419 418 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) ) )
420 fveq2 ⊢ ( 𝑗 = ( 𝑚 − 1 ) → ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) = ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) )
421 420 mpteq2dv ⊢ ( 𝑗 = ( 𝑚 − 1 ) → ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) ) )
422 eqid ⊢ ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) )
423 31 mptex ⊢ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) ) ∈ V
424 421 422 423 fvmpt ⊢ ( ( 𝑚 − 1 ) ∈ ℕ0 → ( ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ‘ ( 𝑚 − 1 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) ) )
425 410 424 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ‘ ( 𝑚 − 1 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ ( 𝑚 − 1 ) ) ) )
426 419 425 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) = ( ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ‘ ( 𝑚 − 1 ) ) )
427 426 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ‘ ( 𝑚 − 1 ) ) ) )
428 8 306 11 307 326 427 ulmshft ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑗 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ ( seq 0 ( + , ( ( 𝑎 ∈ ℂ ↦ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑖 + 1 ) · ( 𝐴 ‘ ( 𝑖 + 1 ) ) ) · ( 𝑎 ↑ 𝑖 ) ) ) ) ‘ 𝑦 ) ) ‘ 𝑗 ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ↔ ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
429 302 428 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
430 177 429 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ↾ ℕ ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
431 1nn0 ⊢ 1 ∈ ℕ0
432 431 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 1 ∈ ℕ0 )
433 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 0 ... 𝑚 ) ∈ Fin )
434 164 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ ℂ )
435 433 434 fsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ∈ ℂ )
436 435 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) : 𝐵 ⟶ ℂ )
437 30 31 elmap ⊢ ( ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ∈ ( ℂ ↑m 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) : 𝐵 ⟶ ℂ )
438 436 437 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ∈ ( ℂ ↑m 𝐵 ) )
439 438 fmpttd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) : ℕ0 ⟶ ( ℂ ↑m 𝐵 ) )
440 8 303 432 439 ulmres ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ↔ ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ↾ ℕ ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
441 430 440 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑚 ) ( ( 𝐴 ‘ 𝑖 ) · if ( 𝑖 = 0 , 0 , ( 𝑖 · ( 𝑦 ↑ ( 𝑖 − 1 ) ) ) ) ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
442 174 441 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝑚 ∈ ℕ0 ↦ ( ℂ D ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝐵 ↦ Σ 𝑖 ∈ ( 0 ... 𝑘 ) ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑖 ) ) ) ‘ 𝑚 ) ) ) ( ⇝𝑢 ‘ 𝐵 ) ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
443 8 10 11 34 44 120 442 ulmdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ℂ D ( 𝐹 ↾ 𝐵 ) ) = ( 𝑦 ∈ 𝐵 ↦ Σ 𝑘 ∈ ℕ0 ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )