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 25590
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 25587 . 2 class 1/Γ
2 vx . . 3 setvar 𝑥
3 cc 10527 . . 3 class
42cv 1529 . . . . 5 class 𝑥
5 cz 11973 . . . . . 6 class
6 cn 11630 . . . . . 6 class
75, 6cdif 3931 . . . . 5 class (ℤ ∖ ℕ)
84, 7wcel 2107 . . . 4 wff 𝑥 ∈ (ℤ ∖ ℕ)
9 cc0 10529 . . . 4 class 0
10 c1 10530 . . . . 5 class 1
11 cgam 25586 . . . . . 6 class Γ
124, 11cfv 6348 . . . . 5 class (Γ‘𝑥)
13 cdiv 11289 . . . . 5 class /
1410, 12, 13co 7148 . . . 4 class (1 / (Γ‘𝑥))
158, 9, 14cif 4465 . . 3 class if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥)))
162, 3, 15cmpt 5137 . 2 class (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
171, 16wceq 1530 1 wff 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  igamval  25616  igamf  25620
  Copyright terms: Public domain W3C validator