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

Theorem abelthlem9 25119
 Description: Lemma for abelth 25120. 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 11934 . . . . . . . 8 0 ∈ ℕ0
32a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0 → 0 ∈ ℕ0)
4 ffvelrn 6833 . . . . . . 7 ((𝐴:ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
51, 3, 4syl2an 599 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
6 nn0uz 12305 . . . . . . . 8 0 = (ℤ‘0)
7 0zd 12017 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
8 eqidd 2760 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) = (𝐴𝑚))
91ffvelrnda 6835 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) ∈ ℂ)
10 abelth.2 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
116, 7, 8, 9, 10isumcl 15149 . . . . . . 7 (𝜑 → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
1211adantr 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
135, 12subcld 11020 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
141ffvelrnda 6835 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
1513, 14ifcld 4459 . . . 4 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
1615fmpttd 6863 . . 3 (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))):ℕ0⟶ℂ)
172a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
1816ffvelrnda 6835 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) ∈ ℂ)
19 1e0p1 12164 . . . . . . . . . 10 1 = (0 + 1)
20 1z 12036 . . . . . . . . . 10 1 ∈ ℤ
2119, 20eqeltrri 2848 . . . . . . . . 9 (0 + 1) ∈ ℤ
2221a1i 11 . . . . . . . 8 (𝜑 → (0 + 1) ∈ ℤ)
23 nnuz 12306 . . . . . . . . . . 11 ℕ = (ℤ‘1)
2419fveq2i 6654 . . . . . . . . . . 11 (ℤ‘1) = (ℤ‘(0 + 1))
2523, 24eqtri 2782 . . . . . . . . . 10 ℕ = (ℤ‘(0 + 1))
2625eleq2i 2842 . . . . . . . . 9 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘(0 + 1)))
27 nnnn0 11926 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
2827adantl 486 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
29 eqeq1 2763 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘 = 0 ↔ 𝑖 = 0))
30 fveq2 6651 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝐴𝑘) = (𝐴𝑖))
3129, 30ifbieq2d 4439 . . . . . . . . . . . 12 (𝑘 = 𝑖 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
32 eqid 2759 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))
33 ovex 7176 . . . . . . . . . . . . 13 ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ V
34 fvex 6664 . . . . . . . . . . . . 13 (𝐴𝑖) ∈ V
3533, 34ifex 4463 . . . . . . . . . . . 12 if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ V
3631, 32, 35fvmpt 6752 . . . . . . . . . . 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 11693 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → 𝑖 ≠ 0)
3938adantl 486 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → 𝑖 ≠ 0)
4039neneqd 2954 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → ¬ 𝑖 = 0)
4140iffalsed 4424 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) = (𝐴𝑖))
4237, 41eqtrd 2794 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4326, 42sylan2br 598 . . . . . . . 8 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4422, 43seqfeq 13430 . . . . . . 7 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) = seq(0 + 1)( + , 𝐴))
456, 7, 8, 9, 10isumclim2 15146 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴) ⇝ Σ𝑚 ∈ ℕ0 (𝐴𝑚))
466, 17, 14, 45clim2ser 15044 . . . . . . . 8 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)))
47 0z 12016 . . . . . . . . . 10 0 ∈ ℤ
48 seq1 13416 . . . . . . . . . 10 (0 ∈ ℤ → (seq0( + , 𝐴)‘0) = (𝐴‘0))
4947, 48ax-mp 5 . . . . . . . . 9 (seq0( + , 𝐴)‘0) = (𝐴‘0)
5049oveq2i 7154 . . . . . . . 8 𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0))
5146, 50breqtrdi 5066 . . . . . . 7 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
5244, 51eqbrtrd 5047 . . . . . 6 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
536, 17, 18, 52clim2ser2 15045 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)))
54 seq1 13416 . . . . . . . . 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 4419 . . . . . . . . . 10 (𝑘 = 0 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
5756, 32, 33fvmpt 6752 . . . . . . . . 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 2782 . . . . . . 7 (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))
6059oveq2i 7154 . . . . . 6 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
611, 2, 4sylancl 590 . . . . . . 7 (𝜑 → (𝐴‘0) ∈ ℂ)
62 npncan2 10936 . . . . . . 7 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ ∧ (𝐴‘0) ∈ ℂ) → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6311, 61, 62syl2anc 588 . . . . . 6 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6460, 63syl5eq 2806 . . . . 5 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = 0)
6553, 64breqtrd 5051 . . . 4 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ 0)
66 seqex 13405 . . . . 5 seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ∈ V
67 c0ex 10658 . . . . 5 0 ∈ V
6866, 67breldm 5741 . . . 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 2759 . . 3 (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖))) = (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))
7416, 69, 70, 71, 72, 73, 65abelthlem8 25118 . 2 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅))
751, 10, 70, 71, 72abelthlem2 25111 . . . . . . . . . . . . . 14 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
7675simpld 499 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ 𝑆)
7776adantr 485 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 1 ∈ 𝑆)
7836adantl 486 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
79 oveq1 7150 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (𝑥𝑖) = (1↑𝑖))
80 nn0z 12029 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ0𝑖 ∈ ℤ)
81 1exp 13493 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℤ → (1↑𝑖) = 1)
8280, 81syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ0 → (1↑𝑖) = 1)
8379, 82sylan9eq 2814 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (𝑥𝑖) = 1)
8478, 83oveq12d 7161 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
8584sumeq2dv 15093 . . . . . . . . . . . . 13 (𝑥 = 1 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
86 sumex 15077 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ V
8785, 73, 86fvmpt 6752 . . . . . . . . . . . 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 12017 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 0 ∈ ℤ)
9036adantl 486 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9161, 11subcld 11020 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
9291ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
931ffvelrnda 6835 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9493adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9592, 94ifcld 4459 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ ℂ)
9695mulid1d 10681 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9790, 96eqtr4d 2797 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
9896, 95eqeltrd 2851 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ ℂ)
99 oveq1 7150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 1 → (𝑥𝑛) = (1↑𝑛))
100 nn0z 12029 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
101 1exp 13493 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
10399, 102sylan9eq 2814 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → (𝑥𝑛) = 1)
104103oveq2d 7159 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑛) · 1))
105104sumeq2dv 15093 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1))
106 fveq2 6651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → (𝐴𝑛) = (𝐴𝑚))
107106oveq1d 7158 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → ((𝐴𝑛) · 1) = ((𝐴𝑚) · 1))
108107cbvsumv 15086 . . . . . . . . . . . . . . . . . . . 20 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1)
109105, 108eqtrdi 2810 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
110 abelth.6 . . . . . . . . . . . . . . . . . . 19 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
111 sumex 15077 . . . . . . . . . . . . . . . . . . 19 Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) ∈ V
112109, 110, 111fvmpt 6752 . . . . . . . . . . . . . . . . . 18 (1 ∈ 𝑆 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
11376, 112syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
1149mulid1d 10681 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ0) → ((𝐴𝑚) · 1) = (𝐴𝑚))
115114sumeq2dv 15093 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
116113, 115eqtrd 2794 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
117116oveq1d 7158 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
11811subidd 11008 . . . . . . . . . . . . . . 15 (𝜑 → (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
119117, 118eqtrd 2794 . . . . . . . . . . . . . 14 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
12065, 119breqtrrd 5053 . . . . . . . . . . . . 13 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
121120adantr 485 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
1226, 89, 97, 98, 121isumclim 15145 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
12388, 122eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
124 oveq1 7150 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
12536, 124oveqan12rd 7163 . . . . . . . . . . . . . 14 ((𝑥 = 𝑦𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
126125sumeq2dv 15093 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
127 sumex 15077 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
128126, 73, 127fvmpt 6752 . . . . . . . . . . . 12 (𝑦𝑆 → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
129128adantl 486 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
130 oveq2 7151 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → (𝑦𝑘) = (𝑦𝑖))
13131, 130oveq12d 7161 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
132 eqid 2759 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))
133 ovex 7176 . . . . . . . . . . . . . 14 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
134131, 132, 133fvmpt 6752 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
135134adantl 486 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
13672ssrab3 3982 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ℂ
137136a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑆 ⊆ ℂ)
138137sselda 3888 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
139 expcl 13482 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
140138, 139sylan 584 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
14195, 140mulcld 10684 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ ℂ)
1422a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 0 ∈ ℕ0)
14315adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
144 expcl 13482 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
145138, 144sylan 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
146143, 145mulcld 10684 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) ∈ ℂ)
147146fmpttd 6863 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))):ℕ0⟶ℂ)
148147ffvelrnda 6835 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
14941oveq1d 7158 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
15028, 134syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
15130, 130oveq12d 7161 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴𝑖) · (𝑦𝑖)))
152 eqid 2759 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))
153 ovex 7176 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
154151, 152, 153fvmpt 6752 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
15528, 154syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
156149, 150, 1553eqtr4d 2804 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15726, 156sylan2br 598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15822, 157seqfeq 13430 . . . . . . . . . . . . . . . 16 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) = seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))))
159158adantr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) = seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))))
16014adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
161160, 145mulcld 10684 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑦𝑘)) ∈ ℂ)
162161fmpttd 6863 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))):ℕ0⟶ℂ)
163162ffvelrnda 6835 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
164154adantl 486 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
16594, 140mulcld 10684 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
1661, 10, 70, 71, 72abelthlem3 25112 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ∈ dom ⇝ )
1676, 89, 164, 165, 166isumclim2 15146 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
168 fveq2 6651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
169 oveq2 7151 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
170168, 169oveq12d 7161 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
171170cbvsumv 15086 . . . . . . . . . . . . . . . . . . . . 21 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖))
172124oveq2d 7159 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
173172sumeq2sdv 15094 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
174171, 173syl5eq 2806 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
175 sumex 15077 . . . . . . . . . . . . . . . . . . . 20 Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
176174, 110, 175fvmpt 6752 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑆 → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
177176adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
178167, 177breqtrrd 5053 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ (𝐹𝑦))
1796, 142, 163, 178clim2ser 15044 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)))
180 seq1 13416 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0))
18147, 180ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0)
182 fveq2 6651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
183 oveq2 7151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝑦𝑘) = (𝑦↑0))
184182, 183oveq12d 7161 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴‘0) · (𝑦↑0)))
185 ovex 7176 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴‘0) · (𝑦↑0)) ∈ V
186184, 152, 185fvmpt 6752 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0)))
1872, 186ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0))
188181, 187eqtri 2782 . . . . . . . . . . . . . . . . . 18 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝐴‘0) · (𝑦↑0))
189138exp0d 13539 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝑦↑0) = 1)
190189oveq2d 7159 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = ((𝐴‘0) · 1))
19161adantr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝐴‘0) ∈ ℂ)
192191mulid1d 10681 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · 1) = (𝐴‘0))
193190, 192eqtrd 2794 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = (𝐴‘0))
194188, 193syl5eq 2806 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = (𝐴‘0))
195194oveq2d 7159 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − (𝐴‘0)))
196179, 195breqtrd 5051 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
197159, 196eqbrtrd 5047 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
1986, 142, 148, 197clim2ser2 15045 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)))
199 seq1 13416 . . . . . . . . . . . . . . . . . 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 7161 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)))
202 ovex 7176 . . . . . . . . . . . . . . . . . . 19 (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) ∈ V
203201, 132, 202fvmpt 6752 . . . . . . . . . . . . . . . . . 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 2782 . . . . . . . . . . . . . . . 16 (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0))
206189oveq2d 7159 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1))
20711adantr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
208191, 207subcld 11020 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
209208mulid1d 10681 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
210206, 209eqtrd 2794 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
211205, 210syl5eq 2806 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
212211oveq2d 7159 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
2131, 10, 70, 71, 72, 110abelthlem4 25113 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑆⟶ℂ)
214213ffvelrnda 6835 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝐹𝑦) ∈ ℂ)
215214, 191, 207npncand 11044 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
216212, 215eqtrd 2794 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
217198, 216breqtrd 5051 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
2186, 89, 135, 141, 217isumclim 15145 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
219129, 218eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
220123, 219oveq12d 7161 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
221213adantr 485 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝐹:𝑆⟶ℂ)
222221, 77ffvelrnd 6836 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝐹‘1) ∈ ℂ)
223222, 214, 207nnncan2d 11055 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹‘1) − (𝐹𝑦)))
224220, 223eqtrd 2794 . . . . . . . 8 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = ((𝐹‘1) − (𝐹𝑦)))
225224fveq2d 6655 . . . . . . 7 ((𝜑𝑦𝑆) → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) = (abs‘((𝐹‘1) − (𝐹𝑦))))
226225breq1d 5035 . . . . . 6 ((𝜑𝑦𝑆) → ((abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅 ↔ (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅))
227226imbi2d 345 . . . . 5 ((𝜑𝑦𝑆) → (((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
228227ralbidva 3123 . . . 4 (𝜑 → (∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
229228rexbidv 3219 . . 3 (𝜑 → (∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
230229adantr 485 . 2 ((𝜑𝑅 ∈ ℝ+) → (∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
23174, 230mpbid 235 1 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∀wral 3068  ∃wrex 3069  {crab 3072   ∖ cdif 3851   ⊆ wss 3854  ifcif 4413  {csn 4515   class class class wbr 5025   ↦ cmpt 5105  dom cdm 5517   ∘ ccom 5521  ⟶wf 6324  ‘cfv 6328  (class class class)co 7143  ℂcc 10558  ℝcr 10559  0cc0 10560  1c1 10561   + caddc 10563   · cmul 10565   < clt 10698   ≤ cle 10699   − cmin 10893  ℕcn 11659  ℕ0cn0 11919  ℤcz 12005  ℤ≥cuz 12267  ℝ+crp 12415  seqcseq 13403  ↑cexp 13464  abscabs 14626   ⇝ cli 14874  Σcsu 15075  ballcbl 20138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-inf2 9122  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-pre-sup 10638  ax-addf 10639  ax-mulf 10640 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-om 7573  df-1st 7686  df-2nd 7687  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-sup 8924  df-inf 8925  df-oi 8992  df-card 9386  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-div 11321  df-nn 11660  df-2 11722  df-3 11723  df-n0 11920  df-z 12006  df-uz 12268  df-rp 12416  df-xadd 12534  df-ico 12770  df-icc 12771  df-fz 12925  df-fzo 13068  df-fl 13196  df-seq 13404  df-exp 13465  df-hash 13726  df-shft 14459  df-cj 14491  df-re 14492  df-im 14493  df-sqrt 14627  df-abs 14628  df-limsup 14861  df-clim 14878  df-rlim 14879  df-sum 15076  df-psmet 20143  df-xmet 20144  df-met 20145  df-bl 20146 This theorem is referenced by:  abelth  25120
 Copyright terms: Public domain W3C validator