Theorem igamf

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

	Ref	Expression
Assertion	igamf	⊢ 1/Γ : ℂ ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-igam	⊢ 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	fmpti	⊢ 1/Γ : ℂ ⟶ ℂ