Theorem abelthlem4

Description: Lemma for abelth . (Contributed by Mario Carneiro, 31-Mar-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	abelthlem4	⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )

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		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8		0zd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 0 ∈ ℤ )
9		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐴 ‘ 𝑚 ) = ( 𝐴 ‘ 𝑛 ) )
10		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝑥 ↑ 𝑚 ) = ( 𝑥 ↑ 𝑛 ) )
11	9 10	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
12		eqid	⊢ ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) )
13		ovex	⊢ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ∈ V
14	11 12 13	fvmpt	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ‘ 𝑛 ) = ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
17	16	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
18	5	ssrab3	⊢ 𝑆 ⊆ ℂ
19	18	a1i	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
20	19	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℂ )
21		expcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑛 ) ∈ ℂ )
22	20 21	sylan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑛 ) ∈ ℂ )
23	17 22	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ∈ ℂ )
24	1 2 3 4 5	abelthlem3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑚 ) · ( 𝑥 ↑ 𝑚 ) ) ) ) ∈ dom ⇝ )
25	7 8 15 23 24	isumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ∈ ℂ )
26	25 6	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )