radcnvcl

Description: The radius of convergence R of an infinite series is a nonnegative extended real number. (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 ⇝\} ℝ^{*} <)$
Assertion	radcnvcl	$⊢ φ \to R \in [0, +∞]$

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		ssrab2	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ$
5		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
6	4 5	sstri	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ^{*}$
7		supxrcl	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ^{} \to sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{*}$
8	6 7	mp1i	$⊢ φ \to sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{}$
9	3 8	eqeltrid	$⊢ φ \to R \in ℝ^{*}$
10	1 2	radcnv0	$⊢ φ \to 0 \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
11		supxrub	$⊢ (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ^{} \land 0 \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}) \to 0 \leq sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{} <)$
12	6 10 11	sylancr	$⊢ φ \to 0 \leq sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
13	12 3	breqtrrdi	$⊢ φ \to 0 \leq R$
14		pnfge	$⊢ R \in ℝ^{*} \to R \leq +∞$
15	9 14	syl	$⊢ φ \to R \leq +∞$
16		0xr	$⊢ 0 \in ℝ^{*}$
17		pnfxr	$⊢ +∞ \in ℝ^{*}$
18		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞))$
19	16 17 18	mp2an	$⊢ R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞)$
20	9 13 15 19	syl3anbrc	$⊢ φ \to R \in [0, +∞]$

Metamath Proof Explorer

Theorem radcnvcl

Proof