Theorem lgam1

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

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

Proof

Step	Hyp	Ref	Expression
1		peano2nn	$$⊢m\in \mathbb{N}\to m+1\in \mathbb{N}$$
2	1	nnrpd	$$⊢m\in \mathbb{N}\to m+1\in {ℝ}^{+}$$
3		nnrp	$$⊢m\in \mathbb{N}\to m\in {ℝ}^{+}$$
4	2 3	rpdivcld	$$⊢m\in \mathbb{N}\to \frac{m+1}{m}\in {ℝ}^{+}$$
5	4	relogcld	$$⊢m\in \mathbb{N}\to \log \left(\frac{m+1}{m}\right)\in ℝ$$
6	5	recnd	$$⊢m\in \mathbb{N}\to \log \left(\frac{m+1}{m}\right)\in ℂ$$
7	6	mulid2d	$$⊢m\in \mathbb{N}\to 1\log \left(\frac{m+1}{m}\right)=\log \left(\frac{m+1}{m}\right)$$
8		nncn	$$⊢m\in \mathbb{N}\to m\in ℂ$$
9		nnne0	$$⊢m\in \mathbb{N}\to m\ne 0$$
10	8 9	dividd	$$⊢m\in \mathbb{N}\to \frac{m}{m}=1$$
11	10	oveq1d	$$⊢m\in \mathbb{N}\to \left(\frac{m}{m}\right)+\left(\frac{1}{m}\right)=1+\left(\frac{1}{m}\right)$$
12		1cnd	$$⊢m\in \mathbb{N}\to 1\in ℂ$$
13	8 12 8 9	divdird	$$⊢m\in \mathbb{N}\to \frac{m+1}{m}=\left(\frac{m}{m}\right)+\left(\frac{1}{m}\right)$$
14	8 9	reccld	$$⊢m\in \mathbb{N}\to \frac{1}{m}\in ℂ$$
15	14 12	addcomd	$$⊢m\in \mathbb{N}\to \left(\frac{1}{m}\right)+1=1+\left(\frac{1}{m}\right)$$
16	11 13 15	3eqtr4rd	$$⊢m\in \mathbb{N}\to \left(\frac{1}{m}\right)+1=\frac{m+1}{m}$$
17	16	fveq2d	$$⊢m\in \mathbb{N}\to \log \left(\left(\frac{1}{m}\right)+1\right)=\log \left(\frac{m+1}{m}\right)$$
18	7 17	oveq12d	$$⊢m\in \mathbb{N}\to 1\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{1}{m}\right)+1\right)=\log \left(\frac{m+1}{m}\right)-\log \left(\frac{m+1}{m}\right)$$
19	6	subidd	$$⊢m\in \mathbb{N}\to \log \left(\frac{m+1}{m}\right)-\log \left(\frac{m+1}{m}\right)=0$$
20	18 19	eqtrd	$$⊢m\in \mathbb{N}\to 1\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{1}{m}\right)+1\right)=0$$
21	20	mpteq2ia	$$⊢\left(m\in \mathbb{N}⟼1\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{1}{m}\right)+1\right)\right)=\left(m\in \mathbb{N}⟼0\right)$$
22		fconstmpt	$$⊢\mathbb{N}\times \left\{0\right\}=\left(m\in \mathbb{N}⟼0\right)$$
23		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
24	23	xpeq1i	$$⊢\mathbb{N}\times \left\{0\right\}={\mathbb{Z}}_{\ge 1}\times \left\{0\right\}$$
25	21 22 24	3eqtr2ri	$$⊢{\mathbb{Z}}_{\ge 1}\times \left\{0\right\}=\left(m\in \mathbb{N}⟼1\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{1}{m}\right)+1\right)\right)$$
26		ax-1cn	$$⊢1\in ℂ$$
27		1nn	$$⊢1\in \mathbb{N}$$
28		eldifn	$$⊢1\in \left(\mathbb{Z}\setminus \mathbb{N}\right)\to \neg 1\in \mathbb{N}$$
29	27 28	mt2	$$⊢\neg 1\in \left(\mathbb{Z}\setminus \mathbb{N}\right)$$
30		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)$$
31	26 29 30	mpbir2an	$$⊢1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
32	31	a1i	$$⊢\top \to 1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
33	25 32	lgamcvg	$$⊢\top \to seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝\left(\log \mathrm{\Gamma }\left(1\right)+\log 1\right)$$
34	33	mptru	$$⊢seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝\left(\log \mathrm{\Gamma }\left(1\right)+\log 1\right)$$
35		log1	$$⊢\log 1=0$$
36	35	oveq2i	$$⊢\log \mathrm{\Gamma }\left(1\right)+\log 1=\log \mathrm{\Gamma }\left(1\right)+0$$
37		lgamcl	$$⊢1\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \log \mathrm{\Gamma }\left(1\right)\in ℂ$$
38	31 37	ax-mp	$$⊢\log \mathrm{\Gamma }\left(1\right)\in ℂ$$
39	38	addid1i	$$⊢\log \mathrm{\Gamma }\left(1\right)+0=\log \mathrm{\Gamma }\left(1\right)$$
40	36 39	eqtri	$$⊢\log \mathrm{\Gamma }\left(1\right)+\log 1=\log \mathrm{\Gamma }\left(1\right)$$
41	34 40	breqtri	$$⊢seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝\log \mathrm{\Gamma }\left(1\right)$$
42		1z	$$⊢1\in \mathbb{Z}$$
43		serclim0	$$⊢1\in \mathbb{Z}\to seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0$$
44	42 43	ax-mp	$$⊢seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0$$
45		climuni	$$⊢\left(seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝\log \mathrm{\Gamma }\left(1\right)\wedge seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0\right)\to \log \mathrm{\Gamma }\left(1\right)=0$$
46	41 44 45	mp2an	$$⊢\log \mathrm{\Gamma }\left(1\right)=0$$