This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑋 ) ≤ 𝑅 )