This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑛 ∈ ℕ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 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )