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 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
radcnv.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
radcnv.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
radcnvle.x ( 𝜑𝑋 ∈ ℂ )
radcnvle.a ( 𝜑 → seq 0 ( + , ( 𝐺𝑋 ) ) ∈ dom ⇝ )
Assertion radcnvle ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 𝑅 )

Proof

Step Hyp Ref Expression
1 pser.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
2 radcnv.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
3 radcnv.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
4 radcnvle.x ( 𝜑𝑋 ∈ ℂ )
5 radcnvle.a ( 𝜑 → seq 0 ( + , ( 𝐺𝑋 ) ) ∈ dom ⇝ )
6 ressxr ℝ ⊆ ℝ*
7 4 abscld ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
8 6 7 sselid ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ* )
9 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
10 1 2 3 radcnvcl ( 𝜑𝑅 ∈ ( 0 [,] +∞ ) )
11 9 10 sselid ( 𝜑𝑅 ∈ ℝ* )
12 simpr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( abs ‘ 𝑋 ) )
13 11 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ* )
14 7 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
15 0xr 0 ∈ ℝ*
16 pnfxr +∞ ∈ ℝ*
17 elicc1 ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) ) )
18 15 16 17 mp2an ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) )
19 10 18 sylib ( 𝜑 → ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) )
20 19 simp2d ( 𝜑 → 0 ≤ 𝑅 )
21 ge0gtmnf ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → -∞ < 𝑅 )
22 11 20 21 syl2anc ( 𝜑 → -∞ < 𝑅 )
23 22 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → -∞ < 𝑅 )
24 8 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ* )
25 13 24 12 xrltled ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ≤ ( abs ‘ 𝑋 ) )
26 xrre ( ( ( 𝑅 ∈ ℝ* ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) ∧ ( -∞ < 𝑅𝑅 ≤ ( abs ‘ 𝑋 ) ) ) → 𝑅 ∈ ℝ )
27 13 14 23 25 26 syl22anc ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ )
28 avglt1 ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
29 27 14 28 syl2anc ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
30 12 29 mpbid ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
31 27 14 readdcld ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 + ( abs ‘ 𝑋 ) ) ∈ ℝ )
32 31 rehalfcld ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ )
33 ssrab2 { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
34 33 6 sstri { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ*
35 2 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
36 32 recnd ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℂ )
37 4 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 𝑋 ∈ ℂ )
38 0red ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 0 ∈ ℝ )
39 20 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ 𝑅 )
40 38 27 32 39 30 lelttrd ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 0 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
41 38 32 40 ltled ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
42 32 41 absidd ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
43 avglt2 ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) )
44 27 14 43 syl2anc ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) )
45 12 44 mpbid ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) )
46 42 45 eqbrtrd ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) < ( abs ‘ 𝑋 ) )
47 5 adantr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺𝑋 ) ) ∈ dom ⇝ )
48 1 35 36 37 46 47 radcnvlem3 ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ )
49 fveq2 ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( 𝐺𝑦 ) = ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) )
50 49 seqeq3d ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → seq 0 ( + , ( 𝐺𝑦 ) ) = seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) )
51 50 eleq1d ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( seq 0 ( + , ( 𝐺𝑦 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) )
52 fveq2 ( 𝑟 = 𝑦 → ( 𝐺𝑟 ) = ( 𝐺𝑦 ) )
53 52 seqeq3d ( 𝑟 = 𝑦 → seq 0 ( + , ( 𝐺𝑟 ) ) = seq 0 ( + , ( 𝐺𝑦 ) ) )
54 53 eleq1d ( 𝑟 = 𝑦 → ( seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺𝑦 ) ) ∈ dom ⇝ ) )
55 54 cbvrabv { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑦 ) ) ∈ dom ⇝ }
56 51 55 elrab2 ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } ↔ ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ ∧ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) )
57 32 48 56 sylanbrc ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } )
58 supxrub ( ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* ∧ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
59 34 57 58 sylancr ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
60 59 3 breqtrrdi ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ 𝑅 )
61 32 27 60 lensymd ( ( 𝜑𝑅 < ( abs ‘ 𝑋 ) ) → ¬ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) )
62 30 61 pm2.65da ( 𝜑 → ¬ 𝑅 < ( abs ‘ 𝑋 ) )
63 8 11 62 xrnltled ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 𝑅 )