Definition df-igam

Description: Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017)

	Ref	Expression
Assertion	df-igam	⊢ 1/Γ = ( 𝑥 ∈ ℂ ↦ if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cigam	⊢ 1/Γ
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3	1	cv	⊢ 𝑥
4		cz	⊢ ℤ
5		cn	⊢ ℕ
6	4 5	cdif	⊢ ( ℤ ∖ ℕ )
7	3 6	wcel	⊢ 𝑥 ∈ ( ℤ ∖ ℕ )
8		cc0	⊢ 0
9		c1	⊢ 1
10		cdiv	⊢ /
11		cgam	⊢ Γ
12	3 11	cfv	⊢ ( Γ ‘ 𝑥 )
13	9 12 10	co	⊢ ( 1 / ( Γ ‘ 𝑥 ) )
14	7 8 13	cif	⊢ if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) ) )
16	0 15	wceq	⊢ 1/Γ = ( 𝑥 ∈ ℂ ↦ if ( 𝑥 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝑥 ) ) ) )