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 ⇝ )