Theorem gam1

Description: The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	gam1	$$⊢\mathrm{\Gamma }\left(1\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		lgam1	$$⊢\log \mathrm{\Gamma }\left(1\right)=0$$
2	1	fveq2i	$$⊢{\mathrm{e}}^{\log \mathrm{\Gamma }\left(1\right)}={\mathrm{e}}^0$$
3		ax-1cn	$$⊢1\in ℂ$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		eldifn	$$⊢1\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\to \neg 1\in \mathbb{N}$$
6	4 5	mt2	$$⊢\neg 1\in \left(\mathbb{Z}\setminus \mathbb{N}\right)$$
7		eldif	$$⊢1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\leftrightarrow \left(1\in ℂ\wedge \neg 1\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
8	3 6 7	mpbir2an	$$⊢1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
9		eflgam	$$⊢1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to {\mathrm{e}}^{\log \mathrm{\Gamma }\left(1\right)}=\mathrm{\Gamma }\left(1\right)$$
10	8 9	ax-mp	$$⊢{\mathrm{e}}^{\log \mathrm{\Gamma }\left(1\right)}=\mathrm{\Gamma }\left(1\right)$$
11		ef0	$$⊢{\mathrm{e}}^0=1$$
12	2 10 11	3eqtr3i	$$⊢\mathrm{\Gamma }\left(1\right)=1$$