Metamath Proof Explorer


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