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	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) = - ( log ‘ ( 1 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
2		1zzd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℤ )
3		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
4		id	⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
5	3 4	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) = ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) )
6		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) )
7		ovex	⊢ ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ∈ V
8	5 6 7	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) )
9	8	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) )
10		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
11		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
12		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
13	10 11 12	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
14		nncn	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
15	14	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
16		nnne0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
18	13 15 17	divcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ∈ ℂ )
19		logtayl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ) ) ⇝ - ( log ‘ ( 1 − 𝐴 ) ) )
20	1 2 9 18 19	isumclim	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) = - ( log ‘ ( 1 − 𝐴 ) ) )