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 \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ} (\frac{A^{k}}{k}) = - \log (1 - A)$

Step	Hyp	Ref	Expression
1		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
2		1zzd	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℤ$
3		oveq2	$⊢ n = k \to A^{n} = A^{k}$
4		id	$⊢ n = k \to n = k$
5	3 4	oveq12d	$⊢ n = k \to \frac{A^{n}}{n} = \frac{A^{k}}{k}$
6		eqid	$⊢ (n \in ℕ ⟼ \frac{A^{n}}{n}) = (n \in ℕ ⟼ \frac{A^{n}}{n})$
7		ovex	$⊢ \frac{A^{k}}{k} \in V$
8	5 6 7	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{A^{n}}{n}) (k) = \frac{A^{k}}{k}$
9	8	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{A^{n}}{n}) (k) = \frac{A^{k}}{k}$
10		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
11		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
12		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
13	10 11 12	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to A^{k} \in ℂ$
14		nncn	$⊢ k \in ℕ \to k \in ℂ$
15	14	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \in ℂ$
16		nnne0	$⊢ k \in ℕ \to k \neq 0$
17	16	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \neq 0$
18	13 15 17	divcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to \frac{A^{k}}{k} \in ℂ$
19		logtayl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{A^{n}}{n})) ⇝ (- \log (1 - A))$
20	1 2 9 18 19	isumclim	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ} (\frac{A^{k}}{k}) = - \log (1 - A)$

Metamath Proof Explorer