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

Theorem pserdvlem2 25320
Description: Lemma for pserdv 25321. (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 12476 . 2 0 = (ℤ‘0)
2 cnelprrecn 10822 . . 3 ℂ ∈ {ℝ, ℂ}
32a1i 11 . 2 ((𝜑𝑎𝑆) → ℂ ∈ {ℝ, ℂ})
4 0zd 12188 . 2 ((𝜑𝑎𝑆) → 0 ∈ ℤ)
5 fzfid 13546 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑘) ∈ Fin)
6 pserf.g . . . . . . . 8 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
7 pserf.a . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℂ)
87ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
9 pserdv.b . . . . . . . . . . 11 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
10 cnxmet 23670 . . . . . . . . . . . 12 (abs ∘ − ) ∈ (∞Met‘ℂ)
11 0cnd 10826 . . . . . . . . . . . 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 25319 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
1716simp1d 1144 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+)
1817rpxrd 12629 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
19 blssm 23316 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
2010, 11, 18, 19mp3an2i 1468 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
219, 20eqsstrid 3949 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝐵 ⊆ ℂ)
2221adantr 484 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℂ)
2322sselda 3901 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
246, 8, 23psergf 25304 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
25 elfznn0 13205 . . . . . . 7 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0)
26 ffvelrn 6902 . . . . . . 7 (((𝐺𝑦):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
2724, 25, 26syl2an 599 . . . . . 6 (((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
285, 27fsumcl 15297 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) ∈ ℂ)
2928fmpttd 6932 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
30 cnex 10810 . . . . 5 ℂ ∈ V
319ovexi 7247 . . . . 5 𝐵 ∈ V
3230, 31elmap 8552 . . . 4 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
3329, 32sylibr 237 . . 3 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵))
3433fmpttd 6932 . 2 ((𝜑𝑎𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))):ℕ0⟶(ℂ ↑m 𝐵))
356, 12, 7, 13, 14, 15psercn 25318 . . . . 5 (𝜑𝐹 ∈ (𝑆cn→ℂ))
36 cncff 23790 . . . . 5 (𝐹 ∈ (𝑆cn→ℂ) → 𝐹:𝑆⟶ℂ)
3735, 36syl 17 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
3837adantr 484 . . 3 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
396, 12, 7, 13, 14, 16psercnlem2 25316 . . . . . 6 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆))
4039simp2d 1145 . . . . 5 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
419, 40eqsstrid 3949 . . . 4 ((𝜑𝑎𝑆) → 𝐵 ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
4239simp3d 1146 . . . 4 ((𝜑𝑎𝑆) → (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)
4341, 42sstrd 3911 . . 3 ((𝜑𝑎𝑆) → 𝐵𝑆)
4438, 43fssresd 6586 . 2 ((𝜑𝑎𝑆) → (𝐹𝐵):𝐵⟶ℂ)
45 0zd 12188 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℤ)
46 eqidd 2738 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) = ((𝐺𝑧)‘𝑗))
477ad2antrr 726 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝐴:ℕ0⟶ℂ)
4821sselda 3901 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ ℂ)
496, 47, 48psergf 25304 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐺𝑧):ℕ0⟶ℂ)
5049ffvelrnda 6904 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) ∈ ℂ)
5148abscld 15000 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ)
5251rexrd 10883 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ*)
5318adantr 484 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
54 iccssxr 13018 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
556, 7, 13radcnvcl 25309 . . . . . . . . 9 (𝜑𝑅 ∈ (0[,]+∞))
5654, 55sseldi 3899 . . . . . . . 8 (𝜑𝑅 ∈ ℝ*)
5756ad2antrr 726 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑅 ∈ ℝ*)
58 0cn 10825 . . . . . . . . . 10 0 ∈ ℂ
59 eqid 2737 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
6059cnmetdval 23668 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6148, 58, 60sylancl 589 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6248subid1d 11178 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 − 0) = 𝑧)
6362fveq2d 6721 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
6461, 63eqtrd 2777 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
65 simpr 488 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝐵)
6665, 9eleqtrdi 2848 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)))
6710a1i 11 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
68 0cnd 10826 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℂ)
69 elbl3 23290 . . . . . . . . . 10 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7067, 53, 68, 48, 69syl22anc 839 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7166, 70mpbid 235 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2))
7264, 71eqbrtrrd 5077 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2))
7316simp3d 1146 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7473adantr 484 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7552, 53, 57, 72, 74xrlttrd 12749 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < 𝑅)
766, 47, 13, 48, 75radcnvlt2 25311 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ∈ dom ⇝ )
771, 45, 46, 50, 76isumclim2 15322 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
7843sselda 3901 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝑆)
79 fveq2 6717 . . . . . . . 8 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
8079fveq1d 6719 . . . . . . 7 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑗) = ((𝐺𝑧)‘𝑗))
8180sumeq2sdv 15268 . . . . . 6 (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
82 sumex 15251 . . . . . 6 Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗) ∈ V
8381, 12, 82fvmpt 6818 . . . . 5 (𝑧𝑆 → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8478, 83syl 17 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8577, 84breqtrrd 5081 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ (𝐹𝑧))
86 oveq2 7221 . . . . . . . . . . 11 (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚))
8786sumeq1d 15265 . . . . . . . . . 10 (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
8887mpteq2dv 5151 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
89 eqid 2737 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))
9031mptex 7039 . . . . . . . . 9 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) ∈ V
9188, 89, 90fvmpt 6818 . . . . . . . 8 (𝑚 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9291adantl 485 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9392fveq1d 6719 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧))
9479fveq1d 6719 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑖) = ((𝐺𝑧)‘𝑖))
9594sumeq2sdv 15268 . . . . . . . 8 (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
96 eqid 2737 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
97 sumex 15251 . . . . . . . 8 Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) ∈ V
9895, 96, 97fvmpt 6818 . . . . . . 7 (𝑧𝐵 → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
9998ad2antlr 727 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
100 eqidd 2738 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) = ((𝐺𝑧)‘𝑖))
101 simpr 488 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
102101, 1eleqtrdi 2848 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ‘0))
10349adantr 484 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺𝑧):ℕ0⟶ℂ)
104 elfznn0 13205 . . . . . . . 8 (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0)
105 ffvelrn 6902 . . . . . . . 8 (((𝐺𝑧):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
106103, 104, 105syl2an 599 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
107100, 102, 106fsumser 15294 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) = (seq0( + , (𝐺𝑧))‘𝑚))
10893, 99, 1073eqtrd 2781 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺𝑧))‘𝑚))
109108mpteq2dva 5150 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
110 0z 12187 . . . . . . 7 0 ∈ ℤ
111 seqfn 13586 . . . . . . 7 (0 ∈ ℤ → seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
112110, 111ax-mp 5 . . . . . 6 seq0( + , (𝐺𝑧)) Fn (ℤ‘0)
1131fneq2i 6477 . . . . . 6 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
114112, 113mpbir 234 . . . . 5 seq0( + , (𝐺𝑧)) Fn ℕ0
115 dffn5 6771 . . . . 5 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
116114, 115mpbi 233 . . . 4 seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚))
117109, 116eqtr4di 2796 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺𝑧)))
118 fvres 6736 . . . 4 (𝑧𝐵 → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
119118adantl 485 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
12085, 117, 1193brtr4d 5085 . 2 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹𝐵)‘𝑧))
12191adantl 485 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
122121oveq2d 7229 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))))
123 eqid 2737 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
124123cnfldtopon 23680 . . . . . . 7 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
125124toponrestid 21818 . . . . . 6 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
1262a1i 11 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ ∈ {ℝ, ℂ})
127123cnfldtopn 23679 . . . . . . . . . 10 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
128127blopn 23398 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
12910, 11, 18, 128mp3an2i 1468 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
1309, 129eqeltrid 2842 . . . . . . 7 ((𝜑𝑎𝑆) → 𝐵 ∈ (TopOpen‘ℂfld))
131130adantr 484 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈ (TopOpen‘ℂfld))
132 fzfid 13546 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
1337ad2antrr 726 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ)
1341333ad2ant1 1135 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
13521adantr 484 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆ ℂ)
136135sselda 3901 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1371363adant2 1133 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1386, 134, 137psergf 25304 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
1391043ad2ant2 1136 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
140138, 139ffvelrnd 6905 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
1412a1i 11 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ, ℂ})
142 ffvelrn 6902 . . . . . . . . . . 11 ((𝐴:ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
143133, 104, 142syl2an 599 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴𝑖) ∈ ℂ)
144143adantr 484 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝐴𝑖) ∈ ℂ)
145136adantlr 715 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
146 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
147104adantl 485 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0)
148 expcl 13653 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
149146, 147, 148syl2anr 600 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑖) ∈ ℂ)
150145, 149syldan 594 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝑦𝑖) ∈ ℂ)
151144, 150mulcld 10853 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
152 ovexd 7248 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V)
153 c0ex 10827 . . . . . . . . . . 11 0 ∈ V
154 ovex 7246 . . . . . . . . . . 11 (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V
155153, 154ifex 4489 . . . . . . . . . 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 24851 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
159147, 158syl 17 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
16021ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ)
161130ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈ (TopOpen‘ℂfld))
162141, 149, 157, 159, 160, 125, 123, 161dvmptres 24860 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ (𝑦𝑖))) = (𝑦𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
163141, 150, 156, 162, 143dvmptcmul 24861 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
164141, 151, 152, 163dvmptcl 24856 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
1651643impa 1112 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
166104ad2antlr 727 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
1676pserval2 25303 . . . . . . . . . 10 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
168145, 166, 167syl2anc 587 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
169168mpteq2dva 5150 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖))))
170169oveq2d 7229 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))))
171170, 163eqtrd 2777 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
172125, 123, 126, 131, 132, 140, 165, 171dvmptfsum 24872 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
173122, 172eqtrd 2777 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
174173mpteq2dva 5150 . . 3 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))))
175 nnssnn0 12093 . . . . . 6 ℕ ⊆ ℕ0
176 resmpt 5905 . . . . . 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 7220 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝑎𝑖) = (𝑥𝑖))
179178oveq2d 7229 . . . . . . . . . . 11 (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)))
180179mpteq2dv 5151 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))))
181 oveq1 7220 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1))
182 fvoveq1 7236 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1)))
183181, 182oveq12d 7231 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
184 oveq2 7221 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → (𝑥𝑖) = (𝑥𝑛))
185183, 184oveq12d 7231 . . . . . . . . . . . 12 (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
186185cbvmptv 5158 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
187 oveq1 7220 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
188 fvoveq1 7236 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1)))
189187, 188oveq12d 7231 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
190 eqid 2737 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))
191 ovex 7246 . . . . . . . . . . . . . 14 ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V
192189, 190, 191fvmpt 6818 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
193192oveq1d 7228 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
194193mpteq2ia 5146 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
195186, 194eqtr4i 2768 . . . . . . . . . 10 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)))
196180, 195eqtrdi 2794 . . . . . . . . 9 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
197196cbvmptv 5158 . . . . . . . 8 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
198 fveq2 6717 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))
199198fveq1d 6719 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
200199sumeq2sdv 15268 . . . . . . . . 9 (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
201200cbvmptv 5158 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑧𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
202 peano2nn0 12130 . . . . . . . . . . . 12 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
203202adantl 485 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℕ0)
204203nn0cnd 12152 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℂ)
205133, 203ffvelrnd 6905 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ)
206204, 205mulcld 10853 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ)
207206fmpttd 6932 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))):ℕ0⟶ℂ)
208 fveq2 6717 . . . . . . . . . . . 12 (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗))
209208seqeq3d 13582 . . . . . . . . . . 11 (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)))
210209eleq1d 2822 . . . . . . . . . 10 (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ ))
211210cbvrabv 3402 . . . . . . . . 9 {𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }
212211supeq1i 9063 . . . . . . . 8 sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*, < )
213198seqeq3d 13582 . . . . . . . . . . . 12 (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)))
214213fveq1d 6719 . . . . . . . . . . 11 (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
215214cbvmptv 5158 . . . . . . . . . 10 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
216 fveq2 6717 . . . . . . . . . . 11 (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚))
217216mpteq2dv 5151 . . . . . . . . . 10 (𝑗 = 𝑚 → (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
218215, 217syl5eq 2790 . . . . . . . . 9 (𝑗 = 𝑚 → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
219218cbvmptv 5158 . . . . . . . 8 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
22017rpred 12628 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ)
2216, 12, 7, 13, 14, 15psercnlem1 25317 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
222221simp1d 1144 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
223222rpxrd 12629 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ*)
224197, 207, 212radcnvcl 25309 . . . . . . . . . 10 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
22554, 224sseldi 3899 . . . . . . . . 9 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
226221simp2d 1145 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑀)
227 cnvimass 5949 . . . . . . . . . . . . . . . 16 (abs “ (0[,)𝑅)) ⊆ dom abs
228 absf 14901 . . . . . . . . . . . . . . . . 17 abs:ℂ⟶ℝ
229228fdmi 6557 . . . . . . . . . . . . . . . 16 dom abs = ℂ
230227, 229sseqtri 3937 . . . . . . . . . . . . . . 15 (abs “ (0[,)𝑅)) ⊆ ℂ
23114, 230eqsstri 3935 . . . . . . . . . . . . . 14 𝑆 ⊆ ℂ
232231a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ ℂ)
233232sselda 3901 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
234233abscld 15000 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
235222rpred 12628 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
236 avglt2 12069 . . . . . . . . . . 11 (((abs‘𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
237234, 235, 236syl2anc 587 . . . . . . . . . 10 ((𝜑𝑎𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
238226, 237mpbid 235 . . . . . . . . 9 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀)
239222rpge0d 12632 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 0 ≤ 𝑀)
240235, 239absidd 14986 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) = 𝑀)
241222rpcnd 12630 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℂ)
242 oveq1 7220 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑀 → (𝑤𝑖) = (𝑀𝑖))
243242oveq2d 7229 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
244243mpteq2dv 5151 . . . . . . . . . . . . . . 15 (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
245 oveq1 7220 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝑖) = (𝑤𝑖))
246245oveq2d 7229 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)))
247246mpteq2dv 5151 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
248247cbvmptv 5158 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
249 nn0ex 12096 . . . . . . . . . . . . . . . 16 0 ∈ V
250249mptex 7039 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) ∈ V
251244, 248, 250fvmpt 6818 . . . . . . . . . . . . . 14 (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
252241, 251syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
253252seqeq3d 13582 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))))
254 fveq2 6717 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
255 oveq2 7221 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
256254, 255oveq12d 7231 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
257256cbvmptv 5158 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖)))
258 oveq1 7220 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
259258oveq2d 7229 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
260259mpteq2dv 5151 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
261257, 260syl5eq 2790 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
262261cbvmptv 5158 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
2636, 262eqtri 2765 . . . . . . . . . . . . 13 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
264 fveq2 6717 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (𝐺𝑟) = (𝐺𝑠))
265264seqeq3d 13582 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → seq0( + , (𝐺𝑟)) = seq0( + , (𝐺𝑠)))
266265eleq1d 2822 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → (seq0( + , (𝐺𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ))
267266cbvrabv 3402 . . . . . . . . . . . . . . 15 {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }
268267supeq1i 9063 . . . . . . . . . . . . . 14 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
26913, 268eqtri 2765 . . . . . . . . . . . . 13 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
270 eqid 2737 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
2717adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝐴:ℕ0⟶ℂ)
272221simp3d 1146 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → 𝑀 < 𝑅)
273240, 272eqbrtrd 5075 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (abs‘𝑀) < 𝑅)
274263, 269, 270, 271, 241, 273dvradcnv 25313 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))) ∈ dom ⇝ )
275253, 274eqeltrd 2838 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) ∈ dom ⇝ )
276197, 207, 212, 241, 275radcnvle 25312 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
277240, 276eqbrtrrd 5077 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
27818, 223, 225, 238, 277xrltletrd 12751 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
279197, 201, 207, 212, 219, 220, 278, 41pserulm 25314 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)))
28021sselda 3901 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
281 oveq1 7220 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → (𝑎𝑖) = (𝑦𝑖))
282281oveq2d 7229 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
283282mpteq2dv 5151 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
284 eqid 2737 . . . . . . . . . . . . . 14 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))
285249mptex 7039 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) ∈ V
286283, 284, 285fvmpt 6818 . . . . . . . . . . . . 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 6719 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
290 oveq1 7220 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
291 fvoveq1 7236 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1)))
292290, 291oveq12d 7231 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
293 oveq2 7221 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑦𝑖) = (𝑦𝑘))
294292, 293oveq12d 7231 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
295 eqid 2737 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
296 ovex 7246 . . . . . . . . . . . 12 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V
297294, 295, 296fvmpt 6818 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
298297adantl 485 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
299289, 298eqtrd 2777 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
300299sumeq2dv 15267 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
301300mpteq2dva 5150 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
302279, 301breqtrd 5079 . . . . . 6 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
303 nnuz 12477 . . . . . . . 8 ℕ = (ℤ‘1)
304 1e0p1 12335 . . . . . . . . 9 1 = (0 + 1)
305304fveq2i 6720 . . . . . . . 8 (ℤ‘1) = (ℤ‘(0 + 1))
306303, 305eqtri 2765 . . . . . . 7 ℕ = (ℤ‘(0 + 1))
307 1zzd 12208 . . . . . . 7 ((𝜑𝑎𝑆) → 1 ∈ ℤ)
308 0zd 12188 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 0 ∈ ℤ)
309 peano2nn0 12130 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
310309nn0cnd 12152 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℂ)
311310adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℂ)
3127ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
313 ffvelrn 6902 . . . . . . . . . . . . . . . . . 18 ((𝐴:ℕ0⟶ℂ ∧ (𝑖 + 1) ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
314312, 309, 313syl2an 599 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
315311, 314mulcld 10853 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ)
316280, 148sylan 583 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
317315, 316mulcld 10853 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) ∈ ℂ)
318287, 317fmpt3d 6933 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦):ℕ0⟶ℂ)
319318ffvelrnda 6904 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑚) ∈ ℂ)
3201, 308, 319serf 13604 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)):ℕ0⟶ℂ)
321320ffvelrnda 6904 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
322321an32s 652 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
323322fmpttd 6932 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
32430, 31elmap 8552 . . . . . . . . 9 ((𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
325323, 324sylibr 237 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵))
326325fmpttd 6932 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ ↑m 𝐵))
327 elfznn 13141 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ)
328327nnne0d 11880 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0)
329328neneqd 2945 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0)
330329iffalsed 4450 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1))))
331330oveq2d 7229 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑚) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
332331sumeq2i 15263 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))
333 1zzd 12208 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 1 ∈ ℤ)
334 nnz 12199 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
335334ad2antlr 727 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑚 ∈ ℤ)
336271ad2antrr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
337327nnnn0d 12150 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0)
338336, 337, 142syl2an 599 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴𝑖) ∈ ℂ)
339327adantl 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ)
340339nncnd 11846 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ)
341280adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
342 nnm1nn0 12131 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (𝑖 − 1) ∈ ℕ0)
343327, 342syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈ ℕ0)
344 expcl 13653 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈ ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
345341, 343, 344syl2an 599 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
346340, 345mulcld 10853 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈ ℂ)
347338, 346mulcld 10853 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ ℂ)
348 fveq2 6717 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝐴𝑖) = (𝐴‘(𝑘 + 1)))
349 id 22 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
350 oveq1 7220 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1))
351350oveq2d 7229 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1)))
352349, 351oveq12d 7231 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
353348, 352oveq12d 7231 . . . . . . . . . . . . 13 (𝑖 = (𝑘 + 1) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
354333, 333, 335, 347, 353fsumshftm 15345 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
355332, 354syl5eq 2790 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
356 fz1ssfz0 13208 . . . . . . . . . . . . 13 (1...𝑚) ⊆ (0...𝑚)
357356a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (1...𝑚) ⊆ (0...𝑚))
358331adantl 485 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
359358, 347eqeltrd 2838 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
360 eldif 3876 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)))
361 elfzuz2 13117 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑚) → 𝑚 ∈ (ℤ‘0))
362 elfzp12 13191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (ℤ‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
363361, 362syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
364363ibi 270 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))
365364ord 864 . . . . . . . . . . . . . . . . . . . 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 7223 . . . . . . . . . . . . . . . . . 18 (1...𝑚) = ((0 + 1)...𝑚)
370369difeq2i 4034 . . . . . . . . . . . . . . . . 17 ((0...𝑚) ∖ (1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚))
371368, 370eleq2s 2856 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0)
372371adantl 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0)
373372iftrued 4447 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0)
374373oveq2d 7229 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · 0))
375 eldifi 4041 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚))
376375, 104syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0)
377336, 376, 142syl2an 599 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴𝑖) ∈ ℂ)
378377mul01d 11031 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · 0) = 0)
379374, 378eqtrd 2777 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0)
380 fzfid 13546 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
381357, 359, 379, 380fsumss 15289 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
382 1m1e0 11902 . . . . . . . . . . . . . 14 (1 − 1) = 0
383382oveq1i 7223 . . . . . . . . . . . . 13 ((1 − 1)...(𝑚 − 1)) = (0...(𝑚 − 1))
384383sumeq1i 15262 . . . . . . . . . . . 12 Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
385 elfznn0 13205 . . . . . . . . . . . . . . . 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 6719 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
391336adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ)
392 peano2nn0 12130 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
393386, 392syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℕ0)
394391, 393ffvelrnd 6905 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
395393nn0cnd 12152 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ)
396 expcl 13653 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
397341, 385, 396syl2an 599 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦𝑘) ∈ ℂ)
398394, 395, 397mul12d 11041 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
399386nn0cnd 12152 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ)
400 ax-1cn 10787 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
401 pncan 11084 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
402399, 400, 401sylancl 589 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘)
403402oveq2d 7229 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦𝑘))
404403oveq2d 7229 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦𝑘)))
405404oveq2d 7229 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))))
406395, 394, 397mulassd 10856 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
407398, 405, 4063eqtr4d 2787 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
408387, 390, 4073eqtr4d 2787 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
409 nnm1nn0 12131 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → (𝑚 − 1) ∈ ℕ0)
410409adantl 485 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈ ℕ0)
411410adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ ℕ0)
412411, 1eleqtrdi 2848 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ (ℤ‘0))
413403, 397eqeltrd 2838 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) ∈ ℂ)
414395, 413mulcld 10853 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) ∈ ℂ)
415394, 414mulcld 10853 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) ∈ ℂ)
416408, 412, 415fsumser 15294 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
417384, 416syl5eq 2790 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
418355, 381, 4173eqtr3d 2785 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
419418mpteq2dva 5150 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
420 fveq2 6717 . . . . . . . . . . . 12 (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
421420mpteq2dv 5151 . . . . . . . . . . 11 (𝑗 = (𝑚 − 1) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
422 eqid 2737 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))
42331mptex 7039 . . . . . . . . . . 11 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V
424421, 422, 423fvmpt 6818 . . . . . . . . . 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 2780 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))
427426mpteq2dva 5150 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))))
4281, 306, 4, 307, 326, 427ulmshft 25282 . . . . . 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 5088 . . . 4 ((𝜑𝑎𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ)(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
431 1nn0 12106 . . . . . 6 1 ∈ ℕ0
432431a1i 11 . . . . 5 ((𝜑𝑎𝑆) → 1 ∈ ℕ0)
433 fzfid 13546 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
434164an32s 652 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
435433, 434fsumcl 15297 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
436435fmpttd 6932 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
43730, 31elmap 8552 . . . . . . 7 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
438436, 437sylibr 237 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵))
439438fmpttd 6932 . . . . 5 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))):ℕ0⟶(ℂ ↑m 𝐵))
4401, 303, 432, 439ulmres 25280 . . . 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 5075 . 2 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
4431, 3, 4, 34, 44, 120, 442ulmdv 25295 1 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2110  {crab 3065  Vcvv 3408  cdif 3863  wss 3866  ifcif 4439  {cpr 4543   class class class wbr 5053  cmpt 5135  ccnv 5550  dom cdm 5551  cres 5553  cima 5554  ccom 5555   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  m cmap 8508  supcsup 9056  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  +∞cpnf 10864  *cxr 10866   < clt 10867  cle 10868  cmin 11062   / cdiv 11489  cn 11830  2c2 11885  0cn0 12090  cz 12176  cuz 12438  +crp 12586  [,)cico 12937  [,]cicc 12938  ...cfz 13095  seqcseq 13574  cexp 13635  abscabs 14797  cli 15045  Σcsu 15249  TopOpenctopn 16926  ∞Metcxmet 20348  ballcbl 20350  fldccnfld 20363  cnccncf 23773   D cdv 24760  𝑢culm 25268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808  ax-mulf 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-supp 7904  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-pm 8511  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fsupp 8986  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-z 12177  df-dec 12294  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-seq 13575  df-exp 13636  df-hash 13897  df-shft 14630  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-limsup 15032  df-clim 15049  df-rlim 15050  df-sum 15250  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-ress 16785  df-plusg 16815  df-mulr 16816  df-starv 16817  df-sca 16818  df-vsca 16819  df-ip 16820  df-tset 16821  df-ple 16822  df-ds 16824  df-unif 16825  df-hom 16826  df-cco 16827  df-rest 16927  df-topn 16928  df-0g 16946  df-gsum 16947  df-topgen 16948  df-pt 16949  df-prds 16952  df-xrs 17007  df-qtop 17012  df-imas 17013  df-xps 17015  df-mre 17089  df-mrc 17090  df-acs 17092  df-mgm 18114  df-sgrp 18163  df-mnd 18174  df-submnd 18219  df-mulg 18489  df-cntz 18711  df-cmn 19172  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-fbas 20360  df-fg 20361  df-cnfld 20364  df-top 21791  df-topon 21808  df-topsp 21830  df-bases 21843  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-lp 22033  df-perf 22034  df-cn 22124  df-cnp 22125  df-haus 22212  df-cmp 22284  df-tx 22459  df-hmeo 22652  df-fil 22743  df-fm 22835  df-flim 22836  df-flf 22837  df-xms 23218  df-ms 23219  df-tms 23220  df-cncf 23775  df-limc 24763  df-dv 24764  df-ulm 25269
This theorem is referenced by:  pserdv  25321
  Copyright terms: Public domain W3C validator