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 ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
radcnv.r ⊢ R = sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
radcnvlt.x ⊢ φ → X ∈ ℂ
radcnvlt.a ⊢ φ → X < R
Assertion radcnvlt2 ⊢ φ → seq 0 + G ⁡ X ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 pser.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
2 radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
3 radcnv.r ⊢ R = sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
4 radcnvlt.x ⊢ φ → X ∈ ℂ
5 radcnvlt.a ⊢ φ → X < R
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 0zd ⊢ φ → 0 ∈ ℤ
8 1 2 4 psergf ⊢ φ → G ⁡ X : ℕ 0 ⟶ ℂ
9 fvco3 ⊢ G ⁡ X : ℕ 0 ⟶ ℂ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
10 8 9 sylan ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
11 8 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k ∈ ℂ
12 id ⊢ m = k → m = k
13 2fveq3 ⊢ m = k → G ⁡ X ⁡ m = G ⁡ X ⁡ k
14 12 13 oveq12d ⊢ m = k → m ⁢ G ⁡ X ⁡ m = k ⁢ G ⁡ X ⁡ k
15 14 cbvmptv ⊢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m = k ∈ ℕ 0 ⟼ k ⁢ G ⁡ X ⁡ k
16 1 2 3 4 5 15 radcnvlt1 ⊢ φ → seq 0 + m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ∈ dom ⁡ ⇝ ∧ seq 0 + abs ∘ G ⁡ X ∈ dom ⁡ ⇝
17 16 simprd ⊢ φ → seq 0 + abs ∘ G ⁡ X ∈ dom ⁡ ⇝
18 6 7 10 11 17 abscvgcvg ⊢ φ → seq 0 + G ⁡ X ∈ dom ⁡ ⇝