Metamath Proof Explorer


Theorem igamcl

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

Ref Expression
Assertion igamcl A1ΓA

Proof

Step Hyp Ref Expression
1 igamval A1ΓA=ifA01ΓA
2 0cnd AA0
3 eldif AA¬A
4 gamcl AΓA
5 gamne0 AΓA0
6 4 5 reccld A1ΓA
7 3 6 sylbir A¬A1ΓA
8 2 7 ifclda AifA01ΓA
9 1 8 eqeltrd A1ΓA