Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Gamma function
igamf
Next ⟩
igamcl
Metamath Proof Explorer
Ascii
Unicode
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
Γ
=
x
∈
ℂ
⟼
if
x
∈
ℤ
∖
ℕ
0
1
Γ
⁡
x
2
0cnd
⊢
x
∈
ℂ
∧
x
∈
ℤ
∖
ℕ
→
0
∈
ℂ
3
eldif
⊢
x
∈
ℂ
∖
ℤ
∖
ℕ
↔
x
∈
ℂ
∧
¬
x
∈
ℤ
∖
ℕ
4
gamcl
⊢
x
∈
ℂ
∖
ℤ
∖
ℕ
→
Γ
⁡
x
∈
ℂ
5
gamne0
⊢
x
∈
ℂ
∖
ℤ
∖
ℕ
→
Γ
⁡
x
≠
0
6
4
5
reccld
⊢
x
∈
ℂ
∖
ℤ
∖
ℕ
→
1
Γ
⁡
x
∈
ℂ
7
3
6
sylbir
⊢
x
∈
ℂ
∧
¬
x
∈
ℤ
∖
ℕ
→
1
Γ
⁡
x
∈
ℂ
8
2
7
ifclda
⊢
x
∈
ℂ
→
if
x
∈
ℤ
∖
ℕ
0
1
Γ
⁡
x
∈
ℂ
9
1
8
fmpti
⊢
1
Γ
:
ℂ
⟶
ℂ