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

Theorem abelthlem9 25943
Description: Lemma for abelth 25944. 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 12483 . . . . . . . 8 0 ∈ ℕ0
32a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0 → 0 ∈ ℕ0)
4 ffvelcdm 7080 . . . . . . 7 ((𝐴:ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
51, 3, 4syl2an 596 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐴‘0) ∈ ℂ)
6 nn0uz 12860 . . . . . . . 8 0 = (ℤ‘0)
7 0zd 12566 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
8 eqidd 2733 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) = (𝐴𝑚))
91ffvelcdmda 7083 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝐴𝑚) ∈ ℂ)
10 abelth.2 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
116, 7, 8, 9, 10isumcl 15703 . . . . . . 7 (𝜑 → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
1211adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
135, 12subcld 11567 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
141ffvelcdmda 7083 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
1513, 14ifcld 4573 . . . 4 ((𝜑𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
1615fmpttd 7111 . . 3 (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))):ℕ0⟶ℂ)
172a1i 11 . . . . . 6 (𝜑 → 0 ∈ ℕ0)
1816ffvelcdmda 7083 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) ∈ ℂ)
19 1e0p1 12715 . . . . . . . . . 10 1 = (0 + 1)
20 1z 12588 . . . . . . . . . 10 1 ∈ ℤ
2119, 20eqeltrri 2830 . . . . . . . . 9 (0 + 1) ∈ ℤ
2221a1i 11 . . . . . . . 8 (𝜑 → (0 + 1) ∈ ℤ)
23 nnuz 12861 . . . . . . . . . . 11 ℕ = (ℤ‘1)
2419fveq2i 6891 . . . . . . . . . . 11 (ℤ‘1) = (ℤ‘(0 + 1))
2523, 24eqtri 2760 . . . . . . . . . 10 ℕ = (ℤ‘(0 + 1))
2625eleq2i 2825 . . . . . . . . 9 (𝑖 ∈ ℕ ↔ 𝑖 ∈ (ℤ‘(0 + 1)))
27 nnnn0 12475 . . . . . . . . . . . 12 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
2827adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0)
29 eqeq1 2736 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘 = 0 ↔ 𝑖 = 0))
30 fveq2 6888 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝐴𝑘) = (𝐴𝑖))
3129, 30ifbieq2d 4553 . . . . . . . . . . . 12 (𝑘 = 𝑖 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
32 eqid 2732 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))
33 ovex 7438 . . . . . . . . . . . . 13 ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ V
34 fvex 6901 . . . . . . . . . . . . 13 (𝐴𝑖) ∈ V
3533, 34ifex 4577 . . . . . . . . . . . 12 if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ V
3631, 32, 35fvmpt 6995 . . . . . . . . . . 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 12242 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → 𝑖 ≠ 0)
3938adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ) → 𝑖 ≠ 0)
4039neneqd 2945 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ) → ¬ 𝑖 = 0)
4140iffalsed 4538 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) = (𝐴𝑖))
4237, 41eqtrd 2772 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4326, 42sylan2br 595 . . . . . . . 8 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (𝐴𝑖))
4422, 43seqfeq 13989 . . . . . . 7 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) = seq(0 + 1)( + , 𝐴))
456, 7, 8, 9, 10isumclim2 15700 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴) ⇝ Σ𝑚 ∈ ℕ0 (𝐴𝑚))
466, 17, 14, 45clim2ser 15597 . . . . . . . 8 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)))
47 0z 12565 . . . . . . . . . 10 0 ∈ ℤ
48 seq1 13975 . . . . . . . . . 10 (0 ∈ ℤ → (seq0( + , 𝐴)‘0) = (𝐴‘0))
4947, 48ax-mp 5 . . . . . . . . 9 (seq0( + , 𝐴)‘0) = (𝐴‘0)
5049oveq2i 7416 . . . . . . . 8 𝑚 ∈ ℕ0 (𝐴𝑚) − (seq0( + , 𝐴)‘0)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0))
5146, 50breqtrdi 5188 . . . . . . 7 (𝜑 → seq(0 + 1)( + , 𝐴) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
5244, 51eqbrtrd 5169 . . . . . 6 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)))
536, 17, 18, 52clim2ser2 15598 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)))
54 seq1 13975 . . . . . . . . 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 4533 . . . . . . . . . 10 (𝑘 = 0 → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
5756, 32, 33fvmpt 6995 . . . . . . . . 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 2760 . . . . . . 7 (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))
6059oveq2i 7416 . . . . . 6 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
611, 2, 4sylancl 586 . . . . . . 7 (𝜑 → (𝐴‘0) ∈ ℂ)
62 npncan2 11483 . . . . . . 7 ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ ∧ (𝐴‘0) ∈ ℂ) → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6311, 61, 62syl2anc 584 . . . . . 6 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = 0)
6460, 63eqtrid 2784 . . . . 5 (𝜑 → ((Σ𝑚 ∈ ℕ0 (𝐴𝑚) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘))))‘0)) = 0)
6553, 64breqtrd 5173 . . . 4 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ⇝ 0)
66 seqex 13964 . . . . 5 seq0( + , (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))) ∈ V
67 c0ex 11204 . . . . 5 0 ∈ V
6866, 67breldm 5906 . . . 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 2732 . . 3 (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖))) = (𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))
7416, 69, 70, 71, 72, 73, 65abelthlem8 25942 . 2 ((𝜑𝑅 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅))
751, 10, 70, 71, 72abelthlem2 25935 . . . . . . . . . . . . . 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 7412 . . . . . . . . . . . . . . . 16 (𝑥 = 1 → (𝑥𝑖) = (1↑𝑖))
80 nn0z 12579 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ0𝑖 ∈ ℤ)
81 1exp 14053 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℤ → (1↑𝑖) = 1)
8280, 81syl 17 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℕ0 → (1↑𝑖) = 1)
8379, 82sylan9eq 2792 . . . . . . . . . . . . . . 15 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (𝑥𝑖) = 1)
8478, 83oveq12d 7423 . . . . . . . . . . . . . 14 ((𝑥 = 1 ∧ 𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
8584sumeq2dv 15645 . . . . . . . . . . . . 13 (𝑥 = 1 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
86 sumex 15630 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ V
8785, 73, 86fvmpt 6995 . . . . . . . . . . . 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 12566 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 0 ∈ ℤ)
9036adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9161, 11subcld 11567 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
9291ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
931ffvelcdmda 7083 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9493adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐴𝑖) ∈ ℂ)
9592, 94ifcld 4573 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) ∈ ℂ)
9695mulridd 11227 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)))
9790, 96eqtr4d 2775 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1))
9896, 95eqeltrd 2833 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) ∈ ℂ)
99 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 1 → (𝑥𝑛) = (1↑𝑛))
100 nn0z 12579 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
101 1exp 14053 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
10399, 102sylan9eq 2792 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → (𝑥𝑛) = 1)
104103oveq2d 7421 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑛) · 1))
105104sumeq2dv 15645 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1))
106 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → (𝐴𝑛) = (𝐴𝑚))
107106oveq1d 7420 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → ((𝐴𝑛) · 1) = ((𝐴𝑚) · 1))
108107cbvsumv 15638 . . . . . . . . . . . . . . . . . . . 20 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · 1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1)
109105, 108eqtrdi 2788 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 1 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
110 abelth.6 . . . . . . . . . . . . . . . . . . 19 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
111 sumex 15630 . . . . . . . . . . . . . . . . . . 19 Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) ∈ V
112109, 110, 111fvmpt 6995 . . . . . . . . . . . . . . . . . 18 (1 ∈ 𝑆 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
11376, 112syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1))
1149mulridd 11227 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ0) → ((𝐴𝑚) · 1) = (𝐴𝑚))
115114sumeq2dv 15645 . . . . . . . . . . . . . . . . 17 (𝜑 → Σ𝑚 ∈ ℕ0 ((𝐴𝑚) · 1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
116113, 115eqtrd 2772 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹‘1) = Σ𝑚 ∈ ℕ0 (𝐴𝑚))
117116oveq1d 7420 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
11811subidd 11555 . . . . . . . . . . . . . . 15 (𝜑 → (Σ𝑚 ∈ ℕ0 (𝐴𝑚) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
119117, 118eqtrd 2772 . . . . . . . . . . . . . 14 (𝜑 → ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) = 0)
12065, 119breqtrrd 5175 . . . . . . . . . . . . 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 15699 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · 1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
12388, 122eqtrd 2772 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) = ((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
124 oveq1 7412 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥𝑖) = (𝑦𝑖))
12536, 124oveqan12rd 7425 . . . . . . . . . . . . . 14 ((𝑥 = 𝑦𝑖 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
126125sumeq2dv 15645 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
127 sumex 15630 . . . . . . . . . . . . 13 Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
128126, 73, 127fvmpt 6995 . . . . . . . . . . . 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 7413 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → (𝑦𝑘) = (𝑦𝑖))
13131, 130oveq12d 7423 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
132 eqid 2732 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))
133 ovex 7438 . . . . . . . . . . . . . 14 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ V
134131, 132, 133fvmpt 6995 . . . . . . . . . . . . 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 4079 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ℂ
137136a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝑆 ⊆ ℂ)
138137sselda 3981 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
139 expcl 14041 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
140138, 139sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑖) ∈ ℂ)
14195, 140mulcld 11230 . . . . . . . . . . . 12 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) ∈ ℂ)
1422a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → 0 ∈ ℕ0)
14315adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) ∈ ℂ)
144 expcl 14041 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
145138, 144sylan 580 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦𝑘) ∈ ℂ)
146143, 145mulcld 11230 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) ∈ ℂ)
147146fmpttd 7111 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))):ℕ0⟶ℂ)
148147ffvelcdmda 7083 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
14941oveq1d 7420 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
15028, 134syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)))
15130, 130oveq12d 7423 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴𝑖) · (𝑦𝑖)))
152 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))
153 ovex 7438 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
154151, 152, 153fvmpt 6995 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
15528, 154syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
156149, 150, 1553eqtr4d 2782 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15726, 156sylan2br 595 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ‘(0 + 1))) → ((𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))‘𝑖) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖))
15822, 157seqfeq 13989 . . . . . . . . . . . . . . . 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 11230 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) · (𝑦𝑘)) ∈ ℂ)
162161fmpttd 7111 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))):ℕ0⟶ℂ)
163162ffvelcdmda 7083 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) ∈ ℂ)
164154adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘𝑖) = ((𝐴𝑖) · (𝑦𝑖)))
16594, 140mulcld 11230 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐴𝑖) · (𝑦𝑖)) ∈ ℂ)
1661, 10, 70, 71, 72abelthlem3 25936 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ∈ dom ⇝ )
1676, 89, 164, 165, 166isumclim2 15700 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
168 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝐴𝑛) = (𝐴𝑖))
169 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝑥𝑛) = (𝑥𝑖))
170168, 169oveq12d 7423 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑖 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑖) · (𝑥𝑖)))
171170cbvsumv 15638 . . . . . . . . . . . . . . . . . . . . 21 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖))
172124oveq2d 7421 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → ((𝐴𝑖) · (𝑥𝑖)) = ((𝐴𝑖) · (𝑦𝑖)))
173172sumeq2sdv 15646 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑥𝑖)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
174171, 173eqtrid 2784 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
175 sumex 15630 . . . . . . . . . . . . . . . . . . . 20 Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)) ∈ V
176174, 110, 175fvmpt 6995 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑆 → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
177176adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → (𝐹𝑦) = Σ𝑖 ∈ ℕ0 ((𝐴𝑖) · (𝑦𝑖)))
178167, 177breqtrrd 5175 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ (𝐹𝑦))
1796, 142, 163, 178clim2ser 15597 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)))
180 seq1 13975 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0))
18147, 180ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0)
182 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝐴𝑘) = (𝐴‘0))
183 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 0 → (𝑦𝑘) = (𝑦↑0))
184182, 183oveq12d 7423 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((𝐴𝑘) · (𝑦𝑘)) = ((𝐴‘0) · (𝑦↑0)))
185 ovex 7438 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴‘0) · (𝑦↑0)) ∈ V
186184, 152, 185fvmpt 6995 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0)))
1872, 186ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))‘0) = ((𝐴‘0) · (𝑦↑0))
188181, 187eqtri 2760 . . . . . . . . . . . . . . . . . 18 (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = ((𝐴‘0) · (𝑦↑0))
189138exp0d 14101 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝑦↑0) = 1)
190189oveq2d 7421 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = ((𝐴‘0) · 1))
19161adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦𝑆) → (𝐴‘0) ∈ ℂ)
192191mulridd 11227 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → ((𝐴‘0) · 1) = (𝐴‘0))
193190, 192eqtrd 2772 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) · (𝑦↑0)) = (𝐴‘0))
194188, 193eqtrid 2784 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0) = (𝐴‘0))
195194oveq2d 7421 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → ((𝐹𝑦) − (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − (𝐴‘0)))
196179, 195breqtrd 5173 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
197159, 196eqbrtrd 5169 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − (𝐴‘0)))
1986, 142, 148, 197clim2ser2 15598 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)))
199 seq1 13975 . . . . . . . . . . . . . . . . . 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 7423 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)))
202 ovex 7438 . . . . . . . . . . . . . . . . . . 19 (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) ∈ V
203201, 132, 202fvmpt 6995 . . . . . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . . . . . 16 (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0))
206189oveq2d 7421 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1))
20711adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑆) → Σ𝑚 ∈ ℕ0 (𝐴𝑚) ∈ ℂ)
208191, 207subcld 11567 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑆) → ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) ∈ ℂ)
209208mulridd 11227 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · 1) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
210206, 209eqtrd 2772 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑆) → (((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) · (𝑦↑0)) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
211205, 210eqtrid 2784 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0) = ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
212211oveq2d 7421 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
2131, 10, 70, 71, 72, 110abelthlem4 25937 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑆⟶ℂ)
214213ffvelcdmda 7083 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑆) → (𝐹𝑦) ∈ ℂ)
215214, 191, 207npncand 11591 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
216212, 215eqtrd 2772 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → (((𝐹𝑦) − (𝐴‘0)) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘))))‘0)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
217198, 216breqtrd 5173 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → seq0( + , (𝑘 ∈ ℕ0 ↦ (if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)) · (𝑦𝑘)))) ⇝ ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
2186, 89, 135, 141, 217isumclim 15699 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → Σ𝑖 ∈ ℕ0 (if(𝑖 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑖)) · (𝑦𝑖)) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
219129, 218eqtrd 2772 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦) = ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)))
220123, 219oveq12d 7423 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))))
221213adantr 481 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝐹:𝑆⟶ℂ)
222221, 77ffvelcdmd 7084 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝐹‘1) ∈ ℂ)
223222, 214, 207nnncan2d 11602 . . . . . . . . 9 ((𝜑𝑦𝑆) → (((𝐹‘1) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)) − ((𝐹𝑦) − Σ𝑚 ∈ ℕ0 (𝐴𝑚))) = ((𝐹‘1) − (𝐹𝑦)))
224220, 223eqtrd 2772 . . . . . . . 8 ((𝜑𝑦𝑆) → (((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦)) = ((𝐹‘1) − (𝐹𝑦)))
225224fveq2d 6892 . . . . . . 7 ((𝜑𝑦𝑆) → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) = (abs‘((𝐹‘1) − (𝐹𝑦))))
226225breq1d 5157 . . . . . 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 3175 . . . 4 (𝜑 → (∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘(((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘1) − ((𝑥𝑆 ↦ Σ𝑖 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if(𝑘 = 0, ((𝐴‘0) − Σ𝑚 ∈ ℕ0 (𝐴𝑚)), (𝐴𝑘)))‘𝑖) · (𝑥𝑖)))‘𝑦))) < 𝑅) ↔ ∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑅)))
229228rexbidv 3178 . . 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 2940  wral 3061  wrex 3070  {crab 3432  cdif 3944  wss 3947  ifcif 4527  {csn 4627   class class class wbr 5147  cmpt 5230  dom cdm 5675  ccom 5679  wf 6536  cfv 6540  (class class class)co 7405  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244  cle 11245  cmin 11440  cn 12208  0cn0 12468  cz 12554  cuz 12818  +crp 12970  seqcseq 13962  cexp 14023  abscabs 15177  cli 15424  Σcsu 15628  ballcbl 20923
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 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-xadd 13089  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931
This theorem is referenced by:  abelth  25944
  Copyright terms: Public domain W3C validator