Theorem lgam1

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

	Ref	Expression
Assertion	lgam1	⊢ ( log Γ ‘ 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		peano2nn	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
2	1	nnrpd	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℝ+ )
3		nnrp	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
4	2 3	rpdivcld	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ+ )
5	4	relogcld	⊢ ( 𝑚 ∈ ℕ → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℝ )
6	5	recnd	⊢ ( 𝑚 ∈ ℕ → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℂ )
7	6	mulid2d	⊢ ( 𝑚 ∈ ℕ → ( 1 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) )
8		nncn	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
9		nnne0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
10	8 9	dividd	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 / 𝑚 ) = 1 )
11	10	oveq1d	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 / 𝑚 ) + ( 1 / 𝑚 ) ) = ( 1 + ( 1 / 𝑚 ) ) )
12		1cnd	⊢ ( 𝑚 ∈ ℕ → 1 ∈ ℂ )
13	8 12 8 9	divdird	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑚 / 𝑚 ) + ( 1 / 𝑚 ) ) )
14	8 9	reccld	⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℂ )
15	14 12	addcomd	⊢ ( 𝑚 ∈ ℕ → ( ( 1 / 𝑚 ) + 1 ) = ( 1 + ( 1 / 𝑚 ) ) )
16	11 13 15	3eqtr4rd	⊢ ( 𝑚 ∈ ℕ → ( ( 1 / 𝑚 ) + 1 ) = ( ( 𝑚 + 1 ) / 𝑚 ) )
17	16	fveq2d	⊢ ( 𝑚 ∈ ℕ → ( log ‘ ( ( 1 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) )
18	7 17	oveq12d	⊢ ( 𝑚 ∈ ℕ → ( ( 1 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 1 / 𝑚 ) + 1 ) ) ) = ( ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) − ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) )
19	6	subidd	⊢ ( 𝑚 ∈ ℕ → ( ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) − ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = 0 )
20	18 19	eqtrd	⊢ ( 𝑚 ∈ ℕ → ( ( 1 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 1 / 𝑚 ) + 1 ) ) ) = 0 )
21	20	mpteq2ia	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 1 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 1 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ 0 )
22		fconstmpt	⊢ ( ℕ × { 0 } ) = ( 𝑚 ∈ ℕ ↦ 0 )
23		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
24	23	xpeq1i	⊢ ( ℕ × { 0 } ) = ( ( ℤ≥ ‘ 1 ) × { 0 } )
25	21 22 24	3eqtr2ri	⊢ ( ( ℤ≥ ‘ 1 ) × { 0 } ) = ( 𝑚 ∈ ℕ ↦ ( ( 1 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 1 / 𝑚 ) + 1 ) ) ) )
26		ax-1cn	⊢ 1 ∈ ℂ
27		1nn	⊢ 1 ∈ ℕ
28		eldifn	⊢ ( 1 ∈ ( ℤ ∖ ℕ ) → ¬ 1 ∈ ℕ )
29	27 28	mt2	⊢ ¬ 1 ∈ ( ℤ ∖ ℕ )
30		eldif	⊢ ( 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 1 ∈ ℂ ∧ ¬ 1 ∈ ( ℤ ∖ ℕ ) ) )
31	26 29 30	mpbir2an	⊢ 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) )
32	31	a1i	⊢ ( ⊤ → 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
33	25 32	lgamcvg	⊢ ( ⊤ → seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ ( ( log Γ ‘ 1 ) + ( log ‘ 1 ) ) )
34	33	mptru	⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ ( ( log Γ ‘ 1 ) + ( log ‘ 1 ) )
35		log1	⊢ ( log ‘ 1 ) = 0
36	35	oveq2i	⊢ ( ( log Γ ‘ 1 ) + ( log ‘ 1 ) ) = ( ( log Γ ‘ 1 ) + 0 )
37		lgamcl	⊢ ( 1 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 1 ) ∈ ℂ )
38	31 37	ax-mp	⊢ ( log Γ ‘ 1 ) ∈ ℂ
39	38	addid1i	⊢ ( ( log Γ ‘ 1 ) + 0 ) = ( log Γ ‘ 1 )
40	36 39	eqtri	⊢ ( ( log Γ ‘ 1 ) + ( log ‘ 1 ) ) = ( log Γ ‘ 1 )
41	34 40	breqtri	⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ ( log Γ ‘ 1 )
42		1z	⊢ 1 ∈ ℤ
43		serclim0	⊢ ( 1 ∈ ℤ → seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0 )
44	42 43	ax-mp	⊢ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0
45		climuni	⊢ ( ( seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ ( log Γ ‘ 1 ) ∧ seq 1 ( + , ( ( ℤ≥ ‘ 1 ) × { 0 } ) ) ⇝ 0 ) → ( log Γ ‘ 1 ) = 0 )
46	41 44 45	mp2an	⊢ ( log Γ ‘ 1 ) = 0