Metamath Proof Explorer

Theorem expcnv

Description: A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006) (Proof shortened by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses expcnv.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
expcnv.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
Assertion expcnv ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )

Proof

Step Hyp Ref Expression
1 expcnv.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 expcnv.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
3 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
4 1zzd ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → 1 ∈ ℤ )
5 nn0ex ⊢ ℕ0 ∈ V
6 5 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ∈ V
7 6 a1i ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ∈ V )
8 0cnd ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → 0 ∈ ℂ )
9 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
10 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
11 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
12 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
13 10 11 12 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
14 9 13 syl ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → 𝐴 = 0 )
16 15 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝐴 ↑ 𝑘 ) = ( 0 ↑ 𝑘 ) )
17 14 16 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 0 ↑ 𝑘 ) )
18 0exp ⊢ ( 𝑘 ∈ ℕ → ( 0 ↑ 𝑘 ) = 0 )
19 18 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( 0 ↑ 𝑘 ) = 0 )
20 17 19 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = 0 )
21 3 4 7 8 20 climconst ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
22 1zzd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 1 ∈ ℤ )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) < 1 )
24 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
25 1 24 sylan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
26 25 reclt1d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) < 1 ↔ 1 < ( 1 / ( abs ‘ 𝐴 ) ) ) )
27 23 26 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 1 < ( 1 / ( abs ‘ 𝐴 ) ) )
28 1re ⊢ 1 ∈ ℝ
29 25 rpreccld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ+ )
30 29 rpred ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ )
31 difrp ⊢ ( ( 1 ∈ ℝ ∧ ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ ) → ( 1 < ( 1 / ( abs ‘ 𝐴 ) ) ↔ ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℝ+ ) )
32 28 30 31 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 < ( 1 / ( abs ‘ 𝐴 ) ) ↔ ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℝ+ ) )
33 27 32 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℝ+ )
34 33 rpreccld ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) ∈ ℝ+ )
35 34 rpcnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) ∈ ℂ )
36 divcnv ⊢ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ⇝ 0 )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ⇝ 0 )
38 nnex ⊢ ℕ ∈ V
39 38 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ∈ V
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ∈ V )
41 oveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) = ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) )
42 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) )
43 ovex ⊢ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) ∈ V
44 41 42 43 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) )
46 34 rpred ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) ∈ ℝ )
47 nndivre ⊢ ( ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) ∈ ℝ )
48 46 47 sylan ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) ∈ ℝ )
49 45 48 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
50 oveq2 ⊢ ( 𝑛 = 𝑘 → ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
51 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) )
52 ovex ⊢ ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ V
53 50 51 52 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
54 53 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
55 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
56 rpexpcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ+ )
57 25 55 56 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ∈ ℝ+ )
58 54 57 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ+ )
59 58 rpred ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
60 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
61 rpmulcl ⊢ ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℝ+ ∧ 𝑘 ∈ ℝ+ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ∈ ℝ+ )
62 33 60 61 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ∈ ℝ+ )
63 62 rpred ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ∈ ℝ )
64 peano2re ⊢ ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ∈ ℝ → ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) + 1 ) ∈ ℝ )
65 63 64 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) + 1 ) ∈ ℝ )
66 rpexpcl ⊢ ( ( ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ∈ ℝ+ )
67 29 55 66 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ∈ ℝ+ )
68 67 rpred ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) ∈ ℝ )
69 63 lep1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ≤ ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) + 1 ) )
70 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ )
71 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
72 29 rpge0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( 1 / ( abs ‘ 𝐴 ) ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 1 / ( abs ‘ 𝐴 ) ) )
74 bernneq2 ⊢ ( ( ( 1 / ( abs ‘ 𝐴 ) ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ ( 1 / ( abs ‘ 𝐴 ) ) ) → ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) + 1 ) ≤ ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) )
75 70 71 73 74 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) + 1 ) ≤ ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) )
76 63 65 68 69 75 letrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ≤ ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) )
77 25 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ) )
78 exprec ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
79 78 3expa ⊢ ( ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ) ∧ 𝑘 ∈ ℤ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
80 77 55 79 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( abs ‘ 𝐴 ) ) ↑ 𝑘 ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
81 76 80 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ≤ ( 1 / ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
82 62 57 81 lerec2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ≤ ( 1 / ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ) )
83 33 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℂ ∧ ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ≠ 0 ) )
84 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
85 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
86 84 85 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
87 recdiv2 ⊢ ( ( ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ∈ ℂ ∧ ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ≠ 0 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) ) → ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) = ( 1 / ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ) )
88 83 86 87 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) = ( 1 / ( ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) · 𝑘 ) ) )
89 82 88 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ≤ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑘 ) )
90 89 54 45 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 1 / ( ( 1 / ( abs ‘ 𝐴 ) ) − 1 ) ) / 𝑛 ) ) ‘ 𝑘 ) )
91 58 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) )
92 3 22 37 40 49 59 90 91 climsqz2 ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ⇝ 0 )
93 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
94 6 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ∈ V )
95 39 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ∈ V )
96 9 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
97 96 13 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
98 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
99 1 9 98 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
100 97 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) ∈ ℂ )
101 absexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
102 1 9 101 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
103 97 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) ) = ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) )
104 53 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
105 102 103 104 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) ) )
106 3 93 94 95 100 105 climabs0 ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 ↔ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ⇝ 0 ) )
107 106 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ↦ ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) ) ⇝ 0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
108 92 107 syldan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
109 21 108 pm2.61dane ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )