Theorem gamne0

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

	Ref	Expression
Assertion	gamne0	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) =/= 0 )

Proof

Step	Hyp	Ref	Expression
1		eflgam	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
2		lgamcl	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )
3		efne0	|- ( ( log_G ` A ) e. CC -> ( exp ` ( log_G ` A ) ) =/= 0 )
4	2 3	syl	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) =/= 0 )
5	1 4	eqnetrrd	|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) =/= 0 )