Theorem gamf

Description: The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Assertion	gamf	⊢ Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		eff	⊢ exp : ℂ ⟶ ℂ
2		lgamf	⊢ log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ
3		fco	⊢ ( ( exp : ℂ ⟶ ℂ ∧ log Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ ) → ( exp ∘ log Γ ) : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ )
4	1 2 3	mp2an	⊢ ( exp ∘ log Γ ) : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ
5		df-gam	⊢ Γ = ( exp ∘ log Γ )
6	5	feq1i	⊢ ( Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ ↔ ( exp ∘ log Γ ) : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ )
7	4 6	mpbir	⊢ Γ : ( ℂ ∖ ( ℤ ∖ ℕ ) ) ⟶ ℂ