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 \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
		radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
		radcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
		radcnvlt.x	$⊢ φ \to X \in ℂ$
		radcnvlt.a	$⊢ φ \to \|X\| < R$
	Assertion	radcnvlt2	$⊢ φ \to seq 0 (+ G (X)) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		pser.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
3		radcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
4		radcnvlt.x	$⊢ φ \to X \in ℂ$
5		radcnvlt.a	$⊢ φ \to \|X\| < R$
6		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
7		0zd	$⊢ φ \to 0 \in ℤ$
8	1 2 4	psergf	$⊢ φ \to G (X) : ℕ_{0} ⟶ ℂ$
9		fvco3	$⊢ (G (X) : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to (abs \circ G (X)) (k) = \|G (X) (k)\|$
10	8 9	sylan	$⊢ (φ \land k \in ℕ_{0}) \to (abs \circ G (X)) (k) = \|G (X) (k)\|$
11	8	ffvelcdmda	$⊢ (φ \land k \in ℕ_{0}) \to G (X) (k) \in ℂ$
12		id	$⊢ m = k \to m = k$
13		2fveq3	$⊢ m = k \to \|G (X) (m)\| = \|G (X) (k)\|$
14	12 13	oveq12d	$⊢ m = k \to m \|G (X) (m)\| = k \|G (X) (k)\|$
15	14	cbvmptv	$⊢ (m \in ℕ_{0} ⟼ m \|G (X) (m)\|) = (k \in ℕ_{0} ⟼ k \|G (X) (k)\|)$
16	1 2 3 4 5 15	radcnvlt1	$⊢ φ \to (seq 0 (+ (m \in ℕ_{0} ⟼ m \|G (X) (m)\|)) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝)$
17	16	simprd	$⊢ φ \to seq 0 (+ (abs \circ G (X))) \in dom ⇝$
18	6 7 10 11 17	abscvgcvg	$⊢ φ \to seq 0 (+ G (X)) \in dom ⇝$