Metamath Proof Explorer


Theorem dvradcnv

Description: The radius of convergence of the (formal) derivative H of the power series G is at least as large as the radius of convergence of G . (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses dvradcnv.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
dvradcnv.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
dvradcnv.h 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑋𝑛 ) ) )
dvradcnv.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
dvradcnv.x ( 𝜑𝑋 ∈ ℂ )
dvradcnv.l ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
Assertion dvradcnv ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 dvradcnv.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
2 dvradcnv.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
3 dvradcnv.h 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑋𝑛 ) ) )
4 dvradcnv.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
5 dvradcnv.x ( 𝜑𝑋 ∈ ℂ )
6 dvradcnv.l ( 𝜑 → ( abs ‘ 𝑋 ) < 𝑅 )
7 nn0uz 0 = ( ℤ ‘ 0 )
8 1nn0 1 ∈ ℕ0
9 8 a1i ( 𝜑 → 1 ∈ ℕ0 )
10 ax-1cn 1 ∈ ℂ
11 nn0cn ( 𝑘 ∈ ℕ0𝑘 ∈ ℂ )
12 11 adantl ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
13 nn0ex 0 ∈ V
14 13 mptex ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ∈ V
15 14 shftval4 ( ( 1 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) )
16 10 12 15 sylancr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) )
17 addcom ( ( 1 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 1 + 𝑘 ) = ( 𝑘 + 1 ) )
18 10 12 17 sylancr ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 1 + 𝑘 ) = ( 𝑘 + 1 ) )
19 18 fveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) = ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 𝑘 + 1 ) ) )
20 peano2nn0 ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
21 20 adantl ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
22 id ( 𝑖 = ( 𝑘 + 1 ) → 𝑖 = ( 𝑘 + 1 ) )
23 2fveq3 ( 𝑖 = ( 𝑘 + 1 ) → ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) )
24 22 23 oveq12d ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) ) )
25 eqid ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) )
26 ovex ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) ) ∈ V
27 24 25 26 fvmpt ( ( 𝑘 + 1 ) ∈ ℕ0 → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) ) )
28 21 27 syl ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) ) )
29 1 pserval2 ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) )
30 5 20 29 syl2an ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) )
31 30 fveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) )
32 31 oveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐺𝑋 ) ‘ ( 𝑘 + 1 ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
33 28 32 eqtrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
34 16 19 33 3eqtrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
35 21 nn0red ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℝ )
36 ffvelrn ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
37 4 20 36 syl2an ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
38 expcl ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝑋 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
39 5 20 38 syl2an ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑋 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
40 37 39 mulcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ∈ ℂ )
41 40 abscld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
42 35 41 remulcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ∈ ℝ )
43 34 42 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ∈ ℝ )
44 oveq1 ( 𝑛 = 𝑘 → ( 𝑛 + 1 ) = ( 𝑘 + 1 ) )
45 44 fveq2d ( 𝑛 = 𝑘 → ( 𝐴 ‘ ( 𝑛 + 1 ) ) = ( 𝐴 ‘ ( 𝑘 + 1 ) ) )
46 44 45 oveq12d ( 𝑛 = 𝑘 → ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) = ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
47 oveq2 ( 𝑛 = 𝑘 → ( 𝑋𝑛 ) = ( 𝑋𝑘 ) )
48 46 47 oveq12d ( 𝑛 = 𝑘 → ( ( ( 𝑛 + 1 ) · ( 𝐴 ‘ ( 𝑛 + 1 ) ) ) · ( 𝑋𝑛 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) )
49 ovex ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ∈ V
50 48 3 49 fvmpt ( 𝑘 ∈ ℕ0 → ( 𝐻𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) )
51 50 adantl ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐻𝑘 ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) )
52 21 nn0cnd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℂ )
53 52 37 mulcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) ∈ ℂ )
54 expcl ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑋𝑘 ) ∈ ℂ )
55 5 54 sylan ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑋𝑘 ) ∈ ℂ )
56 53 55 mulcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ∈ ℂ )
57 51 56 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐻𝑘 ) ∈ ℂ )
58 id ( 𝑖 = 𝑘𝑖 = 𝑘 )
59 2fveq3 ( 𝑖 = 𝑘 → ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑘 ) ) )
60 58 59 oveq12d ( 𝑖 = 𝑘 → ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑘 ) ) ) )
61 60 cbvmptv ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑘 ) ) ) )
62 1 4 2 5 6 61 radcnvlt1 ( 𝜑 → ( seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺𝑋 ) ) ) ∈ dom ⇝ ) )
63 62 simpld ( 𝜑 → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ∈ dom ⇝ )
64 climdm ( seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) )
65 63 64 sylib ( 𝜑 → seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) )
66 0z 0 ∈ ℤ
67 neg1z - 1 ∈ ℤ
68 14 isershft ( ( 0 ∈ ℤ ∧ - 1 ∈ ℤ ) → ( seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) ↔ seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) ) )
69 66 67 68 mp2an ( seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) ↔ seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) )
70 65 69 sylib ( 𝜑 → seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) )
71 seqex seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ V
72 fvex ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) ∈ V
73 71 72 breldm ( seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ) ) → seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ dom ⇝ )
74 70 73 syl ( 𝜑 → seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ dom ⇝ )
75 eqid ( ℤ ‘ ( 0 + - 1 ) ) = ( ℤ ‘ ( 0 + - 1 ) )
76 neg1cn - 1 ∈ ℂ
77 76 addid2i ( 0 + - 1 ) = - 1
78 0le1 0 ≤ 1
79 1re 1 ∈ ℝ
80 le0neg2 ( 1 ∈ ℝ → ( 0 ≤ 1 ↔ - 1 ≤ 0 ) )
81 79 80 ax-mp ( 0 ≤ 1 ↔ - 1 ≤ 0 )
82 78 81 mpbi - 1 ≤ 0
83 77 82 eqbrtri ( 0 + - 1 ) ≤ 0
84 77 67 eqeltri ( 0 + - 1 ) ∈ ℤ
85 84 eluz1i ( 0 ∈ ( ℤ ‘ ( 0 + - 1 ) ) ↔ ( 0 ∈ ℤ ∧ ( 0 + - 1 ) ≤ 0 ) )
86 66 83 85 mpbir2an 0 ∈ ( ℤ ‘ ( 0 + - 1 ) )
87 86 a1i ( 𝜑 → 0 ∈ ( ℤ ‘ ( 0 + - 1 ) ) )
88 eluzelcn ( 𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) → 𝑘 ∈ ℂ )
89 88 adantl ( ( 𝜑𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) ) → 𝑘 ∈ ℂ )
90 10 89 15 sylancr ( ( 𝜑𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) )
91 nn0re ( 𝑖 ∈ ℕ0𝑖 ∈ ℝ )
92 91 adantl ( ( 𝜑𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℝ )
93 1 4 5 psergf ( 𝜑 → ( 𝐺𝑋 ) : ℕ0 ⟶ ℂ )
94 93 ffvelrnda ( ( 𝜑𝑖 ∈ ℕ0 ) → ( ( 𝐺𝑋 ) ‘ 𝑖 ) ∈ ℂ )
95 94 abscld ( ( 𝜑𝑖 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ∈ ℝ )
96 92 95 remulcld ( ( 𝜑𝑖 ∈ ℕ0 ) → ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ∈ ℝ )
97 96 recnd ( ( 𝜑𝑖 ∈ ℕ0 ) → ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ∈ ℂ )
98 97 fmpttd ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) : ℕ0 ⟶ ℂ )
99 10 88 17 sylancr ( 𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) → ( 1 + 𝑘 ) = ( 𝑘 + 1 ) )
100 eluzp1p1 ( 𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) → ( 𝑘 + 1 ) ∈ ( ℤ ‘ ( ( 0 + - 1 ) + 1 ) ) )
101 77 oveq1i ( ( 0 + - 1 ) + 1 ) = ( - 1 + 1 )
102 1pneg1e0 ( 1 + - 1 ) = 0
103 10 76 102 addcomli ( - 1 + 1 ) = 0
104 101 103 eqtri ( ( 0 + - 1 ) + 1 ) = 0
105 104 fveq2i ( ℤ ‘ ( ( 0 + - 1 ) + 1 ) ) = ( ℤ ‘ 0 )
106 7 105 eqtr4i 0 = ( ℤ ‘ ( ( 0 + - 1 ) + 1 ) )
107 100 106 eleqtrrdi ( 𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) → ( 𝑘 + 1 ) ∈ ℕ0 )
108 99 107 eqeltrd ( 𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) → ( 1 + 𝑘 ) ∈ ℕ0 )
109 ffvelrn ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) : ℕ0 ⟶ ℂ ∧ ( 1 + 𝑘 ) ∈ ℕ0 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) ∈ ℂ )
110 98 108 109 syl2an ( ( 𝜑𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) ) → ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) ‘ ( 1 + 𝑘 ) ) ∈ ℂ )
111 90 110 eqeltrd ( ( 𝜑𝑘 ∈ ( ℤ ‘ ( 0 + - 1 ) ) ) → ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ∈ ℂ )
112 75 87 111 iserex ( 𝜑 → ( seq ( 0 + - 1 ) ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ dom ⇝ ) )
113 74 112 mpbid ( 𝜑 → seq 0 ( + , ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ) ∈ dom ⇝ )
114 1red ( ( 𝜑𝑋 = 0 ) → 1 ∈ ℝ )
115 neqne ( ¬ 𝑋 = 0 → 𝑋 ≠ 0 )
116 absrpcl ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ+ )
117 5 115 116 syl2an ( ( 𝜑 ∧ ¬ 𝑋 = 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ+ )
118 117 rprecred ( ( 𝜑 ∧ ¬ 𝑋 = 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ )
119 114 118 ifclda ( 𝜑 → if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) ∈ ℝ )
120 oveq1 ( 1 = if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
121 120 breq2d ( 1 = if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) → ( ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) ↔ ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) ) )
122 oveq1 ( ( 1 / ( abs ‘ 𝑋 ) ) = if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
123 122 breq2d ( ( 1 / ( abs ‘ 𝑋 ) ) = if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) → ( ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) ↔ ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) ) )
124 elnnuz ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ ‘ 1 ) )
125 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
126 124 125 sylbir ( 𝑘 ∈ ( ℤ ‘ 1 ) → 𝑘 ∈ ℕ0 )
127 21 nn0ge0d ( ( 𝜑𝑘 ∈ ℕ0 ) → 0 ≤ ( 𝑘 + 1 ) )
128 40 absge0d ( ( 𝜑𝑘 ∈ ℕ0 ) → 0 ≤ ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) )
129 35 41 127 128 mulge0d ( ( 𝜑𝑘 ∈ ℕ0 ) → 0 ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
130 126 129 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → 0 ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
131 130 adantr ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → 0 ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
132 oveq1 ( 𝑋 = 0 → ( 𝑋𝑘 ) = ( 0 ↑ 𝑘 ) )
133 simpr ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
134 133 124 sylibr ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → 𝑘 ∈ ℕ )
135 134 0expd ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( 0 ↑ 𝑘 ) = 0 )
136 132 135 sylan9eqr ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( 𝑋𝑘 ) = 0 )
137 136 oveq2d ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) )
138 53 mul01d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
139 126 138 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
140 139 adantr ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
141 137 140 eqtrd ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) = 0 )
142 141 abs00bd ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) = 0 )
143 42 recnd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ∈ ℂ )
144 143 mulid2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
145 126 144 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
146 145 adantr ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
147 131 142 146 3brtr4d ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
148 df-ne ( 𝑋 ≠ 0 ↔ ¬ 𝑋 = 0 )
149 56 abscld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ∈ ℝ )
150 52 37 55 mulassd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) = ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) )
151 150 fveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) = ( abs ‘ ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
152 37 55 mulcld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ∈ ℂ )
153 52 152 absmuld ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) = ( ( abs ‘ ( 𝑘 + 1 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
154 35 127 absidd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑘 + 1 ) ) = ( 𝑘 + 1 ) )
155 154 oveq1d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( abs ‘ ( 𝑘 + 1 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
156 151 153 155 3eqtrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
157 149 156 eqled ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
158 157 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
159 5 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑋 ∈ ℂ )
160 116 rpreccld ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ+ )
161 159 160 sylan ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ+ )
162 161 rpcnd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℂ )
163 52 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑘 + 1 ) ∈ ℂ )
164 41 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
165 164 recnd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
166 162 163 165 mul12d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
167 40 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ∈ ℂ )
168 5 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ℂ )
169 simpr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
170 167 168 169 absdivd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) / ( abs ‘ 𝑋 ) ) )
171 37 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
172 39 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
173 171 172 168 169 divassd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) ) )
174 12 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑘 ∈ ℂ )
175 pncan ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
176 174 10 175 sylancl ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
177 176 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( 𝑋𝑘 ) )
178 21 nn0zd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
179 178 adantr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑘 + 1 ) ∈ ℤ )
180 168 169 179 expm1d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) )
181 177 180 eqtr3d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋𝑘 ) = ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) )
182 181 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) ) )
183 173 182 eqtr4d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) )
184 183 fveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) )
185 5 abscld ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
186 185 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ )
187 186 recnd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℂ )
188 159 116 sylan ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ+ )
189 188 rpne0d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ≠ 0 )
190 165 187 189 divrec2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) / ( abs ‘ 𝑋 ) ) = ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
191 170 184 190 3eqtr3rd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) )
192 191 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑘 + 1 ) · ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
193 166 192 eqtrd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋𝑘 ) ) ) ) )
194 158 193 breqtrrd ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
195 126 194 sylanl2 ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
196 148 195 sylan2br ( ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) ∧ ¬ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
197 121 123 147 196 ifbothda ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
198 51 fveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐻𝑘 ) ) = ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) )
199 126 198 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( abs ‘ ( 𝐻𝑘 ) ) = ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋𝑘 ) ) ) )
200 34 oveq2d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
201 126 200 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
202 197 199 201 3brtr4d ( ( 𝜑𝑘 ∈ ( ℤ ‘ 1 ) ) → ( abs ‘ ( 𝐻𝑘 ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) )
203 7 9 43 57 113 119 202 cvgcmpce ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )