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 eqtrid ⊢ ( 𝜑 → ( ( Σ 𝑚 ∈ ℕ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 eqtrid ⊢ ( 𝑥 = 𝑦 → Σ 𝑛 ∈ ℕ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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 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 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )