Metamath Proof Explorer

Theorem logtaylsum

Description: The Taylor series for -u log ( 1 - A ) , as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion logtaylsum ⊢ A ∈ ℂ ∧ A < 1 → ∑ k ∈ ℕ A k k = − log ⁡ 1 − A

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1zzd ⊢ A ∈ ℂ ∧ A < 1 → 1 ∈ ℤ
3 oveq2 ⊢ n = k → A n = A k
4 id ⊢ n = k → n = k
5 3 4 oveq12d ⊢ n = k → A n n = A k k
6 eqid ⊢ n ∈ ℕ ⟼ A n n = n ∈ ℕ ⟼ A n n
7 ovex ⊢ A k k ∈ V
8 5 6 7 fvmpt ⊢ k ∈ ℕ → n ∈ ℕ ⟼ A n n ⁡ k = A k k
9 8 adantl ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → n ∈ ℕ ⟼ A n n ⁡ k = A k k
10 simpl ⊢ A ∈ ℂ ∧ A < 1 → A ∈ ℂ
11 nnnn0 ⊢ k ∈ ℕ → k ∈ ℕ 0
12 expcl ⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → A k ∈ ℂ
13 10 11 12 syl2an ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → A k ∈ ℂ
14 nncn ⊢ k ∈ ℕ → k ∈ ℂ
15 14 adantl ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → k ∈ ℂ
16 nnne0 ⊢ k ∈ ℕ → k ≠ 0
17 16 adantl ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → k ≠ 0
18 13 15 17 divcld ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → A k k ∈ ℂ
19 logtayl ⊢ A ∈ ℂ ∧ A < 1 → seq 1 + n ∈ ℕ ⟼ A n n ⇝ − log ⁡ 1 − A
20 1 2 9 18 19 isumclim ⊢ A ∈ ℂ ∧ A < 1 → ∑ k ∈ ℕ A k k = − log ⁡ 1 − A