Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pserdvlem2 Structured version   Visualization version   GIF version

Theorem pserdvlem2 25033
 Description: Lemma for pserdv 25034. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
pserf.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
pserf.f 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
pserf.a (𝜑𝐴:ℕ0⟶ℂ)
pserf.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
psercn.s 𝑆 = (abs “ (0[,)𝑅))
psercn.m 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
pserdv.b 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
Assertion
Ref Expression
pserdvlem2 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
Distinct variable groups:   𝑗,𝑎,𝑘,𝑛,𝑟,𝑥,𝑦,𝐴   𝑗,𝑀,𝑘,𝑦   𝐵,𝑗,𝑘,𝑥,𝑦   𝑗,𝐺,𝑘,𝑟,𝑦   𝑆,𝑎,𝑗,𝑘,𝑦   𝐹,𝑎   𝜑,𝑎,𝑗,𝑘,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝐵(𝑛,𝑟,𝑎)   𝑅(𝑥,𝑦,𝑗,𝑘,𝑛,𝑟,𝑎)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑗,𝑘,𝑛,𝑟)   𝐺(𝑥,𝑛,𝑎)   𝑀(𝑥,𝑛,𝑟,𝑎)

Proof of Theorem pserdvlem2
Dummy variables 𝑚 𝑠 𝑤 𝑧 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 12271 . 2 0 = (ℤ‘0)
2 cnelprrecn 10622 . . 3 ℂ ∈ {ℝ, ℂ}
32a1i 11 . 2 ((𝜑𝑎𝑆) → ℂ ∈ {ℝ, ℂ})
4 0zd 11984 . 2 ((𝜑𝑎𝑆) → 0 ∈ ℤ)
5 fzfid 13339 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑘) ∈ Fin)
6 pserf.g . . . . . . . 8 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
7 pserf.a . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℂ)
87ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
9 pserdv.b . . . . . . . . . . 11 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
10 cnxmet 23388 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
11 0cnd 10626 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 0 ∈ ℂ)
12 pserf.f . . . . . . . . . . . . . . 15 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
13 pserf.r . . . . . . . . . . . . . . 15 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
14 psercn.s . . . . . . . . . . . . . . 15 𝑆 = (abs “ (0[,)𝑅))
15 psercn.m . . . . . . . . . . . . . . 15 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
166, 12, 7, 13, 14, 15pserdvlem1 25032 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
1716simp1d 1139 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+)
1817rpxrd 12423 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
19 blssm 23035 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
2010, 11, 18, 19mp3an2i 1463 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
219, 20eqsstrid 3963 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝐵 ⊆ ℂ)
2221adantr 484 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℂ)
2322sselda 3915 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
246, 8, 23psergf 25017 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
25 elfznn0 12998 . . . . . . 7 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0)
26 ffvelrn 6827 . . . . . . 7 (((𝐺𝑦):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
2724, 25, 26syl2an 598 . . . . . 6 (((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
285, 27fsumcl 15085 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) ∈ ℂ)
2928fmpttd 6857 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
30 cnex 10610 . . . . 5 ℂ ∈ V
319ovexi 7170 . . . . 5 𝐵 ∈ V
3230, 31elmap 8421 . . . 4 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
3329, 32sylibr 237 . . 3 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵))
3433fmpttd 6857 . 2 ((𝜑𝑎𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))):ℕ0⟶(ℂ ↑m 𝐵))
356, 12, 7, 13, 14, 15psercn 25031 . . . . 5 (𝜑𝐹 ∈ (𝑆cn→ℂ))
36 cncff 23508 . . . . 5 (𝐹 ∈ (𝑆cn→ℂ) → 𝐹:𝑆⟶ℂ)
3735, 36syl 17 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
3837adantr 484 . . 3 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
396, 12, 7, 13, 14, 16psercnlem2 25029 . . . . . 6 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆))
4039simp2d 1140 . . . . 5 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
419, 40eqsstrid 3963 . . . 4 ((𝜑𝑎𝑆) → 𝐵 ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
4239simp3d 1141 . . . 4 ((𝜑𝑎𝑆) → (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)
4341, 42sstrd 3925 . . 3 ((𝜑𝑎𝑆) → 𝐵𝑆)
4438, 43fssresd 6520 . 2 ((𝜑𝑎𝑆) → (𝐹𝐵):𝐵⟶ℂ)
45 0zd 11984 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℤ)
46 eqidd 2799 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) = ((𝐺𝑧)‘𝑗))
477ad2antrr 725 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝐴:ℕ0⟶ℂ)
4821sselda 3915 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ ℂ)
496, 47, 48psergf 25017 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐺𝑧):ℕ0⟶ℂ)
5049ffvelrnda 6829 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) ∈ ℂ)
5148abscld 14791 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ)
5251rexrd 10683 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ*)
5318adantr 484 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
54 iccssxr 12811 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
556, 7, 13radcnvcl 25022 . . . . . . . . 9 (𝜑𝑅 ∈ (0[,]+∞))
5654, 55sseldi 3913 . . . . . . . 8 (𝜑𝑅 ∈ ℝ*)
5756ad2antrr 725 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑅 ∈ ℝ*)
58 0cn 10625 . . . . . . . . . 10 0 ∈ ℂ
59 eqid 2798 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
6059cnmetdval 23386 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6148, 58, 60sylancl 589 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6248subid1d 10978 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 − 0) = 𝑧)
6362fveq2d 6650 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
6461, 63eqtrd 2833 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
65 simpr 488 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝐵)
6665, 9eleqtrdi 2900 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)))
6710a1i 11 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
68 0cnd 10626 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℂ)
69 elbl3 23009 . . . . . . . . . 10 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7067, 53, 68, 48, 69syl22anc 837 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7166, 70mpbid 235 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2))
7264, 71eqbrtrrd 5055 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2))
7316simp3d 1141 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7473adantr 484 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7552, 53, 57, 72, 74xrlttrd 12543 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < 𝑅)
766, 47, 13, 48, 75radcnvlt2 25024 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ∈ dom ⇝ )
771, 45, 46, 50, 76isumclim2 15108 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
7843sselda 3915 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝑆)
79 fveq2 6646 . . . . . . . 8 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
8079fveq1d 6648 . . . . . . 7 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑗) = ((𝐺𝑧)‘𝑗))
8180sumeq2sdv 15056 . . . . . 6 (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
82 sumex 15039 . . . . . 6 Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗) ∈ V
8381, 12, 82fvmpt 6746 . . . . 5 (𝑧𝑆 → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8478, 83syl 17 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8577, 84breqtrrd 5059 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ (𝐹𝑧))
86 oveq2 7144 . . . . . . . . . . 11 (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚))
8786sumeq1d 15053 . . . . . . . . . 10 (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
8887mpteq2dv 5127 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
89 eqid 2798 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))
9031mptex 6964 . . . . . . . . 9 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) ∈ V
9188, 89, 90fvmpt 6746 . . . . . . . 8 (𝑚 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9291adantl 485 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9392fveq1d 6648 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧))
9479fveq1d 6648 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑖) = ((𝐺𝑧)‘𝑖))
9594sumeq2sdv 15056 . . . . . . . 8 (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
96 eqid 2798 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
97 sumex 15039 . . . . . . . 8 Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) ∈ V
9895, 96, 97fvmpt 6746 . . . . . . 7 (𝑧𝐵 → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
9998ad2antlr 726 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
100 eqidd 2799 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) = ((𝐺𝑧)‘𝑖))
101 simpr 488 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
102101, 1eleqtrdi 2900 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ‘0))
10349adantr 484 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺𝑧):ℕ0⟶ℂ)
104 elfznn0 12998 . . . . . . . 8 (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0)
105 ffvelrn 6827 . . . . . . . 8 (((𝐺𝑧):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
106103, 104, 105syl2an 598 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
107100, 102, 106fsumser 15082 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) = (seq0( + , (𝐺𝑧))‘𝑚))
10893, 99, 1073eqtrd 2837 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺𝑧))‘𝑚))
109108mpteq2dva 5126 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
110 0z 11983 . . . . . . 7 0 ∈ ℤ
111 seqfn 13379 . . . . . . 7 (0 ∈ ℤ → seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
112110, 111ax-mp 5 . . . . . 6 seq0( + , (𝐺𝑧)) Fn (ℤ‘0)
1131fneq2i 6422 . . . . . 6 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
114112, 113mpbir 234 . . . . 5 seq0( + , (𝐺𝑧)) Fn ℕ0
115 dffn5 6700 . . . . 5 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
116114, 115mpbi 233 . . . 4 seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚))
117109, 116eqtr4di 2851 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺𝑧)))
118 fvres 6665 . . . 4 (𝑧𝐵 → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
119118adantl 485 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
12085, 117, 1193brtr4d 5063 . 2 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹𝐵)‘𝑧))
12191adantl 485 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
122121oveq2d 7152 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))))
123 eqid 2798 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
124123cnfldtopon 23398 . . . . . . 7 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
125124toponrestid 21536 . . . . . 6 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
1262a1i 11 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ ∈ {ℝ, ℂ})
127123cnfldtopn 23397 . . . . . . . . . 10 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
128127blopn 23117 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
12910, 11, 18, 128mp3an2i 1463 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
1309, 129eqeltrid 2894 . . . . . . 7 ((𝜑𝑎𝑆) → 𝐵 ∈ (TopOpen‘ℂfld))
131130adantr 484 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈ (TopOpen‘ℂfld))
132 fzfid 13339 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
1337ad2antrr 725 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ)
1341333ad2ant1 1130 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
13521adantr 484 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆ ℂ)
136135sselda 3915 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1371363adant2 1128 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1386, 134, 137psergf 25017 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
1391043ad2ant2 1131 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
140138, 139ffvelrnd 6830 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
1412a1i 11 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ, ℂ})
142 ffvelrn 6827 . . . . . . . . . . 11 ((𝐴:ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
143133, 104, 142syl2an 598 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴𝑖) ∈ ℂ)
144143adantr 484 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝐴𝑖) ∈ ℂ)
145136adantlr 714 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
146 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
147104adantl 485 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0)
148 expcl 13446 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
149146, 147, 148syl2anr 599 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑖) ∈ ℂ)
150145, 149syldan 594 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝑦𝑖) ∈ ℂ)
151144, 150mulcld 10653 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
152 ovexd 7171 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V)
153 c0ex 10627 . . . . . . . . . . 11 0 ∈ V
154 ovex 7169 . . . . . . . . . . 11 (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V
155153, 154ifex 4473 . . . . . . . . . 10 if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V
156155a1i 11 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V)
157155a1i 11 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V)
158 dvexp2 24567 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
159147, 158syl 17 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
16021ad2antrr 725 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ)
161130ad2antrr 725 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈ (TopOpen‘ℂfld))
162141, 149, 157, 159, 160, 125, 123, 161dvmptres 24576 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ (𝑦𝑖))) = (𝑦𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
163141, 150, 156, 162, 143dvmptcmul 24577 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
164141, 151, 152, 163dvmptcl 24572 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
1651643impa 1107 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
166104ad2antlr 726 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
1676pserval2 25016 . . . . . . . . . 10 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
168145, 166, 167syl2anc 587 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
169168mpteq2dva 5126 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖))))
170169oveq2d 7152 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))))
171170, 163eqtrd 2833 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
172125, 123, 126, 131, 132, 140, 165, 171dvmptfsum 24588 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
173122, 172eqtrd 2833 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
174173mpteq2dva 5126 . . 3 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))))
175 nnssnn0 11891 . . . . . 6 ℕ ⊆ ℕ0
176 resmpt 5873 . . . . . 6 (ℕ ⊆ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))))
177175, 176ax-mp 5 . . . . 5 ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
178 oveq1 7143 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝑎𝑖) = (𝑥𝑖))
179178oveq2d 7152 . . . . . . . . . . 11 (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)))
180179mpteq2dv 5127 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))))
181 oveq1 7143 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1))
182 fvoveq1 7159 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1)))
183181, 182oveq12d 7154 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
184 oveq2 7144 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → (𝑥𝑖) = (𝑥𝑛))
185183, 184oveq12d 7154 . . . . . . . . . . . 12 (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
186185cbvmptv 5134 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
187 oveq1 7143 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
188 fvoveq1 7159 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1)))
189187, 188oveq12d 7154 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
190 eqid 2798 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))
191 ovex 7169 . . . . . . . . . . . . . 14 ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V
192189, 190, 191fvmpt 6746 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
193192oveq1d 7151 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
194193mpteq2ia 5122 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
195186, 194eqtr4i 2824 . . . . . . . . . 10 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)))
196180, 195eqtrdi 2849 . . . . . . . . 9 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
197196cbvmptv 5134 . . . . . . . 8 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
198 fveq2 6646 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))
199198fveq1d 6648 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
200199sumeq2sdv 15056 . . . . . . . . 9 (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
201200cbvmptv 5134 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑧𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
202 peano2nn0 11928 . . . . . . . . . . . 12 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
203202adantl 485 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℕ0)
204203nn0cnd 11948 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℂ)
205133, 203ffvelrnd 6830 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ)
206204, 205mulcld 10653 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ)
207206fmpttd 6857 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))):ℕ0⟶ℂ)
208 fveq2 6646 . . . . . . . . . . . 12 (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗))
209208seqeq3d 13375 . . . . . . . . . . 11 (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)))
210209eleq1d 2874 . . . . . . . . . 10 (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ ))
211210cbvrabv 3439 . . . . . . . . 9 {𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }
212211supeq1i 8898 . . . . . . . 8 sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*, < )
213198seqeq3d 13375 . . . . . . . . . . . 12 (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)))
214213fveq1d 6648 . . . . . . . . . . 11 (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
215214cbvmptv 5134 . . . . . . . . . 10 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
216 fveq2 6646 . . . . . . . . . . 11 (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚))
217216mpteq2dv 5127 . . . . . . . . . 10 (𝑗 = 𝑚 → (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
218215, 217syl5eq 2845 . . . . . . . . 9 (𝑗 = 𝑚 → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
219218cbvmptv 5134 . . . . . . . 8 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
22017rpred 12422 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ)
2216, 12, 7, 13, 14, 15psercnlem1 25030 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
222221simp1d 1139 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
223222rpxrd 12423 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ*)
224197, 207, 212radcnvcl 25022 . . . . . . . . . 10 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
22554, 224sseldi 3913 . . . . . . . . 9 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
226221simp2d 1140 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑀)
227 cnvimass 5917 . . . . . . . . . . . . . . . 16 (abs “ (0[,)𝑅)) ⊆ dom abs
228 absf 14692 . . . . . . . . . . . . . . . . 17 abs:ℂ⟶ℝ
229228fdmi 6499 . . . . . . . . . . . . . . . 16 dom abs = ℂ
230227, 229sseqtri 3951 . . . . . . . . . . . . . . 15 (abs “ (0[,)𝑅)) ⊆ ℂ
23114, 230eqsstri 3949 . . . . . . . . . . . . . 14 𝑆 ⊆ ℂ
232231a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ ℂ)
233232sselda 3915 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
234233abscld 14791 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
235222rpred 12422 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
236 avglt2 11867 . . . . . . . . . . 11 (((abs‘𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
237234, 235, 236syl2anc 587 . . . . . . . . . 10 ((𝜑𝑎𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
238226, 237mpbid 235 . . . . . . . . 9 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀)
239222rpge0d 12426 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 0 ≤ 𝑀)
240235, 239absidd 14777 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) = 𝑀)
241222rpcnd 12424 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℂ)
242 oveq1 7143 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑀 → (𝑤𝑖) = (𝑀𝑖))
243242oveq2d 7152 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
244243mpteq2dv 5127 . . . . . . . . . . . . . . 15 (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
245 oveq1 7143 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝑖) = (𝑤𝑖))
246245oveq2d 7152 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)))
247246mpteq2dv 5127 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
248247cbvmptv 5134 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
249 nn0ex 11894 . . . . . . . . . . . . . . . 16 0 ∈ V
250249mptex 6964 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) ∈ V
251244, 248, 250fvmpt 6746 . . . . . . . . . . . . . 14 (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
252241, 251syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
253252seqeq3d 13375 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))))
254 fveq2 6646 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
255 oveq2 7144 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
256254, 255oveq12d 7154 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
257256cbvmptv 5134 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖)))
258 oveq1 7143 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
259258oveq2d 7152 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
260259mpteq2dv 5127 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
261257, 260syl5eq 2845 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
262261cbvmptv 5134 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
2636, 262eqtri 2821 . . . . . . . . . . . . 13 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
264 fveq2 6646 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (𝐺𝑟) = (𝐺𝑠))
265264seqeq3d 13375 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → seq0( + , (𝐺𝑟)) = seq0( + , (𝐺𝑠)))
266265eleq1d 2874 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → (seq0( + , (𝐺𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ))
267266cbvrabv 3439 . . . . . . . . . . . . . . 15 {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }
268267supeq1i 8898 . . . . . . . . . . . . . 14 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
26913, 268eqtri 2821 . . . . . . . . . . . . 13 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
270 eqid 2798 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
2717adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝐴:ℕ0⟶ℂ)
272221simp3d 1141 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → 𝑀 < 𝑅)
273240, 272eqbrtrd 5053 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (abs‘𝑀) < 𝑅)
274263, 269, 270, 271, 241, 273dvradcnv 25026 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))) ∈ dom ⇝ )
275253, 274eqeltrd 2890 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) ∈ dom ⇝ )
276197, 207, 212, 241, 275radcnvle 25025 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
277240, 276eqbrtrrd 5055 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
27818, 223, 225, 238, 277xrltletrd 12545 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
279197, 201, 207, 212, 219, 220, 278, 41pserulm 25027 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)))
28021sselda 3915 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
281 oveq1 7143 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → (𝑎𝑖) = (𝑦𝑖))
282281oveq2d 7152 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
283282mpteq2dv 5127 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
284 eqid 2798 . . . . . . . . . . . . . 14 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))
285249mptex 6964 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) ∈ V
286283, 284, 285fvmpt 6746 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
287280, 286syl 17 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
288287adantr 484 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
289288fveq1d 6648 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
290 oveq1 7143 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
291 fvoveq1 7159 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1)))
292290, 291oveq12d 7154 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
293 oveq2 7144 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑦𝑖) = (𝑦𝑘))
294292, 293oveq12d 7154 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
295 eqid 2798 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
296 ovex 7169 . . . . . . . . . . . 12 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V
297294, 295, 296fvmpt 6746 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
298297adantl 485 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
299289, 298eqtrd 2833 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
300299sumeq2dv 15055 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
301300mpteq2dva 5126 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
302279, 301breqtrd 5057 . . . . . 6 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
303 nnuz 12272 . . . . . . . 8 ℕ = (ℤ‘1)
304 1e0p1 12131 . . . . . . . . 9 1 = (0 + 1)
305304fveq2i 6649 . . . . . . . 8 (ℤ‘1) = (ℤ‘(0 + 1))
306303, 305eqtri 2821 . . . . . . 7 ℕ = (ℤ‘(0 + 1))
307 1zzd 12004 . . . . . . 7 ((𝜑𝑎𝑆) → 1 ∈ ℤ)
308 0zd 11984 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 0 ∈ ℤ)
309 peano2nn0 11928 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
310309nn0cnd 11948 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℂ)
311310adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℂ)
3127ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
313 ffvelrn 6827 . . . . . . . . . . . . . . . . . 18 ((𝐴:ℕ0⟶ℂ ∧ (𝑖 + 1) ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
314312, 309, 313syl2an 598 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
315311, 314mulcld 10653 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ)
316280, 148sylan 583 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
317315, 316mulcld 10653 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) ∈ ℂ)
318287, 317fmpt3d 6858 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦):ℕ0⟶ℂ)
319318ffvelrnda 6829 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑚) ∈ ℂ)
3201, 308, 319serf 13397 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)):ℕ0⟶ℂ)
321320ffvelrnda 6829 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
322321an32s 651 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
323322fmpttd 6857 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
32430, 31elmap 8421 . . . . . . . . 9 ((𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
325323, 324sylibr 237 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵))
326325fmpttd 6857 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ ↑m 𝐵))
327 elfznn 12934 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ)
328327nnne0d 11678 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0)
329328neneqd 2992 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0)
330329iffalsed 4436 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1))))
331330oveq2d 7152 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑚) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
332331sumeq2i 15051 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))
333 1zzd 12004 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 1 ∈ ℤ)
334 nnz 11995 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
335334ad2antlr 726 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑚 ∈ ℤ)
336271ad2antrr 725 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
337327nnnn0d 11946 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0)
338336, 337, 142syl2an 598 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴𝑖) ∈ ℂ)
339327adantl 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ)
340339nncnd 11644 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ)
341280adantlr 714 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
342 nnm1nn0 11929 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (𝑖 − 1) ∈ ℕ0)
343327, 342syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈ ℕ0)
344 expcl 13446 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈ ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
345341, 343, 344syl2an 598 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
346340, 345mulcld 10653 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈ ℂ)
347338, 346mulcld 10653 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ ℂ)
348 fveq2 6646 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝐴𝑖) = (𝐴‘(𝑘 + 1)))
349 id 22 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
350 oveq1 7143 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1))
351350oveq2d 7152 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1)))
352349, 351oveq12d 7154 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
353348, 352oveq12d 7154 . . . . . . . . . . . . 13 (𝑖 = (𝑘 + 1) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
354333, 333, 335, 347, 353fsumshftm 15131 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
355332, 354syl5eq 2845 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
356 fz1ssfz0 13001 . . . . . . . . . . . . 13 (1...𝑚) ⊆ (0...𝑚)
357356a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (1...𝑚) ⊆ (0...𝑚))
358331adantl 485 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
359358, 347eqeltrd 2890 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
360 eldif 3891 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)))
361 elfzuz2 12910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑚) → 𝑚 ∈ (ℤ‘0))
362 elfzp12 12984 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (ℤ‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
363361, 362syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
364363ibi 270 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))
365364ord 861 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...𝑚) → (¬ 𝑖 = 0 → 𝑖 ∈ ((0 + 1)...𝑚)))
366365con1d 147 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0...𝑚) → (¬ 𝑖 ∈ ((0 + 1)...𝑚) → 𝑖 = 0))
367366imp 410 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)) → 𝑖 = 0)
368360, 367sylbi 220 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) → 𝑖 = 0)
369304oveq1i 7146 . . . . . . . . . . . . . . . . . 18 (1...𝑚) = ((0 + 1)...𝑚)
370369difeq2i 4047 . . . . . . . . . . . . . . . . 17 ((0...𝑚) ∖ (1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚))
371368, 370eleq2s 2908 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0)
372371adantl 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0)
373372iftrued 4433 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0)
374373oveq2d 7152 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · 0))
375 eldifi 4054 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚))
376375, 104syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0)
377336, 376, 142syl2an 598 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴𝑖) ∈ ℂ)
378377mul01d 10831 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · 0) = 0)
379374, 378eqtrd 2833 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0)
380 fzfid 13339 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
381357, 359, 379, 380fsumss 15077 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
382 1m1e0 11700 . . . . . . . . . . . . . 14 (1 − 1) = 0
383382oveq1i 7146 . . . . . . . . . . . . 13 ((1 − 1)...(𝑚 − 1)) = (0...(𝑚 − 1))
384383sumeq1i 15050 . . . . . . . . . . . 12 Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
385 elfznn0 12998 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...(𝑚 − 1)) → 𝑘 ∈ ℕ0)
386385adantl 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℕ0)
387386, 297syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
388341adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑦 ∈ ℂ)
389388, 286syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
390389fveq1d 6648 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
391336adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ)
392 peano2nn0 11928 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
393386, 392syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℕ0)
394391, 393ffvelrnd 6830 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
395393nn0cnd 11948 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ)
396 expcl 13446 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
397341, 385, 396syl2an 598 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦𝑘) ∈ ℂ)
398394, 395, 397mul12d 10841 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
399386nn0cnd 11948 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ)
400 ax-1cn 10587 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
401 pncan 10884 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
402399, 400, 401sylancl 589 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘)
403402oveq2d 7152 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦𝑘))
404403oveq2d 7152 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦𝑘)))
405404oveq2d 7152 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))))
406395, 394, 397mulassd 10656 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
407398, 405, 4063eqtr4d 2843 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
408387, 390, 4073eqtr4d 2843 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
409 nnm1nn0 11929 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → (𝑚 − 1) ∈ ℕ0)
410409adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈ ℕ0)
411410adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ ℕ0)
412411, 1eleqtrdi 2900 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ (ℤ‘0))
413403, 397eqeltrd 2890 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) ∈ ℂ)
414395, 413mulcld 10653 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) ∈ ℂ)
415394, 414mulcld 10653 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) ∈ ℂ)
416408, 412, 415fsumser 15082 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
417384, 416syl5eq 2845 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
418355, 381, 4173eqtr3d 2841 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
419418mpteq2dva 5126 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
420 fveq2 6646 . . . . . . . . . . . 12 (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
421420mpteq2dv 5127 . . . . . . . . . . 11 (𝑗 = (𝑚 − 1) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
422 eqid 2798 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))
42331mptex 6964 . . . . . . . . . . 11 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V
424421, 422, 423fvmpt 6746 . . . . . . . . . 10 ((𝑚 − 1) ∈ ℕ0 → ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
425410, 424syl 17 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
426419, 425eqtr4d 2836 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))
427426mpteq2dva 5126 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))))
4281, 306, 4, 307, 326, 427ulmshft 24995 . . . . . 6 ((𝜑𝑎𝑆) → ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) ↔ (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))))
429302, 428mpbid 235 . . . . 5 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
430177, 429eqbrtrid 5066 . . . 4 ((𝜑𝑎𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ)(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
431 1nn0 11904 . . . . . 6 1 ∈ ℕ0
432431a1i 11 . . . . 5 ((𝜑𝑎𝑆) → 1 ∈ ℕ0)
433 fzfid 13339 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
434164an32s 651 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
435433, 434fsumcl 15085 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
436435fmpttd 6857 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
43730, 31elmap 8421 . . . . . . 7 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
438436, 437sylibr 237 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵))
439438fmpttd 6857 . . . . 5 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))):ℕ0⟶(ℂ ↑m 𝐵))
4401, 303, 432, 439ulmres 24993 . . . 4 ((𝜑𝑎𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) ↔ ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ)(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))))
441430, 440mpbird 260 . . 3 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
442174, 441eqbrtrd 5053 . 2 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
4431, 3, 4, 34, 44, 120, 442ulmdv 25008 1 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ifcif 4425  {cpr 4527   class class class wbr 5031   ↦ cmpt 5111  ◡ccnv 5519  dom cdm 5520   ↾ cres 5522   “ cima 5523   ∘ ccom 5524   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136   ↑m cmap 8392  supcsup 8891  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11628  2c2 11683  ℕ0cn0 11888  ℤcz 11972  ℤ≥cuz 12234  ℝ+crp 12380  [,)cico 12731  [,]cicc 12732  ...cfz 12888  seqcseq 13367  ↑cexp 13428  abscabs 14588   ⇝ cli 14836  Σcsu 15037  TopOpenctopn 16690  ∞Metcxmet 20080  ballcbl 20082  ℂfldccnfld 20095  –cn→ccncf 23491   D cdv 24476  ⇝𝑢culm 24981 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-om 7564  df-1st 7674  df-2nd 7675  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8821  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-4 11693  df-5 11694  df-6 11695  df-7 11696  df-8 11697  df-9 11698  df-n0 11889  df-z 11973  df-dec 12090  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13429  df-hash 13690  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21509  df-topon 21526  df-topsp 21548  df-bases 21561  df-cld 21634  df-ntr 21635  df-cls 21636  df-nei 21713  df-lp 21751  df-perf 21752  df-cn 21842  df-cnp 21843  df-haus 21930  df-cmp 22002  df-tx 22177  df-hmeo 22370  df-fil 22461  df-fm 22553  df-flim 22554  df-flf 22555  df-xms 22937  df-ms 22938  df-tms 22939  df-cncf 23493  df-limc 24479  df-dv 24480  df-ulm 24982 This theorem is referenced by:  pserdv  25034
 Copyright terms: Public domain W3C validator