Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Gamma function
igamcl
Next ⟩
gamigam
Metamath Proof Explorer
Ascii
Unicode
Theorem
igamcl
Description:
Closure of the inverse Gamma function.
(Contributed by
Mario Carneiro
, 16-Jul-2017)
Ref
Expression
Assertion
igamcl
⊢
A
∈
ℂ
→
1
Γ
⁡
A
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
igamval
⊢
A
∈
ℂ
→
1
Γ
⁡
A
=
if
A
∈
ℤ
∖
ℕ
0
1
Γ
⁡
A
2
0cnd
⊢
A
∈
ℂ
∧
A
∈
ℤ
∖
ℕ
→
0
∈
ℂ
3
eldif
⊢
A
∈
ℂ
∖
ℤ
∖
ℕ
↔
A
∈
ℂ
∧
¬
A
∈
ℤ
∖
ℕ
4
gamcl
⊢
A
∈
ℂ
∖
ℤ
∖
ℕ
→
Γ
⁡
A
∈
ℂ
5
gamne0
⊢
A
∈
ℂ
∖
ℤ
∖
ℕ
→
Γ
⁡
A
≠
0
6
4
5
reccld
⊢
A
∈
ℂ
∖
ℤ
∖
ℕ
→
1
Γ
⁡
A
∈
ℂ
7
3
6
sylbir
⊢
A
∈
ℂ
∧
¬
A
∈
ℤ
∖
ℕ
→
1
Γ
⁡
A
∈
ℂ
8
2
7
ifclda
⊢
A
∈
ℂ
→
if
A
∈
ℤ
∖
ℕ
0
1
Γ
⁡
A
∈
ℂ
9
1
8
eqeltrd
⊢
A
∈
ℂ
→
1
Γ
⁡
A
∈
ℂ