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

Metamath Proof Explorer

Theorem radcnvlt2

Description: If X is within the open disk of radius R centered at zero, then the infinite series converges at X . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
radcnv.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
radcnvlt.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
radcnvlt.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
Assertion radcnvlt2 ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3 radcnv.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
4 radcnvlt.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 radcnvlt.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
6 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
8 1 2 4 psergf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ )
9 fvco3 ⊢ ( ( ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) )
10 8 9 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) )
11 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ∈ ℂ )
12 id ⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 )
13 2fveq3 ⊢ ( 𝑚 = 𝑘 → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) )
14 12 13 oveq12d ⊢ ( 𝑚 = 𝑘 → ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) )
15 14 cbvmptv ⊢ ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) )
16 1 2 3 4 5 15 radcnvlt1 ⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) )
17 16 simprd ⊢ ( 𝜑 → seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ )
18 6 7 10 11 17 abscvgcvg ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ )