| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12921 | . . 3
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12648 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → 1 ∈
ℤ) | 
| 3 |  | nn0ex 12532 | . . . . 5
⊢
ℕ0 ∈ V | 
| 4 | 3 | mptex 7243 | . . . 4
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) ∈ V | 
| 5 | 4 | a1i 11 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ∈ V) | 
| 6 |  | 0cnd 11254 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℂ) | 
| 7 |  | nnnn0 12533 | . . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 8 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐴↑𝑛) = (𝐴↑𝑘)) | 
| 9 |  | eqid 2737 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) | 
| 10 |  | ovex 7464 | . . . . . . 7
⊢ (𝐴↑𝑘) ∈ V | 
| 11 | 8, 9, 10 | fvmpt 7016 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) | 
| 12 | 7, 11 | syl 17 | . . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) | 
| 13 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 = 0) | 
| 14 | 13 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝐴↑𝑘) = (0↑𝑘)) | 
| 15 | 12, 14 | sylan9eqr 2799 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (0↑𝑘)) | 
| 16 |  | 0exp 14138 | . . . . 5
⊢ (𝑘 ∈ ℕ →
(0↑𝑘) =
0) | 
| 17 | 16 | adantl 481 | . . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (0↑𝑘) = 0) | 
| 18 | 15, 17 | eqtrd 2777 | . . 3
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = 0) | 
| 19 | 1, 2, 5, 6, 18 | climconst 15579 | . 2
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) | 
| 20 |  | 1zzd 12648 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 1 ∈
ℤ) | 
| 21 |  | expcnv.2 | . . . . . . . . . 10
⊢ (𝜑 → (abs‘𝐴) < 1) | 
| 22 | 21 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) < 1) | 
| 23 |  | expcnv.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 24 |  | absrpcl 15327 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 25 | 23, 24 | sylan 580 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 26 | 25 | reclt1d 13090 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐴) < 1 ↔ 1 < (1 /
(abs‘𝐴)))) | 
| 27 | 22, 26 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 1 < (1 / (abs‘𝐴))) | 
| 28 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 29 | 25 | rpreccld 13087 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 / (abs‘𝐴)) ∈
ℝ+) | 
| 30 | 29 | rpred 13077 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 / (abs‘𝐴)) ∈
ℝ) | 
| 31 |  | difrp 13073 | . . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (1 / (abs‘𝐴)) ∈ ℝ) → (1 < (1 /
(abs‘𝐴)) ↔ ((1 /
(abs‘𝐴)) − 1)
∈ ℝ+)) | 
| 32 | 28, 30, 31 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 < (1 /
(abs‘𝐴)) ↔ ((1 /
(abs‘𝐴)) − 1)
∈ ℝ+)) | 
| 33 | 27, 32 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((1 / (abs‘𝐴)) − 1) ∈
ℝ+) | 
| 34 | 33 | rpreccld 13087 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 / ((1 / (abs‘𝐴)) − 1)) ∈
ℝ+) | 
| 35 | 34 | rpcnd 13079 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 / ((1 / (abs‘𝐴)) − 1)) ∈
ℂ) | 
| 36 |  | divcnv 15889 | . . . . 5
⊢ ((1 / ((1
/ (abs‘𝐴)) −
1)) ∈ ℂ → (𝑛 ∈ ℕ ↦ ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑛)) ⇝
0) | 
| 37 | 35, 36 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ ℕ ↦ ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑛)) ⇝
0) | 
| 38 |  | nnex 12272 | . . . . . 6
⊢ ℕ
∈ V | 
| 39 | 38 | mptex 7243 | . . . . 5
⊢ (𝑛 ∈ ℕ ↦
((abs‘𝐴)↑𝑛)) ∈ V | 
| 40 | 39 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) ∈ V) | 
| 41 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑛 = 𝑘 → ((1 / ((1 / (abs‘𝐴)) − 1)) / 𝑛) = ((1 / ((1 / (abs‘𝐴)) − 1)) / 𝑘)) | 
| 42 |  | eqid 2737 | . . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ ((1 /
((1 / (abs‘𝐴))
− 1)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((1 /
((1 / (abs‘𝐴))
− 1)) / 𝑛)) | 
| 43 |  | ovex 7464 | . . . . . . 7
⊢ ((1 / ((1
/ (abs‘𝐴)) −
1)) / 𝑘) ∈
V | 
| 44 | 41, 42, 43 | fvmpt 7016 | . . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((1 /
((1 / (abs‘𝐴))
− 1)) / 𝑛))‘𝑘) = ((1 / ((1 / (abs‘𝐴)) − 1)) / 𝑘)) | 
| 45 | 44 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑛))‘𝑘) = ((1 / ((1 / (abs‘𝐴)) − 1)) / 𝑘)) | 
| 46 | 34 | rpred 13077 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (1 / ((1 / (abs‘𝐴)) − 1)) ∈
ℝ) | 
| 47 |  | nndivre 12307 | . . . . . 6
⊢ (((1 /
((1 / (abs‘𝐴))
− 1)) ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑘) ∈
ℝ) | 
| 48 | 46, 47 | sylan 580 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑘) ∈
ℝ) | 
| 49 | 45, 48 | eqeltrd 2841 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑛))‘𝑘) ∈
ℝ) | 
| 50 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → ((abs‘𝐴)↑𝑛) = ((abs‘𝐴)↑𝑘)) | 
| 51 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
((abs‘𝐴)↑𝑛)) = (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) | 
| 52 |  | ovex 7464 | . . . . . . . 8
⊢
((abs‘𝐴)↑𝑘) ∈ V | 
| 53 | 50, 51, 52 | fvmpt 7016 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) | 
| 54 | 53 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) | 
| 55 |  | nnz 12634 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) | 
| 56 |  | rpexpcl 14121 | . . . . . . 7
⊢
(((abs‘𝐴)
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((abs‘𝐴)↑𝑘) ∈
ℝ+) | 
| 57 | 25, 55, 56 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴)↑𝑘) ∈
ℝ+) | 
| 58 | 54, 57 | eqeltrd 2841 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) ∈
ℝ+) | 
| 59 | 58 | rpred 13077 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) ∈ ℝ) | 
| 60 |  | nnrp 13046 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) | 
| 61 |  | rpmulcl 13058 | . . . . . . . 8
⊢ ((((1 /
(abs‘𝐴)) − 1)
∈ ℝ+ ∧ 𝑘 ∈ ℝ+) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ∈
ℝ+) | 
| 62 | 33, 60, 61 | syl2an 596 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ∈
ℝ+) | 
| 63 | 62 | rpred 13077 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ∈
ℝ) | 
| 64 |  | peano2re 11434 | . . . . . . . . . 10
⊢ ((((1 /
(abs‘𝐴)) − 1)
· 𝑘) ∈ ℝ
→ ((((1 / (abs‘𝐴)) − 1) · 𝑘) + 1) ∈ ℝ) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((((1 /
(abs‘𝐴)) − 1)
· 𝑘) + 1) ∈
ℝ) | 
| 66 |  | rpexpcl 14121 | . . . . . . . . . . 11
⊢ (((1 /
(abs‘𝐴)) ∈
ℝ+ ∧ 𝑘
∈ ℤ) → ((1 / (abs‘𝐴))↑𝑘) ∈
ℝ+) | 
| 67 | 29, 55, 66 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((1 /
(abs‘𝐴))↑𝑘) ∈
ℝ+) | 
| 68 | 67 | rpred 13077 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((1 /
(abs‘𝐴))↑𝑘) ∈
ℝ) | 
| 69 | 63 | lep1d 12199 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ≤ ((((1 /
(abs‘𝐴)) − 1)
· 𝑘) +
1)) | 
| 70 | 30 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (1 / (abs‘𝐴)) ∈
ℝ) | 
| 71 | 7 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) | 
| 72 | 29 | rpge0d 13081 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 0 ≤ (1 / (abs‘𝐴))) | 
| 73 | 72 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 /
(abs‘𝐴))) | 
| 74 |  | bernneq2 14269 | . . . . . . . . . 10
⊢ (((1 /
(abs‘𝐴)) ∈
ℝ ∧ 𝑘 ∈
ℕ0 ∧ 0 ≤ (1 / (abs‘𝐴))) → ((((1 / (abs‘𝐴)) − 1) · 𝑘) + 1) ≤ ((1 /
(abs‘𝐴))↑𝑘)) | 
| 75 | 70, 71, 73, 74 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((((1 /
(abs‘𝐴)) − 1)
· 𝑘) + 1) ≤ ((1 /
(abs‘𝐴))↑𝑘)) | 
| 76 | 63, 65, 68, 69, 75 | letrd 11418 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ≤ ((1 /
(abs‘𝐴))↑𝑘)) | 
| 77 | 25 | rpcnne0d 13086 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((abs‘𝐴) ∈ ℂ ∧
(abs‘𝐴) ≠
0)) | 
| 78 |  | exprec 14144 | . . . . . . . . . 10
⊢
(((abs‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ≠ 0 ∧ 𝑘 ∈ ℤ) → ((1 /
(abs‘𝐴))↑𝑘) = (1 / ((abs‘𝐴)↑𝑘))) | 
| 79 | 78 | 3expa 1119 | . . . . . . . . 9
⊢
((((abs‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ≠ 0) ∧ 𝑘 ∈ ℤ) → ((1 /
(abs‘𝐴))↑𝑘) = (1 / ((abs‘𝐴)↑𝑘))) | 
| 80 | 77, 55, 79 | syl2an 596 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((1 /
(abs‘𝐴))↑𝑘) = (1 / ((abs‘𝐴)↑𝑘))) | 
| 81 | 76, 80 | breqtrd 5169 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → (((1 /
(abs‘𝐴)) − 1)
· 𝑘) ≤ (1 /
((abs‘𝐴)↑𝑘))) | 
| 82 | 62, 57, 81 | lerec2d 13098 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴)↑𝑘) ≤ (1 / (((1 / (abs‘𝐴)) − 1) · 𝑘))) | 
| 83 | 33 | rpcnne0d 13086 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (((1 / (abs‘𝐴)) − 1) ∈ ℂ
∧ ((1 / (abs‘𝐴))
− 1) ≠ 0)) | 
| 84 |  | nncn 12274 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 85 |  | nnne0 12300 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) | 
| 86 | 84, 85 | jca 511 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) | 
| 87 |  | recdiv2 11980 | . . . . . . 7
⊢ (((((1 /
(abs‘𝐴)) − 1)
∈ ℂ ∧ ((1 / (abs‘𝐴)) − 1) ≠ 0) ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) → ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑘) = (1 / (((1 /
(abs‘𝐴)) − 1)
· 𝑘))) | 
| 88 | 83, 86, 87 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑘) = (1 / (((1 /
(abs‘𝐴)) − 1)
· 𝑘))) | 
| 89 | 82, 88 | breqtrrd 5171 | . . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴)↑𝑘) ≤ ((1 / ((1 / (abs‘𝐴)) − 1)) / 𝑘)) | 
| 90 | 89, 54, 45 | 3brtr4d 5175 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ ((1 / ((1 /
(abs‘𝐴)) − 1))
/ 𝑛))‘𝑘)) | 
| 91 | 58 | rpge0d 13081 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦
((abs‘𝐴)↑𝑛))‘𝑘)) | 
| 92 | 1, 20, 37, 40, 49, 59, 90, 91 | climsqz2 15678 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) ⇝ 0) | 
| 93 |  | 1zzd 12648 | . . . . 5
⊢ (𝜑 → 1 ∈
ℤ) | 
| 94 | 4 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ∈ V) | 
| 95 | 39 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) ∈ V) | 
| 96 | 7 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) | 
| 97 | 96, 11 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) | 
| 98 |  | expcl 14120 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) | 
| 99 | 23, 7, 98 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) ∈ ℂ) | 
| 100 | 97, 99 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) ∈ ℂ) | 
| 101 |  | absexp 15343 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) | 
| 102 | 23, 7, 101 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) | 
| 103 | 97 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑘)) = (abs‘(𝐴↑𝑘))) | 
| 104 | 53 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) | 
| 105 | 102, 103,
104 | 3eqtr4rd 2788 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = (abs‘((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘))) | 
| 106 | 1, 93, 94, 95, 100, 105 | climabs0 15621 | . . . 4
⊢ (𝜑 → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0 ↔ (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) ⇝ 0)) | 
| 107 | 106 | biimpar 477 | . . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ↦ ((abs‘𝐴)↑𝑛)) ⇝ 0) → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) | 
| 108 | 92, 107 | syldan 591 | . 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) | 
| 109 | 19, 108 | pm2.61dane 3029 | 1
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |