Metamath Proof Explorer

Theorem gamcvg2

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

Ref Expression
Hypotheses gamcvg2.f ⊢ F = m ∈ ℕ ⟼ m + 1 m A A m + 1
gamcvg2.a ⊢ φ → A ∈ ℂ ∖ ℤ ∖ ℕ
Assertion gamcvg2 ⊢ φ → seq 1 × F ⇝ Γ ⁡ A ⁢ A

Proof

Step Hyp Ref Expression
1 gamcvg2.f ⊢ F = m ∈ ℕ ⟼ m + 1 m A A m + 1
2 gamcvg2.a ⊢ φ → A ∈ ℂ ∖ ℤ ∖ ℕ
3 eqid ⊢ m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 = m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1
4 1 2 3 gamcvg2lem ⊢ φ → exp ∘ seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 = seq 1 × F
5 3 2 gamcvg ⊢ φ → exp ∘ seq 1 + m ∈ ℕ ⟼ A ⁢ log ⁡ m + 1 m − log ⁡ A m + 1 ⇝ Γ ⁡ A ⁢ A
6 4 5 eqbrtrrd ⊢ φ → seq 1 × F ⇝ Γ ⁡ A ⁢ A