This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ ( 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 − 𝐴 ) ) )