Theorem lgamcvg

Description: The series G converges to log_G ( A ) + log ( A ) . (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Hypotheses	lgamcvg.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
	lgamcvg.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion	lgamcvg	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
2		lgamcvg.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		eqid	⊢ { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑦 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑦 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑦 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑦 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
4	3 2 1	lgamcvglem	⊢ ( 𝜑 → ( ( log Γ ‘ 𝐴 ) ∈ ℂ ∧ seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ) )
5	4	simprd	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )