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 ffvelcdm ⊢ ( ( 𝐴 : ℕ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 addlidi ⊢ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ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 ffvelcdm ⊢ ( ( ( 𝑖 ∈ ℕ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 124 bilanri ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ℕ )
134 133 0expd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( 0 ↑ 𝑘 ) = 0 )
135 132 134 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( 𝑋 ↑ 𝑘 ) = 0 )
136 135 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) )
137 53 mul01d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
138 126 137 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · 0 ) = 0 )
140 136 139 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) = 0 )
141 140 abs00bd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) = 0 )
142 42 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ∈ ℂ )
143 142 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
144 126 143 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
145 144 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
146 131 141 145 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( 1 · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
147 df-ne ⊢ ( 𝑋 ≠ 0 ↔ ¬ 𝑋 = 0 )
148 56 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ∈ ℝ )
149 52 37 55 mulassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
150 149 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( abs ‘ ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
151 37 55 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ∈ ℂ )
152 52 151 absmuld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝑘 + 1 ) · ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) = ( ( abs ‘ ( 𝑘 + 1 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
153 35 127 absidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝑘 + 1 ) ) = ( 𝑘 + 1 ) )
154 153 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ ( 𝑘 + 1 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
155 150 152 154 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
156 148 155 eqled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
157 156 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
158 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ ℂ )
159 116 rpreccld ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ+ )
160 158 159 sylan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ+ )
161 160 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℂ )
162 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑘 + 1 ) ∈ ℂ )
163 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
164 163 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℂ )
165 161 162 164 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
166 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ∈ ℂ )
167 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ℂ )
168 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
169 166 167 168 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) / ( abs ‘ 𝑋 ) ) )
170 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
171 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
172 170 171 167 168 divassd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) ) )
173 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → 𝑘 ∈ ℂ )
174 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
175 173 10 174 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
176 175 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( 𝑋 ↑ 𝑘 ) )
177 21 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
178 177 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑘 + 1 ) ∈ ℤ )
179 167 168 178 expm1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) )
180 176 179 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ↑ 𝑘 ) = ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) )
181 180 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( ( 𝑋 ↑ ( 𝑘 + 1 ) ) / 𝑋 ) ) )
182 172 181 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) = ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) )
183 182 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) / 𝑋 ) ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
184 5 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
185 184 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ )
186 185 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℂ )
187 158 116 sylan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ∈ ℝ+ )
188 187 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ 𝑋 ) ≠ 0 )
189 164 186 188 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) / ( abs ‘ 𝑋 ) ) = ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) )
190 169 183 189 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) = ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
191 190 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑘 + 1 ) · ( ( 1 / ( abs ‘ 𝑋 ) ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
192 165 191 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) = ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ) )
193 157 192 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
194 126 193 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ 𝑋 ≠ 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
195 147 194 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) ∧ ¬ 𝑋 = 0 ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( ( 1 / ( abs ‘ 𝑋 ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
196 121 123 146 195 ifbothda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
197 51 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐻 ‘ 𝑘 ) ) = ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
198 126 197 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( 𝐻 ‘ 𝑘 ) ) = ( abs ‘ ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑋 ↑ 𝑘 ) ) ) )
199 34 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
200 126 199 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) = ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( 𝑘 + 1 ) · ( abs ‘ ( ( 𝐴 ‘ ( 𝑘 + 1 ) ) · ( 𝑋 ↑ ( 𝑘 + 1 ) ) ) ) ) ) )
201 196 198 200 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( 𝐻 ‘ 𝑘 ) ) ≤ ( if ( 𝑋 = 0 , 1 , ( 1 / ( abs ‘ 𝑋 ) ) ) · ( ( ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑖 ) ) ) ) shift - 1 ) ‘ 𝑘 ) ) )
202 7 9 43 57 113 119 201 cvgcmpce ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )