Metamath Proof Explorer

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

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 ssrab2 ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ
5 ressxr ⊢ ℝ ⊆ ℝ *
6 4 5 sstri ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ *
7 supxrcl ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ * → sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ ℝ *
8 6 7 mp1i ⊢ φ → sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ ℝ *
9 3 8 eqeltrid ⊢ φ → R ∈ ℝ *
10 1 2 radcnv0 ⊢ φ → 0 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝
11 supxrub ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ * ∧ 0 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ → 0 ≤ sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
12 6 10 11 sylancr ⊢ φ → 0 ≤ sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
13 12 3 breqtrrdi ⊢ φ → 0 ≤ R
14 pnfge ⊢ R ∈ ℝ * → R ≤ +∞
15 9 14 syl ⊢ φ → R ≤ +∞
16 0xr ⊢ 0 ∈ ℝ *
17 pnfxr ⊢ +∞ ∈ ℝ *
18 elicc1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → R ∈ 0 +∞ ↔ R ∈ ℝ * ∧ 0 ≤ R ∧ R ≤ +∞
19 16 17 18 mp2an ⊢ R ∈ 0 +∞ ↔ R ∈ ℝ * ∧ 0 ≤ R ∧ R ≤ +∞
20 9 13 15 19 syl3anbrc ⊢ φ → R ∈ 0 +∞