Theorem gamcvg2

Description: An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	gamcvg2.f	⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) )
	gamcvg2.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
Assertion	gamcvg2	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		gamcvg2.f	⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) )
2		gamcvg2.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
3		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
4	1 2 3	gamcvg2lem	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ) = seq 1 ( · , 𝐹 ) )
5	3 2	gamcvg	⊢ ( 𝜑 → ( exp ∘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )
6	4 5	eqbrtrrd	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )