Definition df-igam 25601

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

Assertion

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

Detailed syntax breakdown of Definition df-igam

Step	Hyp	Ref	Expression
1		cigam 25598	. 2 class 1/Γ
2		vx	. . 3 setvar 𝑥
3		cc 10538	. . 3 class ℂ
4	2	cv 1535	. . . . 5 class 𝑥
5		cz 11984	. . . . . 6 class ℤ
6		cn 11641	. . . . . 6 class ℕ
7	5, 6	cdif 3936	. . . . 5 class (ℤ ∖ ℕ)
8	4, 7	wcel 2113	. . . 4 wff 𝑥 ∈ (ℤ ∖ ℕ)
9		cc0 10540	. . . 4 class 0
10		c1 10541	. . . . 5 class 1
11		cgam 25597	. . . . . 6 class Γ
12	4, 11	cfv 6358	. . . . 5 class (Γ‘𝑥)
13		cdiv 11300	. . . . 5 class /
14	10, 12, 13	co 7159	. . . 4 class (1 / (Γ‘𝑥))
15	8, 9, 14	cif 4470	. . 3 class if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥)))
16	2, 3, 15	cmpt 5149	. 2 class (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
17	1, 16	wceq 1536	1 wff 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))

This definition is referenced by:  igamval  25627  igamf  25631