Description: Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | igamcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | igamval | |
|
2 | 0cnd | |
|
3 | eldif | |
|
4 | gamcl | |
|
5 | gamne0 | |
|
6 | 4 5 | reccld | |
7 | 3 6 | sylbir | |
8 | 2 7 | ifclda | |
9 | 1 8 | eqeltrd | |