Metamath Proof Explorer

Theorem radcnvlt1

Description: If X is within the open disk of radius R centered at zero, then the infinite series converges absolutely at X , and also converges when the series is multiplied by n . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
radcnv.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
radcnvlt.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
radcnvlt.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
radcnvlt1.h ⊢ 𝐻 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
Assertion radcnvlt1 ( 𝜑 → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 pser.g ⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2 radcnv.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3 radcnv.r ⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
4 radcnvlt.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 radcnvlt.a ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
6 radcnvlt1.h ⊢ 𝐻 = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) )
7 ressxr ⊢ ℝ ⊆ ℝ*
8 4 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
9 7 8 sseldi ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ* )
10 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
11 1 2 3 radcnvcl ⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
12 10 11 sseldi ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
13 xrltnle ⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑋 ) < 𝑅 ↔ ¬ 𝑅 ≤ ( abs ‘ 𝑋 ) ) )
14 9 12 13 syl2anc ⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) < 𝑅 ↔ ¬ 𝑅 ≤ ( abs ‘ 𝑋 ) ) )
15 5 14 mpbid ⊢ ( 𝜑 → ¬ 𝑅 ≤ ( abs ‘ 𝑋 ) )
16 3 breq1i ⊢ ( 𝑅 ≤ ( abs ‘ 𝑋 ) ↔ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ≤ ( abs ‘ 𝑋 ) )
17 ssrab2 ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
18 17 7 sstri ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ*
19 supxrleub ⊢ ( ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* ∧ ( abs ‘ 𝑋 ) ∈ ℝ* ) → ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ≤ ( abs ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
20 18 9 19 sylancr ⊢ ( 𝜑 → ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ≤ ( abs ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
21 16 20 syl5bb ⊢ ( 𝜑 → ( 𝑅 ≤ ( abs ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
22 fveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑠 ) )
23 22 seqeq3d ⊢ ( 𝑟 = 𝑠 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) )
24 23 eleq1d ⊢ ( 𝑟 = 𝑠 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ) )
25 24 ralrab ⊢ ( ∀ 𝑠 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } 𝑠 ≤ ( abs ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ → 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
26 21 25 bitrdi ⊢ ( 𝜑 → ( 𝑅 ≤ ( abs ‘ 𝑋 ) ↔ ∀ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ → 𝑠 ≤ ( abs ‘ 𝑋 ) ) ) )
27 15 26 mtbid ⊢ ( 𝜑 → ¬ ∀ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ → 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
28 rexanali ⊢ ( ∃ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) ↔ ¬ ∀ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ → 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
29 27 28 sylibr ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
30 ltnle ⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 𝑠 ↔ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
31 8 30 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 𝑠 ↔ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ) → ( ( abs ‘ 𝑋 ) < 𝑠 ↔ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) )
33 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
34 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 𝑋 ∈ ℂ )
35 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 𝑠 ∈ ℝ )
36 35 recnd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 𝑠 ∈ ℂ )
37 simprr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → ( abs ‘ 𝑋 ) < 𝑠 )
38 0red ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 0 ∈ ℝ )
39 34 abscld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ )
40 34 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 0 ≤ ( abs ‘ 𝑋 ) )
41 38 39 35 40 37 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 0 < 𝑠 )
42 38 35 41 ltled ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → 0 ≤ 𝑠 )
43 35 42 absidd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → ( abs ‘ 𝑠 ) = 𝑠 )
44 37 43 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑠 ) )
45 simprl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ )
46 1 33 34 36 44 45 6 radcnvlem1 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )
47 1 33 34 36 44 45 radcnvlem2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ )
48 46 47 jca ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ( abs ‘ 𝑋 ) < 𝑠 ) ) → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) )
49 48 expr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ) → ( ( abs ‘ 𝑋 ) < 𝑠 → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) ) )
50 32 49 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ) → ( ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) ) )
51 50 expimpd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) ) )
52 51 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℝ ( seq 0 ( + , ( 𝐺 ‘ 𝑠 ) ) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ ( abs ‘ 𝑋 ) ) → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) ) )
53 29 52 mpd ⊢ ( 𝜑 → ( seq 0 ( + , 𝐻 ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) )