MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-igam Structured version   Visualization version   GIF version

Definition df-igam 25525
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
StepHypRef Expression
1 cigam 25522 . 2 class 1/Γ
2 vx . . 3 setvar 𝑥
3 cc 10523 . . 3 class
42cv 1527 . . . . 5 class 𝑥
5 cz 11969 . . . . . 6 class
6 cn 11626 . . . . . 6 class
75, 6cdif 3930 . . . . 5 class (ℤ ∖ ℕ)
84, 7wcel 2105 . . . 4 wff 𝑥 ∈ (ℤ ∖ ℕ)
9 cc0 10525 . . . 4 class 0
10 c1 10526 . . . . 5 class 1
11 cgam 25521 . . . . . 6 class Γ
124, 11cfv 6348 . . . . 5 class (Γ‘𝑥)
13 cdiv 11285 . . . . 5 class /
1410, 12, 13co 7145 . . . 4 class (1 / (Γ‘𝑥))
158, 9, 14cif 4463 . . 3 class if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥)))
162, 3, 15cmpt 5137 . 2 class (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
171, 16wceq 1528 1 wff 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  igamval  25551  igamf  25555
  Copyright terms: Public domain W3C validator