Theorem igamz

Description: Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eldifi	|- ( A e. ( ZZ \ NN ) -> A e. ZZ )
2	1	zcnd	|- ( A e. ( ZZ \ NN ) -> A e. CC )
3		igamval	|- ( A e. CC -> ( 1/_G ` A ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) )
4	2 3	syl	|- ( A e. ( ZZ \ NN ) -> ( 1/_G ` A ) = if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) )
5		iftrue	|- ( A e. ( ZZ \ NN ) -> if ( A e. ( ZZ \ NN ) , 0 , ( 1 / ( _G ` A ) ) ) = 0 )
6	4 5	eqtrd	|- ( A e. ( ZZ \ NN ) -> ( 1/_G ` A ) = 0 )