Theorem igamval

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

	Ref	Expression
Assertion	igamval	⊢ ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( ℤ ∖ ℕ ) ↔ 𝐴 ∈ ( ℤ ∖ ℕ ) ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( Γ ‘ 𝑥 ) = ( Γ ‘ 𝐴 ) )
3	2	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 1 / ( Γ ‘ 𝑥 ) ) = ( 1 / ( Γ ‘ 𝐴 ) ) )
4	1 3	ifbieq2d	⊢ ( 𝑥 = 𝐴 → if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )
5		df-igam	⊢ 1/Γ = ( 𝑥 ∈ ℂ ↦ if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) ) )
6		c0ex	⊢ 0 ∈ V
7		ovex	⊢ ( 1 / ( Γ ‘ 𝐴 ) ) ∈ V
8	6 7	ifex	⊢ if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) ∈ V
9	4 5 8	fvmpt	⊢ ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )