Metamath Proof Explorer


Theorem abelthlem9

Description: Lemma for abelth . By adjusting the constant term, we can assume that the entire series converges to 0 . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Hypotheses abelth.1 ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ( 𝜑𝑀 ∈ ℝ )
abelth.4 ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 𝐹 = ( 𝑥𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) )
Assertion abelthlem9 ( ( 𝜑𝑅 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ( 𝜑𝑀 ∈ ℝ )
4 abelth.4 ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 𝐹 = ( 𝑥𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) )
7 0nn0 0 ∈ ℕ0
8 7 a1i ( 𝑘 ∈ ℕ0 → 0 ∈ ℕ0 )
9 ffvelrn ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
10 1 8 9 syl2an ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
11 nn0uz 0 = ( ℤ ‘ 0 )
12 0zd ( 𝜑 → 0 ∈ ℤ )
13 eqidd ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝐴𝑚 ) = ( 𝐴𝑚 ) )
14 1 ffvelrnda ( ( 𝜑𝑚 ∈ ℕ0 ) → ( 𝐴𝑚 ) ∈ ℂ )
15 11 12 13 14 2 isumcl ( 𝜑 → Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ∈ ℂ )
16 15 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ∈ ℂ )
17 10 16 subcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ∈ ℂ )
18 1 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
19 17 18 ifcld ( ( 𝜑𝑘 ∈ ℕ0 ) → if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ∈ ℂ )
20 19 fmpttd ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) : ℕ0 ⟶ ℂ )
21 7 a1i ( 𝜑 → 0 ∈ ℕ0 )
22 20 ffvelrnda ( ( 𝜑𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
23 1e0p1 1 = ( 0 + 1 )
24 1z 1 ∈ ℤ
25 23 24 eqeltrri ( 0 + 1 ) ∈ ℤ
26 25 a1i ( 𝜑 → ( 0 + 1 ) ∈ ℤ )
27 nnuz ℕ = ( ℤ ‘ 1 )
28 23 fveq2i ( ℤ ‘ 1 ) = ( ℤ ‘ ( 0 + 1 ) )
29 27 28 eqtri ℕ = ( ℤ ‘ ( 0 + 1 ) )
30 29 eleq2i ( 𝑖 ∈ ℕ ↔ 𝑖 ∈ ( ℤ ‘ ( 0 + 1 ) ) )
31 nnnn0 ( 𝑖 ∈ ℕ → 𝑖 ∈ ℕ0 )
32 31 adantl ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ0 )
33 eqeq1 ( 𝑘 = 𝑖 → ( 𝑘 = 0 ↔ 𝑖 = 0 ) )
34 fveq2 ( 𝑘 = 𝑖 → ( 𝐴𝑘 ) = ( 𝐴𝑖 ) )
35 33 34 ifbieq2d ( 𝑘 = 𝑖 → if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
36 eqid ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) )
37 ovex ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ∈ V
38 fvex ( 𝐴𝑖 ) ∈ V
39 37 38 ifex if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) ∈ V
40 35 36 39 fvmpt ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
41 32 40 syl ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
42 nnne0 ( 𝑖 ∈ ℕ → 𝑖 ≠ 0 )
43 42 adantl ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ≠ 0 )
44 43 neneqd ( ( 𝜑𝑖 ∈ ℕ ) → ¬ 𝑖 = 0 )
45 44 iffalsed ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) = ( 𝐴𝑖 ) )
46 41 45 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = ( 𝐴𝑖 ) )
47 30 46 sylan2br ( ( 𝜑𝑖 ∈ ( ℤ ‘ ( 0 + 1 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = ( 𝐴𝑖 ) )
48 26 47 seqfeq ( 𝜑 → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) = seq ( 0 + 1 ) ( + , 𝐴 ) )
49 11 12 13 14 2 isumclim2 ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) )
50 11 21 18 49 clim2ser ( 𝜑 → seq ( 0 + 1 ) ( + , 𝐴 ) ⇝ ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( seq 0 ( + , 𝐴 ) ‘ 0 ) ) )
51 0z 0 ∈ ℤ
52 seq1 ( 0 ∈ ℤ → ( seq 0 ( + , 𝐴 ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
53 51 52 ax-mp ( seq 0 ( + , 𝐴 ) ‘ 0 ) = ( 𝐴 ‘ 0 )
54 53 oveq2i ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( seq 0 ( + , 𝐴 ) ‘ 0 ) ) = ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) )
55 50 54 breqtrdi ( 𝜑 → seq ( 0 + 1 ) ( + , 𝐴 ) ⇝ ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) )
56 48 55 eqbrtrd ( 𝜑 → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) )
57 11 21 22 56 clim2ser2 ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) ) )
58 seq1 ( 0 ∈ ℤ → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 0 ) )
59 51 58 ax-mp ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 0 )
60 iftrue ( 𝑘 = 0 → if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
61 60 36 37 fvmpt ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
62 7 61 ax-mp ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) )
63 59 62 eqtri ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) )
64 63 oveq2i ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) ) = ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
65 1 7 9 sylancl ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ℂ )
66 npncan2 ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ∈ ℂ ∧ ( 𝐴 ‘ 0 ) ∈ ℂ ) → ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) = 0 )
67 15 65 66 syl2anc ( 𝜑 → ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) = 0 )
68 64 67 syl5eq ( 𝜑 → ( ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ‘ 0 ) ) = 0 )
69 57 68 breqtrd ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ 0 )
70 seqex seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ∈ V
71 c0ex 0 ∈ V
72 70 71 breldm ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ 0 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ∈ dom ⇝ )
73 69 72 syl ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ∈ dom ⇝ )
74 eqid ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) = ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) )
75 20 73 3 4 5 74 69 abelthlem8 ( ( 𝜑𝑅 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ) )
76 1 2 3 4 5 abelthlem2 ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
77 76 simpld ( 𝜑 → 1 ∈ 𝑆 )
78 77 adantr ( ( 𝜑𝑦𝑆 ) → 1 ∈ 𝑆 )
79 40 adantl ( ( 𝑥 = 1 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
80 oveq1 ( 𝑥 = 1 → ( 𝑥𝑖 ) = ( 1 ↑ 𝑖 ) )
81 nn0z ( 𝑖 ∈ ℕ0𝑖 ∈ ℤ )
82 1exp ( 𝑖 ∈ ℤ → ( 1 ↑ 𝑖 ) = 1 )
83 81 82 syl ( 𝑖 ∈ ℕ0 → ( 1 ↑ 𝑖 ) = 1 )
84 80 83 sylan9eq ( ( 𝑥 = 1 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑥𝑖 ) = 1 )
85 79 84 oveq12d ( ( 𝑥 = 1 ∧ 𝑖 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) )
86 85 sumeq2dv ( 𝑥 = 1 → Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) )
87 sumex Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) ∈ V
88 86 74 87 fvmpt ( 1 ∈ 𝑆 → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) )
89 78 88 syl ( ( 𝜑𝑦𝑆 ) → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) )
90 0zd ( ( 𝜑𝑦𝑆 ) → 0 ∈ ℤ )
91 40 adantl ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
92 65 15 subcld ( 𝜑 → ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ∈ ℂ )
93 92 ad2antrr ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ∈ ℂ )
94 1 ffvelrnda ( ( 𝜑𝑖 ∈ ℕ0 ) → ( 𝐴𝑖 ) ∈ ℂ )
95 94 adantlr ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐴𝑖 ) ∈ ℂ )
96 93 95 ifcld ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) ∈ ℂ )
97 96 mulid1d ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) = if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) )
98 91 97 eqtr4d ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) )
99 97 96 eqeltrd ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) ∈ ℂ )
100 oveq1 ( 𝑥 = 1 → ( 𝑥𝑛 ) = ( 1 ↑ 𝑛 ) )
101 nn0z ( 𝑛 ∈ ℕ0𝑛 ∈ ℤ )
102 1exp ( 𝑛 ∈ ℤ → ( 1 ↑ 𝑛 ) = 1 )
103 101 102 syl ( 𝑛 ∈ ℕ0 → ( 1 ↑ 𝑛 ) = 1 )
104 100 103 sylan9eq ( ( 𝑥 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥𝑛 ) = 1 )
105 104 oveq2d ( ( 𝑥 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = ( ( 𝐴𝑛 ) · 1 ) )
106 105 sumeq2dv ( 𝑥 = 1 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · 1 ) )
107 fveq2 ( 𝑛 = 𝑚 → ( 𝐴𝑛 ) = ( 𝐴𝑚 ) )
108 107 oveq1d ( 𝑛 = 𝑚 → ( ( 𝐴𝑛 ) · 1 ) = ( ( 𝐴𝑚 ) · 1 ) )
109 108 cbvsumv Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · 1 ) = Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 )
110 106 109 eqtrdi ( 𝑥 = 1 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 ) )
111 sumex Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 ) ∈ V
112 110 6 111 fvmpt ( 1 ∈ 𝑆 → ( 𝐹 ‘ 1 ) = Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 ) )
113 77 112 syl ( 𝜑 → ( 𝐹 ‘ 1 ) = Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 ) )
114 14 mulid1d ( ( 𝜑𝑚 ∈ ℕ0 ) → ( ( 𝐴𝑚 ) · 1 ) = ( 𝐴𝑚 ) )
115 114 sumeq2dv ( 𝜑 → Σ 𝑚 ∈ ℕ0 ( ( 𝐴𝑚 ) · 1 ) = Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) )
116 113 115 eqtrd ( 𝜑 → ( 𝐹 ‘ 1 ) = Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) )
117 116 oveq1d ( 𝜑 → ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) = ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
118 15 subidd ( 𝜑 → ( Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) = 0 )
119 117 118 eqtrd ( 𝜑 → ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) = 0 )
120 69 119 breqtrrd ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
121 120 adantr ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ) ⇝ ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
122 11 90 98 99 121 isumclim ( ( 𝜑𝑦𝑆 ) → Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · 1 ) = ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
123 89 122 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) = ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
124 oveq1 ( 𝑥 = 𝑦 → ( 𝑥𝑖 ) = ( 𝑦𝑖 ) )
125 40 124 oveqan12rd ( ( 𝑥 = 𝑦𝑖 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
126 125 sumeq2dv ( 𝑥 = 𝑦 → Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
127 sumex Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) ∈ V
128 126 74 127 fvmpt ( 𝑦𝑆 → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
129 128 adantl ( ( 𝜑𝑦𝑆 ) → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) = Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
130 oveq2 ( 𝑘 = 𝑖 → ( 𝑦𝑘 ) = ( 𝑦𝑖 ) )
131 35 130 oveq12d ( 𝑘 = 𝑖 → ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
132 eqid ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) )
133 ovex ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) ∈ V
134 131 132 133 fvmpt ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
135 134 adantl ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
136 5 ssrab3 𝑆 ⊆ ℂ
137 136 a1i ( 𝜑𝑆 ⊆ ℂ )
138 137 sselda ( ( 𝜑𝑦𝑆 ) → 𝑦 ∈ ℂ )
139 expcl ( ( 𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦𝑖 ) ∈ ℂ )
140 138 139 sylan ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦𝑖 ) ∈ ℂ )
141 96 140 mulcld ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) ∈ ℂ )
142 7 a1i ( ( 𝜑𝑦𝑆 ) → 0 ∈ ℕ0 )
143 19 adantlr ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ∈ ℂ )
144 expcl ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦𝑘 ) ∈ ℂ )
145 138 144 sylan ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦𝑘 ) ∈ ℂ )
146 143 145 mulcld ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ∈ ℂ )
147 146 fmpttd ( ( 𝜑𝑦𝑆 ) → ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) : ℕ0 ⟶ ℂ )
148 147 ffvelrnda ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
149 45 oveq1d ( ( 𝜑𝑖 ∈ ℕ ) → ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
150 32 134 syl ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) )
151 34 130 oveq12d ( 𝑘 = 𝑖 → ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
152 eqid ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) )
153 ovex ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) ∈ V
154 151 152 153 fvmpt ( 𝑖 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
155 32 154 syl ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
156 149 150 155 3eqtr4d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) )
157 30 156 sylan2br ( ( 𝜑𝑖 ∈ ( ℤ ‘ ( 0 + 1 ) ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) )
158 26 157 seqfeq ( 𝜑 → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) = seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) )
159 158 adantr ( ( 𝜑𝑦𝑆 ) → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) = seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) )
160 18 adantlr ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
161 160 145 mulcld ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ∈ ℂ )
162 161 fmpttd ( ( 𝜑𝑦𝑆 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) : ℕ0 ⟶ ℂ )
163 162 ffvelrnda ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
164 154 adantl ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 𝑖 ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
165 95 140 mulcld ( ( ( 𝜑𝑦𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) ∈ ℂ )
166 1 2 3 4 5 abelthlem3 ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ∈ dom ⇝ )
167 11 90 164 165 166 isumclim2 ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ⇝ Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
168 fveq2 ( 𝑛 = 𝑖 → ( 𝐴𝑛 ) = ( 𝐴𝑖 ) )
169 oveq2 ( 𝑛 = 𝑖 → ( 𝑥𝑛 ) = ( 𝑥𝑖 ) )
170 168 169 oveq12d ( 𝑛 = 𝑖 → ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = ( ( 𝐴𝑖 ) · ( 𝑥𝑖 ) ) )
171 170 cbvsumv Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑥𝑖 ) )
172 124 oveq2d ( 𝑥 = 𝑦 → ( ( 𝐴𝑖 ) · ( 𝑥𝑖 ) ) = ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
173 172 sumeq2sdv ( 𝑥 = 𝑦 → Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑥𝑖 ) ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
174 171 173 syl5eq ( 𝑥 = 𝑦 → Σ 𝑛 ∈ ℕ0 ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
175 sumex Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) ∈ V
176 174 6 175 fvmpt ( 𝑦𝑆 → ( 𝐹𝑦 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
177 176 adantl ( ( 𝜑𝑦𝑆 ) → ( 𝐹𝑦 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐴𝑖 ) · ( 𝑦𝑖 ) ) )
178 167 177 breqtrrd ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( 𝐹𝑦 ) )
179 11 142 163 178 clim2ser ( ( 𝜑𝑦𝑆 ) → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( ( 𝐹𝑦 ) − ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) ) )
180 seq1 ( 0 ∈ ℤ → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) )
181 51 180 ax-mp ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 0 )
182 fveq2 ( 𝑘 = 0 → ( 𝐴𝑘 ) = ( 𝐴 ‘ 0 ) )
183 oveq2 ( 𝑘 = 0 → ( 𝑦𝑘 ) = ( 𝑦 ↑ 0 ) )
184 182 183 oveq12d ( 𝑘 = 0 → ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) ) )
185 ovex ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) ) ∈ V
186 184 152 185 fvmpt ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) ) )
187 7 186 ax-mp ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) )
188 181 187 eqtri ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) )
189 138 exp0d ( ( 𝜑𝑦𝑆 ) → ( 𝑦 ↑ 0 ) = 1 )
190 189 oveq2d ( ( 𝜑𝑦𝑆 ) → ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
191 65 adantr ( ( 𝜑𝑦𝑆 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
192 191 mulid1d ( ( 𝜑𝑦𝑆 ) → ( ( 𝐴 ‘ 0 ) · 1 ) = ( 𝐴 ‘ 0 ) )
193 190 192 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( 𝐴 ‘ 0 ) · ( 𝑦 ↑ 0 ) ) = ( 𝐴 ‘ 0 ) )
194 188 193 syl5eq ( ( 𝜑𝑦𝑆 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( 𝐴 ‘ 0 ) )
195 194 oveq2d ( ( 𝜑𝑦𝑆 ) → ( ( 𝐹𝑦 ) − ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) ) = ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) )
196 179 195 breqtrd ( ( 𝜑𝑦𝑆 ) → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴𝑘 ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) )
197 159 196 eqbrtrd ( ( 𝜑𝑦𝑆 ) → seq ( 0 + 1 ) ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) )
198 11 142 148 197 clim2ser2 ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) ) )
199 seq1 ( 0 ∈ ℤ → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) )
200 51 199 ax-mp ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 0 )
201 60 183 oveq12d ( 𝑘 = 0 → ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) = ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) ) )
202 ovex ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) ) ∈ V
203 201 132 202 fvmpt ( 0 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) = ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) ) )
204 7 203 ax-mp ( ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ‘ 0 ) = ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) )
205 200 204 eqtri ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) )
206 189 oveq2d ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) ) = ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · 1 ) )
207 15 adantr ( ( 𝜑𝑦𝑆 ) → Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ∈ ℂ )
208 191 207 subcld ( ( 𝜑𝑦𝑆 ) → ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ∈ ℂ )
209 208 mulid1d ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · 1 ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
210 206 209 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) · ( 𝑦 ↑ 0 ) ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
211 205 210 syl5eq ( ( 𝜑𝑦𝑆 ) → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) = ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
212 211 oveq2d ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) ) = ( ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) + ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) )
213 1 2 3 4 5 6 abelthlem4 ( 𝜑𝐹 : 𝑆 ⟶ ℂ )
214 213 ffvelrnda ( ( 𝜑𝑦𝑆 ) → ( 𝐹𝑦 ) ∈ ℂ )
215 214 191 207 npncand ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) + ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) = ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
216 212 215 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐹𝑦 ) − ( 𝐴 ‘ 0 ) ) + ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ‘ 0 ) ) = ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
217 198 216 breqtrd ( ( 𝜑𝑦𝑆 ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) · ( 𝑦𝑘 ) ) ) ) ⇝ ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
218 11 90 135 141 217 isumclim ( ( 𝜑𝑦𝑆 ) → Σ 𝑖 ∈ ℕ0 ( if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑖 ) ) · ( 𝑦𝑖 ) ) = ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
219 129 218 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) = ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) )
220 123 219 oveq12d ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) = ( ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) − ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) )
221 213 adantr ( ( 𝜑𝑦𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
222 221 78 ffvelrnd ( ( 𝜑𝑦𝑆 ) → ( 𝐹 ‘ 1 ) ∈ ℂ )
223 222 214 207 nnncan2d ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝐹 ‘ 1 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) − ( ( 𝐹𝑦 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) ) = ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) )
224 220 223 eqtrd ( ( 𝜑𝑦𝑆 ) → ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) )
225 224 fveq2d ( ( 𝜑𝑦𝑆 ) → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) )
226 225 breq1d ( ( 𝜑𝑦𝑆 ) → ( ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ↔ ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) )
227 226 imbi2d ( ( 𝜑𝑦𝑆 ) → ( ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ) ↔ ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) ) )
228 227 ralbidva ( 𝜑 → ( ∀ 𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ) ↔ ∀ 𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) ) )
229 228 rexbidv ( 𝜑 → ( ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ) ↔ ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) ) )
230 229 adantr ( ( 𝜑𝑅 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 1 ) − ( ( 𝑥𝑆 ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴𝑚 ) ) , ( 𝐴𝑘 ) ) ) ‘ 𝑖 ) · ( 𝑥𝑖 ) ) ) ‘ 𝑦 ) ) ) < 𝑅 ) ↔ ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) ) )
231 75 230 mpbid ( ( 𝜑𝑅 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+𝑦𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹𝑦 ) ) ) < 𝑅 ) )