Theorem gamne0

Description: The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	gamne0	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		eflgam	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )
2		lgamcl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ )
3		efne0	⊢ ( ( log Γ ‘ 𝐴 ) ∈ ℂ → ( exp ‘ ( log Γ ‘ 𝐴 ) ) ≠ 0 )
4	2 3	syl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) ≠ 0 )
5	1 4	eqnetrrd	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ≠ 0 )