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	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
	radcnv.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < )
Assertion	radcnvcl	⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
3		radcnv.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < )
4		ssrab2	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
5		ressxr	⊢ ℝ ⊆ ℝ^*
6	4 5	sstri	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ^*
7		supxrcl	⊢ ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ^* → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) ∈ ℝ^* )
8	6 7	mp1i	⊢ ( 𝜑 → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) ∈ ℝ^* )
9	3 8	eqeltrid	⊢ ( 𝜑 → 𝑅 ∈ ℝ^* )
10	1 2	radcnv0	⊢ ( 𝜑 → 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )
11		supxrub	⊢ ( ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ^* ∧ 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → 0 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) )
12	6 10 11	sylancr	⊢ ( 𝜑 → 0 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ^* , < ) )
13	12 3	breqtrrdi	⊢ ( 𝜑 → 0 ≤ 𝑅 )
14		pnfge	⊢ ( 𝑅 ∈ ℝ^* → 𝑅 ≤ +∞ )
15	9 14	syl	⊢ ( 𝜑 → 𝑅 ≤ +∞ )
16		0xr	⊢ 0 ∈ ℝ^*
17		pnfxr	⊢ +∞ ∈ ℝ^*
18		elicc1	⊢ ( ( 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) )
19	16 17 18	mp2an	⊢ ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ^* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) )
20	9 13 15 19	syl3anbrc	⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )

Metamath Proof Explorer

Theorem radcnvcl

Proof