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		ffvelcdm	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
10	1 8 9	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
11		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
12		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
13		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑚 ) )
14	1	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
15	11 12 13 14 2	isumcl	⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ0 ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑚 ∈ ℕ0 ( 𝐴 ‘ 𝑚 ) ∈ ℂ )
17	10 16	subcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴 ‘ 𝑚 ) ) ∈ ℂ )
18	1	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
95	94	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
96	93 95	ifcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → if ( 𝑖 = 0 , ( ( 𝐴 ‘ 0 ) − Σ 𝑚 ∈ ℕ0 ( 𝐴 ‘ 𝑚 ) ) , ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
97	96	mulridd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ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	mulridd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ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	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ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	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ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	mulridd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐴 ‘ 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	mulridd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝐴 ‘ 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 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 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑅 ) )