Metamath Proof Explorer

Theorem igamz

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

Ref Expression
Assertion igamz ⊢ A ∈ ℤ ∖ ℕ → 1 Γ ⁡ A = 0

Proof

Step Hyp Ref Expression
1 eldifi ⊢ A ∈ ℤ ∖ ℕ → A ∈ ℤ
2 1 zcnd ⊢ A ∈ ℤ ∖ ℕ → A ∈ ℂ
3 igamval ⊢ A ∈ ℂ → 1 Γ ⁡ A = if A ∈ ℤ ∖ ℕ 0 1 Γ ⁡ A
4 2 3 syl ⊢ A ∈ ℤ ∖ ℕ → 1 Γ ⁡ A = if A ∈ ℤ ∖ ℕ 0 1 Γ ⁡ A
5 iftrue ⊢ A ∈ ℤ ∖ ℕ → if A ∈ ℤ ∖ ℕ 0 1 Γ ⁡ A = 0
6 4 5 eqtrd ⊢ A ∈ ℤ ∖ ℕ → 1 Γ ⁡ A = 0