Metamath Proof Explorer

Theorem radcnvle

Description: If X is a convergent point of the infinite series, then X is within the closed disk of radius R centered at zero. Or, by contraposition, the series diverges at any point strictly more than R from the origin. (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 ⁡ ⇝ ℝ * <
radcnvle.x ⊢ φ → X ∈ ℂ
radcnvle.a ⊢ φ → seq 0 + G ⁡ X ∈ dom ⁡ ⇝
Assertion radcnvle ⊢ φ → X ≤ R

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 radcnvle.x ⊢ φ → X ∈ ℂ
5 radcnvle.a ⊢ φ → seq 0 + G ⁡ X ∈ dom ⁡ ⇝
6 ressxr ⊢ ℝ ⊆ ℝ *
7 4 abscld ⊢ φ → X ∈ ℝ
8 6 7 sselid ⊢ φ → X ∈ ℝ *
9 iccssxr ⊢ 0 +∞ ⊆ ℝ *
10 1 2 3 radcnvcl ⊢ φ → R ∈ 0 +∞
11 9 10 sselid ⊢ φ → R ∈ ℝ *
12 simpr ⊢ φ ∧ R < X → R < X
13 11 adantr ⊢ φ ∧ R < X → R ∈ ℝ *
14 7 adantr ⊢ φ ∧ R < X → X ∈ ℝ
15 0xr ⊢ 0 ∈ ℝ *
16 pnfxr ⊢ +∞ ∈ ℝ *
17 elicc1 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * → R ∈ 0 +∞ ↔ R ∈ ℝ * ∧ 0 ≤ R ∧ R ≤ +∞
18 15 16 17 mp2an ⊢ R ∈ 0 +∞ ↔ R ∈ ℝ * ∧ 0 ≤ R ∧ R ≤ +∞
19 10 18 sylib ⊢ φ → R ∈ ℝ * ∧ 0 ≤ R ∧ R ≤ +∞
20 19 simp2d ⊢ φ → 0 ≤ R
21 ge0gtmnf ⊢ R ∈ ℝ * ∧ 0 ≤ R → −∞ < R
22 11 20 21 syl2anc ⊢ φ → −∞ < R
23 22 adantr ⊢ φ ∧ R < X → −∞ < R
24 8 adantr ⊢ φ ∧ R < X → X ∈ ℝ *
25 13 24 12 xrltled ⊢ φ ∧ R < X → R ≤ X
26 xrre ⊢ R ∈ ℝ * ∧ X ∈ ℝ ∧ −∞ < R ∧ R ≤ X → R ∈ ℝ
27 13 14 23 25 26 syl22anc ⊢ φ ∧ R < X → R ∈ ℝ
28 avglt1 ⊢ R ∈ ℝ ∧ X ∈ ℝ → R < X ↔ R < R + X 2
29 27 14 28 syl2anc ⊢ φ ∧ R < X → R < X ↔ R < R + X 2
30 12 29 mpbid ⊢ φ ∧ R < X → R < R + X 2
31 27 14 readdcld ⊢ φ ∧ R < X → R + X ∈ ℝ
32 31 rehalfcld ⊢ φ ∧ R < X → R + X 2 ∈ ℝ
33 ssrab2 ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ
34 33 6 sstri ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ *
35 2 adantr ⊢ φ ∧ R < X → A : ℕ 0 ⟶ ℂ
36 32 recnd ⊢ φ ∧ R < X → R + X 2 ∈ ℂ
37 4 adantr ⊢ φ ∧ R < X → X ∈ ℂ
38 0red ⊢ φ ∧ R < X → 0 ∈ ℝ
39 20 adantr ⊢ φ ∧ R < X → 0 ≤ R
40 38 27 32 39 30 lelttrd ⊢ φ ∧ R < X → 0 < R + X 2
41 38 32 40 ltled ⊢ φ ∧ R < X → 0 ≤ R + X 2
42 32 41 absidd ⊢ φ ∧ R < X → R + X 2 = R + X 2
43 avglt2 ⊢ R ∈ ℝ ∧ X ∈ ℝ → R < X ↔ R + X 2 < X
44 27 14 43 syl2anc ⊢ φ ∧ R < X → R < X ↔ R + X 2 < X
45 12 44 mpbid ⊢ φ ∧ R < X → R + X 2 < X
46 42 45 eqbrtrd ⊢ φ ∧ R < X → R + X 2 < X
47 5 adantr ⊢ φ ∧ R < X → seq 0 + G ⁡ X ∈ dom ⁡ ⇝
48 1 35 36 37 46 47 radcnvlem3 ⊢ φ ∧ R < X → seq 0 + G ⁡ R + X 2 ∈ dom ⁡ ⇝
49 fveq2 ⊢ y = R + X 2 → G ⁡ y = G ⁡ R + X 2
50 49 seqeq3d ⊢ y = R + X 2 → seq 0 + G ⁡ y = seq 0 + G ⁡ R + X 2
51 50 eleq1d ⊢ y = R + X 2 → seq 0 + G ⁡ y ∈ dom ⁡ ⇝ ↔ seq 0 + G ⁡ R + X 2 ∈ dom ⁡ ⇝
52 fveq2 ⊢ r = y → G ⁡ r = G ⁡ y
53 52 seqeq3d ⊢ r = y → seq 0 + G ⁡ r = seq 0 + G ⁡ y
54 53 eleq1d ⊢ r = y → seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ↔ seq 0 + G ⁡ y ∈ dom ⁡ ⇝
55 54 cbvrabv ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ = y ∈ ℝ | seq 0 + G ⁡ y ∈ dom ⁡ ⇝
56 51 55 elrab2 ⊢ R + X 2 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ↔ R + X 2 ∈ ℝ ∧ seq 0 + G ⁡ R + X 2 ∈ dom ⁡ ⇝
57 32 48 56 sylanbrc ⊢ φ ∧ R < X → R + X 2 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝
58 supxrub ⊢ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ * ∧ R + X 2 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ → R + X 2 ≤ sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
59 34 57 58 sylancr ⊢ φ ∧ R < X → R + X 2 ≤ sup r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ℝ * <
60 59 3 breqtrrdi ⊢ φ ∧ R < X → R + X 2 ≤ R
61 32 27 60 lensymd ⊢ φ ∧ R < X → ¬ R < R + X 2
62 30 61 pm2.65da ⊢ φ → ¬ R < X
63 8 11 62 xrnltled ⊢ φ → X ≤ R