Theorem gam1

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

	Ref	Expression
Assertion	gam1	⊢ ( Γ ‘ 1 ) = 1

Proof

Step	Hyp	Ref	Expression
1		lgam1	⊢ ( log Γ ‘ 1 ) = 0
2	1	fveq2i	⊢ ( exp ‘ ( log Γ ‘ 1 ) ) = ( exp ‘ 0 )
3		ax-1cn	⊢ 1 ∈ ℂ
4		1nn	⊢ 1 ∈ ℕ
5		eldifn	⊢ ( 1 ∈ ( ℤ ∖ ℕ ) → ¬ 1 ∈ ℕ )
6	4 5	mt2	⊢ ¬ 1 ∈ ( ℤ ∖ ℕ )
7		eldif	⊢ ( 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 1 ∈ ℂ ∧ ¬ 1 ∈ ( ℤ ∖ ℕ ) ) )
8	3 6 7	mpbir2an	⊢ 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) )
9		eflgam	⊢ ( 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 1 ) ) = ( Γ ‘ 1 ) )
10	8 9	ax-mp	⊢ ( exp ‘ ( log Γ ‘ 1 ) ) = ( Γ ‘ 1 )
11		ef0	⊢ ( exp ‘ 0 ) = 1
12	2 10 11	3eqtr3i	⊢ ( Γ ‘ 1 ) = 1