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

Theorem abelthlem9 25799
Description: Lemma for abelth 25800. By adjusting the constant term, we can assume that the entire series converges to 0. (Contributed by Mario Carneiro, 1-Apr-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
Assertion
Ref Expression
abelthlem9 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅))
Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧,𝑀   𝑅,𝑛,𝑤,𝑥,𝑦,𝑧   𝐴,𝑛,𝑤,𝑥,𝑦,𝑧   𝜑,𝑛,𝑤,𝑥,𝑦   𝑤,𝐹,𝑦   𝑆,𝑛,𝑤,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑛)

Proof of Theorem abelthlem9
Dummy variables 𝑖 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abelth.1 . . . . . . 7 (𝜑𝐴:ℕ0⟶ℂ)
2 0nn0 12428 . . . . . . . 8 0 ∈ ℕ0
32a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0 → 0 ∈ ℕ0)
4 ffvelcdm 7032 . . . . . . 7 ((𝐴:ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
51, 3, 4syl2an 596 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
6 nn0uz 12805 . . . . . . . 8 0 = (ℤ‘0)
7 0zd 12511 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
8 eqidd 2737 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) = (𝐴𝑚))
91ffvelcdmda 7035 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) ∈ ℂ)
10 abelth.2 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
116, 7, 8, 9, 10isumcl 15646 . . . . . . 7 (𝜑 → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
1211adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
135, 12subcld 11512 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
141ffvelcdmda 7035 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
1513, 14ifcld 4532 . . . 4 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
1615fmpttd 7063 . . 3 (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))):ℕ0⟶ℂ)
172a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
1816ffvelcdmda 7035 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) ∈ ℂ)
19 1e0p1 12660 . . . . . . . . . 10 1 = (0 + 1)
20 1z 12533 . . . . . . . . . 10 1 ∈ ℤ
2119, 20eqeltrri 2835 . . . . . . . . 9 (0 + 1) ∈ ℤ
2221a1i 11 . . . . . . . 8 (𝜑 → (0 + 1) ∈ ℤ)
23 nnuz 12806 . . . . . . . . . . 11 ℕ = (ℤ‘1)
2419fveq2i 6845 . . . . . . . . . . 11 (ℤ‘1) = (ℤ‘(0 + 1))
2523, 24eqtri 2764 . . . . . . . . . 10 ℕ = (ℤ‘(0 + 1))
2625eleq2i 2829 . . . . . . . . 9 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘(0 + 1)))
27 nnnn0 12420 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
2827adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
29 eqeq1 2740 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘 = 0 ↔ 𝑖 = 0))
30 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝐴𝑘) = (𝐴𝑖))
3129, 30ifbieq2d 4512 . . . . . . . . . . . 12 (𝑘 = 𝑖 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
32 eqid 2736 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))
33 ovex 7390 . . . . . . . . . . . . 13 ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ V
34 fvex 6855 . . . . . . . . . . . . 13 (𝐴𝑖) ∈ V
3533, 34ifex 4536 . . . . . . . . . . . 12 if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ V
3631, 32, 35fvmpt 6948 . . . . . . . . . . 11 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
3728, 36syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
38 nnne0 12187 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → 𝑖 ≠ 0)
3938adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → 𝑖 ≠ 0)
4039neneqd 2948 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → ¬ 𝑖 = 0)
4140iffalsed 4497 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) = (𝐴𝑖))
4237, 41eqtrd 2776 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4326, 42sylan2br 595 . . . . . . . 8 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4422, 43seqfeq 13933 . . . . . . 7 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) = seq(0 + 1)( + , 𝐴))
456, 7, 8, 9, 10isumclim2 15643 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴) ⇝ Σ𝑚 ∈ ℕ0 (𝐴𝑚))
466, 17, 14, 45clim2ser 15539 . . . . . . . 8 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)))
47 0z 12510 . . . . . . . . . 10 0 ∈ ℤ
48 seq1 13919 . . . . . . . . . 10 (0 ∈ ℤ → (seq0( + , 𝐴)‘0) = (𝐴‘0))
4947, 48ax-mp 5 . . . . . . . . 9 (seq0( + , 𝐴)‘0) = (𝐴‘0)
5049oveq2i 7368 . . . . . . . 8 𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0))
5146, 50breqtrdi 5146 . . . . . . 7 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
5244, 51eqbrtrd 5127 . . . . . 6 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
536, 17, 18, 52clim2ser2 15540 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)))
54 seq1 13919 . . . . . . . . 9 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘0))
5547, 54ax-mp 5 . . . . . . . 8 (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘0)
56 iftrue 4492 . . . . . . . . . 10 (𝑘 = 0 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
5756, 32, 33fvmpt 6948 . . . . . . . . 9 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
582, 57ax-mp 5 . . . . . . . 8 ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))
5955, 58eqtri 2764 . . . . . . 7 (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))
6059oveq2i 7368 . . . . . 6 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
611, 2, 4sylancl 586 . . . . . . 7 (𝜑 → (𝐴‘0) ∈ ℂ)
62 npncan2 11428 . . . . . . 7 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ ∧ (𝐴‘0) ∈ ℂ) → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6311, 61, 62syl2anc 584 . . . . . 6 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6460, 63eqtrid 2788 . . . . 5 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = 0)
6553, 64breqtrd 5131 . . . 4 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ 0)
66 seqex 13908 . . . . 5 seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ∈ V
67 c0ex 11149 . . . . 5 0 ∈ V
6866, 67breldm 5864 . . . 4 (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ 0 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ∈ dom ⇝ )
6965, 68syl 17 . . 3 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ∈ dom ⇝ )
70 abelth.3 . . 3 (𝜑𝑀 ∈ ℝ)
71 abelth.4 . . 3 (𝜑 → 0 ≤ 𝑀)
72 abelth.5 . . 3 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
73 eqid 2736 . . 3 (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖))) = (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))
7416, 69, 70, 71, 72, 73, 65abelthlem8 25798 . 2 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅))
751, 10, 70, 71, 72abelthlem2 25791 . . . . . . . . . . . . . 14 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
7675simpld 495 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ 𝑆)
7776adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 1 ∈ 𝑆)
7836adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
79 oveq1 7364 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (𝑥𝑖) = (1↑𝑖))
80 nn0z 12524 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ0𝑖 ∈ ℤ)
81 1exp 13997 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℤ → (1↑𝑖) = 1)
8280, 81syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ0 → (1↑𝑖) = 1)
8379, 82sylan9eq 2796 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (𝑥𝑖) = 1)
8478, 83oveq12d 7375 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
8584sumeq2dv 15588 . . . . . . . . . . . . 13 (𝑥 = 1 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
86 sumex 15572 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ V
8785, 73, 86fvmpt 6948 . . . . . . . . . . . 12 (1 ∈ 𝑆 → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
8877, 87syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
89 0zd 12511 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 0 ∈ ℤ)
9036adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9161, 11subcld 11512 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
9291ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
931ffvelcdmda 7035 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9493adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9592, 94ifcld 4532 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ ℂ)
9695mulid1d 11172 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9790, 96eqtr4d 2779 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
9896, 95eqeltrd 2838 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ ℂ)
99 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 1 → (𝑥𝑛) = (1↑𝑛))
100 nn0z 12524 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
101 1exp 13997 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
10399, 102sylan9eq 2796 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → (𝑥𝑛) = 1)
104103oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑛) · 1))
105104sumeq2dv 15588 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1))
106 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → (𝐴𝑛) = (𝐴𝑚))
107106oveq1d 7372 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → ((𝐴𝑛) · 1) = ((𝐴𝑚) · 1))
108107cbvsumv 15581 . . . . . . . . . . . . . . . . . . . 20 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1)
109105, 108eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
110 abelth.6 . . . . . . . . . . . . . . . . . . 19 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
111 sumex 15572 . . . . . . . . . . . . . . . . . . 19 Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) ∈ V
112109, 110, 111fvmpt 6948 . . . . . . . . . . . . . . . . . 18 (1 ∈ 𝑆 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
11376, 112syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
1149mulid1d 11172 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ0) → ((𝐴𝑚) · 1) = (𝐴𝑚))
115114sumeq2dv 15588 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
116113, 115eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
117116oveq1d 7372 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
11811subidd 11500 . . . . . . . . . . . . . . 15 (𝜑 → (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
119117, 118eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
12065, 119breqtrrd 5133 . . . . . . . . . . . . 13 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
121120adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
1226, 89, 97, 98, 121isumclim 15642 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
12388, 122eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
124 oveq1 7364 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
12536, 124oveqan12rd 7377 . . . . . . . . . . . . . 14 ((𝑥 = 𝑦𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
126125sumeq2dv 15588 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
127 sumex 15572 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
128126, 73, 127fvmpt 6948 . . . . . . . . . . . 12 (𝑦𝑆 → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
129128adantl 482 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
130 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → (𝑦𝑘) = (𝑦𝑖))
13131, 130oveq12d 7375 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
132 eqid 2736 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))
133 ovex 7390 . . . . . . . . . . . . . 14 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
134131, 132, 133fvmpt 6948 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
135134adantl 482 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
13672ssrab3 4040 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ℂ
137136a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑆 ⊆ ℂ)
138137sselda 3944 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
139 expcl 13985 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
140138, 139sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
14195, 140mulcld 11175 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ ℂ)
1422a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 0 ∈ ℕ0)
14315adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
144 expcl 13985 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
145138, 144sylan 580 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
146143, 145mulcld 11175 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) ∈ ℂ)
147146fmpttd 7063 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))):ℕ0⟶ℂ)
148147ffvelcdmda 7035 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
14941oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
15028, 134syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
15130, 130oveq12d 7375 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴𝑖) · (𝑦𝑖)))
152 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))
153 ovex 7390 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
154151, 152, 153fvmpt 6948 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
15528, 154syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
156149, 150, 1553eqtr4d 2786 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15726, 156sylan2br 595 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15822, 157seqfeq 13933 . . . . . . . . . . . . . . . 16 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) = seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))))
159158adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) = seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))))
16014adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
161160, 145mulcld 11175 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑦𝑘)) ∈ ℂ)
162161fmpttd 7063 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))):ℕ0⟶ℂ)
163162ffvelcdmda 7035 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
164154adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
16594, 140mulcld 11175 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
1661, 10, 70, 71, 72abelthlem3 25792 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ∈ dom ⇝ )
1676, 89, 164, 165, 166isumclim2 15643 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
168 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
169 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
170168, 169oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
171170cbvsumv 15581 . . . . . . . . . . . . . . . . . . . . 21 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖))
172124oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
173172sumeq2sdv 15589 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
174171, 173eqtrid 2788 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
175 sumex 15572 . . . . . . . . . . . . . . . . . . . 20 Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
176174, 110, 175fvmpt 6948 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑆 → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
177176adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
178167, 177breqtrrd 5133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ (𝐹𝑦))
1796, 142, 163, 178clim2ser 15539 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)))
180 seq1 13919 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0))
18147, 180ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0)
182 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
183 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝑦𝑘) = (𝑦↑0))
184182, 183oveq12d 7375 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴‘0) · (𝑦↑0)))
185 ovex 7390 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴‘0) · (𝑦↑0)) ∈ V
186184, 152, 185fvmpt 6948 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0)))
1872, 186ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0))
188181, 187eqtri 2764 . . . . . . . . . . . . . . . . . 18 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝐴‘0) · (𝑦↑0))
189138exp0d 14045 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝑦↑0) = 1)
190189oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = ((𝐴‘0) · 1))
19161adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝐴‘0) ∈ ℂ)
192191mulid1d 11172 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · 1) = (𝐴‘0))
193190, 192eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = (𝐴‘0))
194188, 193eqtrid 2788 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = (𝐴‘0))
195194oveq2d 7373 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − (𝐴‘0)))
196179, 195breqtrd 5131 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
197159, 196eqbrtrd 5127 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
1986, 142, 148, 197clim2ser2 15540 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)))
199 seq1 13919 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘0))
20047, 199ax-mp 5 . . . . . . . . . . . . . . . . 17 (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘0)
20156, 183oveq12d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)))
202 ovex 7390 . . . . . . . . . . . . . . . . . . 19 (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) ∈ V
203201, 132, 202fvmpt 6948 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘0) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)))
2042, 203ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘0) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0))
205200, 204eqtri 2764 . . . . . . . . . . . . . . . 16 (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0))
206189oveq2d 7373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1))
20711adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
208191, 207subcld 11512 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
209208mulid1d 11172 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
210206, 209eqtrd 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
211205, 210eqtrid 2788 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
212211oveq2d 7373 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
2131, 10, 70, 71, 72, 110abelthlem4 25793 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑆⟶ℂ)
214213ffvelcdmda 7035 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝐹𝑦) ∈ ℂ)
215214, 191, 207npncand 11536 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
216212, 215eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
217198, 216breqtrd 5131 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
2186, 89, 135, 141, 217isumclim 15642 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
219129, 218eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
220123, 219oveq12d 7375 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
221213adantr 481 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝐹:𝑆⟶ℂ)
222221, 77ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝐹‘1) ∈ ℂ)
223222, 214, 207nnncan2d 11547 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹‘1) − (𝐹𝑦)))
224220, 223eqtrd 2776 . . . . . . . 8 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = ((𝐹‘1) − (𝐹𝑦)))
225224fveq2d 6846 . . . . . . 7 ((𝜑𝑦𝑆) → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) = (abs‘((𝐹‘1) − (𝐹𝑦))))
226225breq1d 5115 . . . . . 6 ((𝜑𝑦𝑆) → ((abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅 ↔ (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅))
227226imbi2d 340 . . . . 5 ((𝜑𝑦𝑆) → (((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
228227ralbidva 3172 . . . 4 (𝜑 → (∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
229228rexbidv 3175 . . 3 (𝜑 → (∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
230229adantr 481 . 2 ((𝜑𝑅 ∈ ℝ+) → (∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
23174, 230mpbid 231 1 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  cdif 3907  wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188  dom cdm 5633  ccom 5637  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  cn 12153  0cn0 12413  cz 12499  cuz 12763  +crp 12915  seqcseq 13906  cexp 13967  abscabs 15119  cli 15366  Σcsu 15570  ballcbl 20783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-xadd 13034  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791
This theorem is referenced by:  abelth  25800
  Copyright terms: Public domain W3C validator