Theorem igamz

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

	Ref	Expression
Assertion	igamz	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → ( 1/Γ ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → 𝐴 ∈ ℤ )
2	1	zcnd	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → 𝐴 ∈ ℂ )
3		igamval	⊢ ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )
4	2 3	syl	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )
5		iftrue	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) = 0 )
6	4 5	eqtrd	⊢ ( 𝐴 ∈ ( ℤ ∖ ℕ ) → ( 1/Γ ‘ 𝐴 ) = 0 )