Metamath Proof Explorer


Theorem igamcl

Description: Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)

Ref Expression
Assertion igamcl ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 igamval ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) = if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) )
2 0cnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ( ℤ ∖ ℕ ) ) → 0 ∈ ℂ )
3 eldif ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( ℤ ∖ ℕ ) ) )
4 gamcl ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ )
5 gamne0 ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ≠ 0 )
6 4 5 reccld ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( 1 / ( Γ ‘ 𝐴 ) ) ∈ ℂ )
7 3 6 sylbir ( ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( ℤ ∖ ℕ ) ) → ( 1 / ( Γ ‘ 𝐴 ) ) ∈ ℂ )
8 2 7 ifclda ( 𝐴 ∈ ℂ → if ( 𝐴 ∈ ( ℤ ∖ ℕ ) , 0 , ( 1 / ( Γ ‘ 𝐴 ) ) ) ∈ ℂ )
9 1 8 eqeltrd ( 𝐴 ∈ ℂ → ( 1/Γ ‘ 𝐴 ) ∈ ℂ )