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

Theorem pserdvlem2 24933
Description: Lemma for pserdv 24934. (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 12272 . 2 0 = (ℤ‘0)
2 cnelprrecn 10622 . . 3 ℂ ∈ {ℝ, ℂ}
32a1i 11 . 2 ((𝜑𝑎𝑆) → ℂ ∈ {ℝ, ℂ})
4 0zd 11985 . 2 ((𝜑𝑎𝑆) → 0 ∈ ℤ)
5 fzfid 13334 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑘) ∈ Fin)
6 pserf.g . . . . . . . 8 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
7 pserf.a . . . . . . . . 9 (𝜑𝐴:ℕ0⟶ℂ)
87ad3antrrr 726 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
9 pserdv.b . . . . . . . . . . 11 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
10 cnxmet 23298 . . . . . . . . . . . 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 24932 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
1716simp1d 1136 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+)
1817rpxrd 12425 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
19 blssm 22945 . . . . . . . . . . . 12 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
2010, 11, 18, 19mp3an2i 1459 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
219, 20eqsstrid 4018 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝐵 ⊆ ℂ)
2221adantr 481 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℂ)
2322sselda 3970 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
246, 8, 23psergf 24917 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
25 elfznn0 12993 . . . . . . 7 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0)
26 ffvelrn 6844 . . . . . . 7 (((𝐺𝑦):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
2724, 25, 26syl2an 595 . . . . . 6 (((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
285, 27fsumcl 15082 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) ∈ ℂ)
2928fmpttd 6874 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
30 cnex 10610 . . . . 5 ℂ ∈ V
319ovexi 7185 . . . . 5 𝐵 ∈ V
3230, 31elmap 8428 . . . 4 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)):𝐵⟶ℂ)
3329, 32sylibr 235 . . 3 (((𝜑𝑎𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵))
3433fmpttd 6874 . 2 ((𝜑𝑎𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))):ℕ0⟶(ℂ ↑m 𝐵))
356, 12, 7, 13, 14, 15psercn 24931 . . . . 5 (𝜑𝐹 ∈ (𝑆cn→ℂ))
36 cncff 23418 . . . . 5 (𝐹 ∈ (𝑆cn→ℂ) → 𝐹:𝑆⟶ℂ)
3735, 36syl 17 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
3837adantr 481 . . 3 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
396, 12, 7, 13, 14, 16psercnlem2 24929 . . . . . 6 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆))
4039simp2d 1137 . . . . 5 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
419, 40eqsstrid 4018 . . . 4 ((𝜑𝑎𝑆) → 𝐵 ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))))
4239simp3d 1138 . . . 4 ((𝜑𝑎𝑆) → (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)
4341, 42sstrd 3980 . . 3 ((𝜑𝑎𝑆) → 𝐵𝑆)
4438, 43fssresd 6541 . 2 ((𝜑𝑎𝑆) → (𝐹𝐵):𝐵⟶ℂ)
45 0zd 11985 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℤ)
46 eqidd 2826 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) = ((𝐺𝑧)‘𝑗))
477ad2antrr 722 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝐴:ℕ0⟶ℂ)
4821sselda 3970 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ ℂ)
496, 47, 48psergf 24917 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐺𝑧):ℕ0⟶ℂ)
5049ffvelrnda 6846 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑧)‘𝑗) ∈ ℂ)
5148abscld 14789 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ)
5251rexrd 10683 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) ∈ ℝ*)
5318adantr 481 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
54 iccssxr 12812 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
556, 7, 13radcnvcl 24922 . . . . . . . . 9 (𝜑𝑅 ∈ (0[,]+∞))
5654, 55sseldi 3968 . . . . . . . 8 (𝜑𝑅 ∈ ℝ*)
5756ad2antrr 722 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑅 ∈ ℝ*)
58 0cn 10625 . . . . . . . . . 10 0 ∈ ℂ
59 eqid 2825 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
6059cnmetdval 23296 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6148, 58, 60sylancl 586 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
6248subid1d 10978 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 − 0) = 𝑧)
6362fveq2d 6670 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
6461, 63eqtrd 2860 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
65 simpr 485 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝐵)
6665, 9syl6eleq 2927 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)))
6710a1i 11 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
68 0cnd 10626 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 0 ∈ ℂ)
69 elbl3 22919 . . . . . . . . . 10 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7067, 53, 68, 48, 69syl22anc 836 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2)))
7166, 70mpbid 233 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑧(abs ∘ − )0) < (((abs‘𝑎) + 𝑀) / 2))
7264, 71eqbrtrrd 5086 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2))
7316simp3d 1138 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7473adantr 481 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅)
7552, 53, 57, 72, 74xrlttrd 12545 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (abs‘𝑧) < 𝑅)
766, 47, 13, 48, 75radcnvlt2 24924 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ∈ dom ⇝ )
771, 45, 46, 50, 76isumclim2 15105 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
7843sselda 3970 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → 𝑧𝑆)
79 fveq2 6666 . . . . . . . 8 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
8079fveq1d 6668 . . . . . . 7 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑗) = ((𝐺𝑧)‘𝑗))
8180sumeq2sdv 15053 . . . . . 6 (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
82 sumex 15037 . . . . . 6 Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗) ∈ V
8381, 12, 82fvmpt 6764 . . . . 5 (𝑧𝑆 → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8478, 83syl 17 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝐹𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺𝑧)‘𝑗))
8577, 84breqtrrd 5090 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → seq0( + , (𝐺𝑧)) ⇝ (𝐹𝑧))
86 oveq2 7159 . . . . . . . . . . 11 (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚))
8786sumeq1d 15050 . . . . . . . . . 10 (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
8887mpteq2dv 5158 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
89 eqid 2825 . . . . . . . . 9 (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))
9031mptex 6984 . . . . . . . . 9 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) ∈ V
9188, 89, 90fvmpt 6764 . . . . . . . 8 (𝑚 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9291adantl 482 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
9392fveq1d 6668 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧))
9479fveq1d 6668 . . . . . . . . 9 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑖) = ((𝐺𝑧)‘𝑖))
9594sumeq2sdv 15053 . . . . . . . 8 (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
96 eqid 2825 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))
97 sumex 15037 . . . . . . . 8 Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) ∈ V
9895, 96, 97fvmpt 6764 . . . . . . 7 (𝑧𝐵 → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
9998ad2antlr 723 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖))
100 eqidd 2826 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) = ((𝐺𝑧)‘𝑖))
101 simpr 485 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
102101, 1syl6eleq 2927 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ‘0))
10349adantr 481 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺𝑧):ℕ0⟶ℂ)
104 elfznn0 12993 . . . . . . . 8 (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0)
105 ffvelrn 6844 . . . . . . . 8 (((𝐺𝑧):ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
106103, 104, 105syl2an 595 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺𝑧)‘𝑖) ∈ ℂ)
107100, 102, 106fsumser 15079 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑚)((𝐺𝑧)‘𝑖) = (seq0( + , (𝐺𝑧))‘𝑚))
10893, 99, 1073eqtrd 2864 . . . . 5 ((((𝜑𝑎𝑆) ∧ 𝑧𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺𝑧))‘𝑚))
109108mpteq2dva 5157 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
110 0z 11984 . . . . . . 7 0 ∈ ℤ
111 seqfn 13374 . . . . . . 7 (0 ∈ ℤ → seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
112110, 111ax-mp 5 . . . . . 6 seq0( + , (𝐺𝑧)) Fn (ℤ‘0)
1131fneq2i 6447 . . . . . 6 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) Fn (ℤ‘0))
114112, 113mpbir 232 . . . . 5 seq0( + , (𝐺𝑧)) Fn ℕ0
115 dffn5 6720 . . . . 5 (seq0( + , (𝐺𝑧)) Fn ℕ0 ↔ seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚)))
116114, 115mpbi 231 . . . 4 seq0( + , (𝐺𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( + , (𝐺𝑧))‘𝑚))
117109, 116syl6eqr 2878 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺𝑧)))
118 fvres 6685 . . . 4 (𝑧𝐵 → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
119118adantl 482 . . 3 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
12085, 117, 1193brtr4d 5094 . 2 (((𝜑𝑎𝑆) ∧ 𝑧𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹𝐵)‘𝑧))
12191adantl 482 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖)))
122121oveq2d 7167 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))))
123 eqid 2825 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
124123cnfldtopon 23308 . . . . . . 7 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
125124toponrestid 21447 . . . . . 6 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
1262a1i 11 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ ∈ {ℝ, ℂ})
127123cnfldtopn 23307 . . . . . . . . . 10 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
128127blopn 23027 . . . . . . . . 9 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
12910, 11, 18, 128mp3an2i 1459 . . . . . . . 8 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ (TopOpen‘ℂfld))
1309, 129eqeltrid 2921 . . . . . . 7 ((𝜑𝑎𝑆) → 𝐵 ∈ (TopOpen‘ℂfld))
131130adantr 481 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈ (TopOpen‘ℂfld))
132 fzfid 13334 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
1337ad2antrr 722 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ)
1341333ad2ant1 1127 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
13521adantr 481 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆ ℂ)
136135sselda 3970 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1371363adant2 1125 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
1386, 134, 137psergf 24917 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → (𝐺𝑦):ℕ0⟶ℂ)
1391043ad2ant2 1128 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
140138, 139ffvelrnd 6847 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) ∈ ℂ)
1412a1i 11 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ, ℂ})
142 ffvelrn 6844 . . . . . . . . . . 11 ((𝐴:ℕ0⟶ℂ ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
143133, 104, 142syl2an 595 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴𝑖) ∈ ℂ)
144143adantr 481 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝐴𝑖) ∈ ℂ)
145136adantlr 711 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
146 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
147104adantl 482 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0)
148 expcl 13440 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
149146, 147, 148syl2anr 596 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦𝑖) ∈ ℂ)
150145, 149syldan 591 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → (𝑦𝑖) ∈ ℂ)
151144, 150mulcld 10653 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
152 ovexd 7186 . . . . . . . 8 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V)
153 c0ex 10627 . . . . . . . . . . 11 0 ∈ V
154 ovex 7184 . . . . . . . . . . 11 (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V
155153, 154ifex 4517 . . . . . . . . . 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 24468 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
159147, 158syl 17 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
16021ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ)
161130ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈ (TopOpen‘ℂfld))
162141, 149, 157, 159, 160, 125, 123, 161dvmptres 24477 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ (𝑦𝑖))) = (𝑦𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
163141, 150, 156, 162, 143dvmptcmul 24478 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
164141, 151, 152, 163dvmptcl 24473 . . . . . . 7 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
1651643impa 1104 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦𝐵) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
166104ad2antlr 723 . . . . . . . . . 10 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → 𝑖 ∈ ℕ0)
1676pserval2 24916 . . . . . . . . . 10 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
168145, 166, 167syl2anc 584 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦𝐵) → ((𝐺𝑦)‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
169168mpteq2dva 5157 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖)) = (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖))))
170169oveq2d 7167 . . . . . . 7 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (ℂ D (𝑦𝐵 ↦ ((𝐴𝑖) · (𝑦𝑖)))))
171170, 163eqtrd 2860 . . . . . 6 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦𝐵 ↦ ((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
172125, 123, 126, 131, 132, 140, 165, 171dvmptfsum 24489 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺𝑦)‘𝑖))) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
173122, 172eqtrd 2860 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)) = (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))
174173mpteq2dva 5157 . . 3 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))))
175 nnssnn0 11892 . . . . . 6 ℕ ⊆ ℕ0
176 resmpt 5903 . . . . . 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 7158 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝑎𝑖) = (𝑥𝑖))
179178oveq2d 7167 . . . . . . . . . . 11 (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)))
180179mpteq2dv 5158 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))))
181 oveq1 7158 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1))
182 fvoveq1 7174 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1)))
183181, 182oveq12d 7169 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
184 oveq2 7159 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → (𝑥𝑖) = (𝑥𝑛))
185183, 184oveq12d 7169 . . . . . . . . . . . 12 (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
186185cbvmptv 5165 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
187 oveq1 7158 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
188 fvoveq1 7174 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1)))
189187, 188oveq12d 7169 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
190 eqid 2825 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))
191 ovex 7184 . . . . . . . . . . . . . 14 ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V
192189, 190, 191fvmpt 6764 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1))))
193192oveq1d 7166 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
194193mpteq2ia 5153 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥𝑛)))
195186, 194eqtr4i 2851 . . . . . . . . . 10 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛)))
196180, 195syl6eq 2876 . . . . . . . . 9 (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
197196cbvmptv 5165 . . . . . . . 8 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥𝑛))))
198 fveq2 6666 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))
199198fveq1d 6668 . . . . . . . . . 10 (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
200199sumeq2sdv 15053 . . . . . . . . 9 (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
201200cbvmptv 5165 . . . . . . . 8 (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑧𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)‘𝑘))
202 peano2nn0 11929 . . . . . . . . . . . 12 (𝑚 ∈ ℕ0 → (𝑚 + 1) ∈ ℕ0)
203202adantl 482 . . . . . . . . . . 11 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℕ0)
204203nn0cnd 11949 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈ ℂ)
205133, 203ffvelrnd 6847 . . . . . . . . . 10 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ)
206204, 205mulcld 10653 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ)
207206fmpttd 6874 . . . . . . . 8 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))):ℕ0⟶ℂ)
208 fveq2 6666 . . . . . . . . . . . 12 (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗))
209208seqeq3d 13370 . . . . . . . . . . 11 (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)))
210209eleq1d 2901 . . . . . . . . . 10 (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ ))
211210cbvrabv 3496 . . . . . . . . 9 {𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }
212211supeq1i 8903 . . . . . . . 8 sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*, < )
213198seqeq3d 13370 . . . . . . . . . . . 12 (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧)))
214213fveq1d 6668 . . . . . . . . . . 11 (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
215214cbvmptv 5165 . . . . . . . . . 10 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗))
216 fveq2 6666 . . . . . . . . . . 11 (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚))
217216mpteq2dv 5158 . . . . . . . . . 10 (𝑗 = 𝑚 → (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
218215, 217syl5eq 2872 . . . . . . . . 9 (𝑗 = 𝑚 → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
219218cbvmptv 5165 . . . . . . . 8 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑧))‘𝑚)))
22017rpred 12424 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ)
2216, 12, 7, 13, 14, 15psercnlem1 24930 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
222221simp1d 1136 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
223222rpxrd 12425 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ*)
224197, 207, 212radcnvcl 24922 . . . . . . . . . 10 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
22554, 224sseldi 3968 . . . . . . . . 9 ((𝜑𝑎𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
226221simp2d 1137 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑀)
227 cnvimass 5946 . . . . . . . . . . . . . . . 16 (abs “ (0[,)𝑅)) ⊆ dom abs
228 absf 14690 . . . . . . . . . . . . . . . . 17 abs:ℂ⟶ℝ
229228fdmi 6520 . . . . . . . . . . . . . . . 16 dom abs = ℂ
230227, 229sseqtri 4006 . . . . . . . . . . . . . . 15 (abs “ (0[,)𝑅)) ⊆ ℂ
23114, 230eqsstri 4004 . . . . . . . . . . . . . 14 𝑆 ⊆ ℂ
232231a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ ℂ)
233232sselda 3970 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
234233abscld 14789 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
235222rpred 12424 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
236 avglt2 11868 . . . . . . . . . . 11 (((abs‘𝑎) ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
237234, 235, 236syl2anc 584 . . . . . . . . . 10 ((𝜑𝑎𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀))
238226, 237mpbid 233 . . . . . . . . 9 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀)
239222rpge0d 12428 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 0 ≤ 𝑀)
240235, 239absidd 14775 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) = 𝑀)
241222rpcnd 12426 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑀 ∈ ℂ)
242 oveq1 7158 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑀 → (𝑤𝑖) = (𝑀𝑖))
243242oveq2d 7167 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
244243mpteq2dv 5158 . . . . . . . . . . . . . . 15 (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
245 oveq1 7158 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝑖) = (𝑤𝑖))
246245oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖)))
247246mpteq2dv 5158 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
248247cbvmptv 5165 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤𝑖))))
249 nn0ex 11895 . . . . . . . . . . . . . . . 16 0 ∈ V
250249mptex 6984 . . . . . . . . . . . . . . 15 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) ∈ V
251244, 248, 250fvmpt 6764 . . . . . . . . . . . . . 14 (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
252241, 251syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))))
253252seqeq3d 13370 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))))
254 fveq2 6666 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
255 oveq2 7159 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
256254, 255oveq12d 7169 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
257256cbvmptv 5165 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖)))
258 oveq1 7158 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
259258oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
260259mpteq2dv 5158 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑥𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
261257, 260syl5eq 2872 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
262261cbvmptv 5165 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
2636, 262eqtri 2848 . . . . . . . . . . . . 13 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴𝑖) · (𝑦𝑖))))
264 fveq2 6666 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (𝐺𝑟) = (𝐺𝑠))
265264seqeq3d 13370 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → seq0( + , (𝐺𝑟)) = seq0( + , (𝐺𝑠)))
266265eleq1d 2901 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑠 → (seq0( + , (𝐺𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺𝑠)) ∈ dom ⇝ ))
267266cbvrabv 3496 . . . . . . . . . . . . . . 15 {𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }
268267supeq1i 8903 . . . . . . . . . . . . . 14 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
26913, 268eqtri 2848 . . . . . . . . . . . . 13 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺𝑠)) ∈ dom ⇝ }, ℝ*, < )
270 eqid 2825 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))
2717adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝐴:ℕ0⟶ℂ)
272221simp3d 1138 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → 𝑀 < 𝑅)
273240, 272eqbrtrd 5084 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (abs‘𝑀) < 𝑅)
274263, 269, 270, 271, 241, 273dvradcnv 24926 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀𝑖)))) ∈ dom ⇝ )
275253, 274eqeltrd 2917 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑀)) ∈ dom ⇝ )
276197, 207, 212, 241, 275radcnvle 24925 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
277240, 276eqbrtrrd 5086 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
27818, 223, 225, 238, 277xrltletrd 12547 . . . . . . . 8 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
279197, 201, 207, 212, 219, 220, 278, 41pserulm 24927 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)))
28021sselda 3970 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
281 oveq1 7158 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → (𝑎𝑖) = (𝑦𝑖))
282281oveq2d 7167 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
283282mpteq2dv 5158 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
284 eqid 2825 . . . . . . . . . . . . . 14 (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))
285249mptex 6984 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) ∈ V
286283, 284, 285fvmpt 6764 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
287280, 286syl 17 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
288287adantr 481 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
289288fveq1d 6668 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
290 oveq1 7158 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
291 fvoveq1 7174 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1)))
292290, 291oveq12d 7169 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
293 oveq2 7159 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑦𝑖) = (𝑦𝑘))
294292, 293oveq12d 7169 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
295 eqid 2825 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))
296 ovex 7184 . . . . . . . . . . . 12 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V
297294, 295, 296fvmpt 6764 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
298297adantl 482 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
299289, 298eqtrd 2860 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
300299sumeq2dv 15052 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
301300mpteq2dva 5157 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
302279, 301breqtrd 5088 . . . . . 6 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
303 nnuz 12273 . . . . . . . 8 ℕ = (ℤ‘1)
304 1e0p1 12132 . . . . . . . . 9 1 = (0 + 1)
305304fveq2i 6669 . . . . . . . 8 (ℤ‘1) = (ℤ‘(0 + 1))
306303, 305eqtri 2848 . . . . . . 7 ℕ = (ℤ‘(0 + 1))
307 1zzd 12005 . . . . . . 7 ((𝜑𝑎𝑆) → 1 ∈ ℤ)
308 0zd 11985 . . . . . . . . . . . . 13 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 0 ∈ ℤ)
309 peano2nn0 11929 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
310309nn0cnd 11949 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℂ)
311310adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈ ℂ)
3127ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
313 ffvelrn 6844 . . . . . . . . . . . . . . . . . 18 ((𝐴:ℕ0⟶ℂ ∧ (𝑖 + 1) ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
314312, 309, 313syl2an 595 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ)
315311, 314mulcld 10653 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ)
316280, 148sylan 580 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
317315, 316mulcld 10653 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)) ∈ ℂ)
318287, 317fmpt3d 6875 . . . . . . . . . . . . . 14 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦):ℕ0⟶ℂ)
319318ffvelrnda 6846 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑚) ∈ ℂ)
3201, 308, 319serf 13391 . . . . . . . . . . . 12 (((𝜑𝑎𝑆) ∧ 𝑦𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)):ℕ0⟶ℂ)
321320ffvelrnda 6846 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑦𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
322321an32s 648 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) ∈ ℂ)
323322fmpttd 6874 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
32430, 31elmap 8428 . . . . . . . . 9 ((𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ)
325323, 324sylibr 235 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵))
326325fmpttd 6874 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ ↑m 𝐵))
327 elfznn 12929 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ)
328327nnne0d 11679 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0)
329328neneqd 3025 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0)
330329iffalsed 4480 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1))))
331330oveq2d 7167 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑚) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
332331sumeq2i 15048 . . . . . . . . . . . 12 Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))
333 1zzd 12005 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 1 ∈ ℤ)
334 nnz 11996 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
335334ad2antlr 723 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑚 ∈ ℤ)
336271ad2antrr 722 . . . . . . . . . . . . . . 15 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝐴:ℕ0⟶ℂ)
337327nnnn0d 11947 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0)
338336, 337, 142syl2an 595 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴𝑖) ∈ ℂ)
339327adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ)
340339nncnd 11646 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ)
341280adantlr 711 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → 𝑦 ∈ ℂ)
342 nnm1nn0 11930 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ → (𝑖 − 1) ∈ ℕ0)
343327, 342syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈ ℕ0)
344 expcl 13440 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈ ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
345341, 343, 344syl2an 595 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ)
346340, 345mulcld 10653 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈ ℂ)
347338, 346mulcld 10653 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ ℂ)
348 fveq2 6666 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝐴𝑖) = (𝐴‘(𝑘 + 1)))
349 id 22 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1))
350 oveq1 7158 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1))
351350oveq2d 7167 . . . . . . . . . . . . . . 15 (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1)))
352349, 351oveq12d 7169 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
353348, 352oveq12d 7169 . . . . . . . . . . . . 13 (𝑖 = (𝑘 + 1) → ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
354333, 333, 335, 347, 353fsumshftm 15128 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
355332, 354syl5eq 2872 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
356 fz1ssfz0 12996 . . . . . . . . . . . . 13 (1...𝑚) ⊆ (0...𝑚)
357356a1i 11 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (1...𝑚) ⊆ (0...𝑚))
358331adantl 482 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))))
359358, 347eqeltrd 2917 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
360 eldif 3949 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)))
361 elfzuz2 12905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑚) → 𝑚 ∈ (ℤ‘0))
362 elfzp12 12979 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (ℤ‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
363361, 362syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))))
364363ibi 268 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))
365364ord 860 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...𝑚) → (¬ 𝑖 = 0 → 𝑖 ∈ ((0 + 1)...𝑚)))
366365con1d 147 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (0...𝑚) → (¬ 𝑖 ∈ ((0 + 1)...𝑚) → 𝑖 = 0))
367366imp 407 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)) → 𝑖 = 0)
368360, 367sylbi 218 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) → 𝑖 = 0)
369304oveq1i 7161 . . . . . . . . . . . . . . . . . 18 (1...𝑚) = ((0 + 1)...𝑚)
370369difeq2i 4099 . . . . . . . . . . . . . . . . 17 ((0...𝑚) ∖ (1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚))
371368, 370eleq2s 2935 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0)
372371adantl 482 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0)
373372iftrued 4477 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0)
374373oveq2d 7167 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴𝑖) · 0))
375 eldifi 4106 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚))
376375, 104syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0)
377336, 376, 142syl2an 595 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴𝑖) ∈ ℂ)
378377mul01d 10831 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · 0) = 0)
379374, 378eqtrd 2860 . . . . . . . . . . . 12 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0)
380 fzfid 13334 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
381357, 359, 379, 380fsumss 15074 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))
382 1m1e0 11701 . . . . . . . . . . . . . 14 (1 − 1) = 0
383382oveq1i 7161 . . . . . . . . . . . . 13 ((1 − 1)...(𝑚 − 1)) = (0...(𝑚 − 1))
384383sumeq1i 15047 . . . . . . . . . . . 12 Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))
385 elfznn0 12993 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...(𝑚 − 1)) → 𝑘 ∈ ℕ0)
386385adantl 482 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℕ0)
387386, 297syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
388341adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑦 ∈ ℂ)
389388, 286syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖))))
390389fveq1d 6668 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦𝑖)))‘𝑘))
391336adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ)
392 peano2nn0 11929 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
393386, 392syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℕ0)
394391, 393ffvelrnd 6847 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ)
395393nn0cnd 11949 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ)
396 expcl 13440 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
397341, 385, 396syl2an 595 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦𝑘) ∈ ℂ)
398394, 395, 397mul12d 10841 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
399386nn0cnd 11949 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ)
400 ax-1cn 10587 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
401 pncan 10884 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
402399, 400, 401sylancl 586 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘)
403402oveq2d 7167 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦𝑘))
404403oveq2d 7167 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦𝑘)))
405404oveq2d 7167 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦𝑘))))
406395, 394, 397mulassd 10656 . . . . . . . . . . . . . . 15 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦𝑘))))
407398, 405, 4063eqtr4d 2870 . . . . . . . . . . . . . 14 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
408387, 390, 4073eqtr4d 2870 . . . . . . . . . . . . 13 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))))
409 nnm1nn0 11930 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → (𝑚 − 1) ∈ ℕ0)
410409adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈ ℕ0)
411410adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ ℕ0)
412411, 1syl6eleq 2927 . . . . . . . . . . . . 13 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → (𝑚 − 1) ∈ (ℤ‘0))
413403, 397eqeltrd 2917 . . . . . . . . . . . . . . 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 15079 . . . . . . . . . . . 12 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
417384, 416syl5eq 2872 . . . . . . . . . . 11 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
418355, 381, 4173eqtr3d 2868 . . . . . . . . . 10 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
419418mpteq2dva 5157 . . . . . . . . 9 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
420 fveq2 6666 . . . . . . . . . . . 12 (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1)))
421420mpteq2dv 5158 . . . . . . . . . . 11 (𝑗 = (𝑚 − 1) → (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)) = (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))))
422 eqid 2825 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))
42331mptex 6984 . . . . . . . . . . 11 (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V
424421, 422, 423fvmpt 6764 . . . . . . . . . 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 2863 . . . . . . . 8 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))
427426mpteq2dva 5157 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))))
4281, 306, 4, 307, 326, 427ulmshft 24895 . . . . . 6 ((𝜑𝑎𝑆) → ((𝑗 ∈ ℕ0 ↦ (𝑦𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎𝑖))))‘𝑦))‘𝑗)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) ↔ (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))))
429302, 428mpbid 233 . . . . 5 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
430177, 429eqbrtrid 5097 . . . 4 ((𝜑𝑎𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ)(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
431 1nn0 11905 . . . . . 6 1 ∈ ℕ0
432431a1i 11 . . . . 5 ((𝜑𝑎𝑆) → 1 ∈ ℕ0)
433 fzfid 13334 . . . . . . . . 9 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → (0...𝑚) ∈ Fin)
434164an32s 648 . . . . . . . . 9 (((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
435433, 434fsumcl 15082 . . . . . . . 8 ((((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ ℂ)
436435fmpttd 6874 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
43730, 31elmap 8428 . . . . . . 7 ((𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵) ↔ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ)
438436, 437sylibr 235 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ ↑m 𝐵))
439438fmpttd 6874 . . . . 5 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))):ℕ0⟶(ℂ ↑m 𝐵))
4401, 303, 432, 439ulmres 24893 . . . 4 ((𝜑𝑎𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) ↔ ((𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ)(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))))
441430, 440mpbird 258 . . 3 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
442174, 441eqbrtrd 5084 . 2 ((𝜑𝑎𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ D ((𝑘 ∈ ℕ0 ↦ (𝑦𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺𝑦)‘𝑖)))‘𝑚)))(⇝𝑢𝐵)(𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
4431, 3, 4, 34, 44, 120, 442ulmdv 24908 1 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2107  {crab 3146  Vcvv 3499  cdif 3936  wss 3939  ifcif 4469  {cpr 4565   class class class wbr 5062  cmpt 5142  ccnv 5552  dom cdm 5553  cres 5555  cima 5556  ccom 5557   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  m cmap 8399  supcsup 8896  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 11630  2c2 11684  0cn0 11889  cz 11973  cuz 12235  +crp 12382  [,)cico 12733  [,]cicc 12734  ...cfz 12885  seqcseq 13362  cexp 13422  abscabs 14586  cli 14834  Σcsu 15035  TopOpenctopn 16687  ∞Metcxmet 20448  ballcbl 20450  fldccnfld 20463  cnccncf 23401   D cdv 24378  𝑢culm 24881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  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 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  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 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ico 12737  df-icc 12738  df-fz 12886  df-fzo 13027  df-fl 13155  df-seq 13363  df-exp 13423  df-hash 13684  df-shft 14419  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-limsup 14821  df-clim 14838  df-rlim 14839  df-sum 15036  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-submnd 17947  df-mulg 18157  df-cntz 18379  df-cmn 18830  df-psmet 20455  df-xmet 20456  df-met 20457  df-bl 20458  df-mopn 20459  df-fbas 20460  df-fg 20461  df-cnfld 20464  df-top 21420  df-topon 21437  df-topsp 21459  df-bases 21472  df-cld 21545  df-ntr 21546  df-cls 21547  df-nei 21624  df-lp 21662  df-perf 21663  df-cn 21753  df-cnp 21754  df-haus 21841  df-cmp 21913  df-tx 22088  df-hmeo 22281  df-fil 22372  df-fm 22464  df-flim 22465  df-flf 22466  df-xms 22847  df-ms 22848  df-tms 22849  df-cncf 23403  df-limc 24381  df-dv 24382  df-ulm 24882
This theorem is referenced by:  pserdv  24934
  Copyright terms: Public domain W3C validator