Theorem gamigam

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

	Ref	Expression
Assertion	gamigam	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)=\frac{1}{\frac{1}{\mathrm{\Gamma }}\left(A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		igamgam	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \frac{1}{\mathrm{\Gamma }}\left(A\right)=\frac{1}{\mathrm{\Gamma }\left(A\right)}$$
2	1	oveq2d	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \frac{1}{\frac{1}{\mathrm{\Gamma }}\left(A\right)}=\frac{1}{\frac{1}{\mathrm{\Gamma }\left(A\right)}}$$
3		gamcl	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)\in ℂ$$
4		gamne0	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)\ne 0$$
5	3 4	recrecd	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \frac{1}{\frac{1}{\mathrm{\Gamma }\left(A\right)}}=\mathrm{\Gamma }\left(A\right)$$
6	2 5	eqtr2d	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \mathrm{\Gamma }\left(A\right)=\frac{1}{\frac{1}{\mathrm{\Gamma }}\left(A\right)}$$