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	$⊢ m \in ℕ \to m + 1 \in ℕ$
2	1	nnrpd	$⊢ m \in ℕ \to m + 1 \in ℝ^{+}$
3		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
4	2 3	rpdivcld	$⊢ m \in ℕ \to \frac{m + 1}{m} \in ℝ^{+}$
5	4	relogcld	$⊢ m \in ℕ \to \log (\frac{m + 1}{m}) \in ℝ$
6	5	recnd	$⊢ m \in ℕ \to \log (\frac{m + 1}{m}) \in ℂ$
7	6	mullidd	$⊢ m \in ℕ \to 1 \log (\frac{m + 1}{m}) = \log (\frac{m + 1}{m})$
8		nncn	$⊢ m \in ℕ \to m \in ℂ$
9		nnne0	$⊢ m \in ℕ \to m \neq 0$
10	8 9	dividd	$⊢ m \in ℕ \to \frac{m}{m} = 1$
11	10	oveq1d	$⊢ m \in ℕ \to (\frac{m}{m}) + (\frac{1}{m}) = 1 + (\frac{1}{m})$
12		1cnd	$⊢ m \in ℕ \to 1 \in ℂ$
13	8 12 8 9	divdird	$⊢ m \in ℕ \to \frac{m + 1}{m} = (\frac{m}{m}) + (\frac{1}{m})$
14	8 9	reccld	$⊢ m \in ℕ \to \frac{1}{m} \in ℂ$
15	14 12	addcomd	$⊢ m \in ℕ \to (\frac{1}{m}) + 1 = 1 + (\frac{1}{m})$
16	11 13 15	3eqtr4rd	$⊢ m \in ℕ \to (\frac{1}{m}) + 1 = \frac{m + 1}{m}$
17	16	fveq2d	$⊢ m \in ℕ \to \log ((\frac{1}{m}) + 1) = \log (\frac{m + 1}{m})$
18	7 17	oveq12d	$⊢ m \in ℕ \to 1 \log (\frac{m + 1}{m}) - \log ((\frac{1}{m}) + 1) = \log (\frac{m + 1}{m}) - \log (\frac{m + 1}{m})$
19	6	subidd	$⊢ m \in ℕ \to \log (\frac{m + 1}{m}) - \log (\frac{m + 1}{m}) = 0$
20	18 19	eqtrd	$⊢ m \in ℕ \to 1 \log (\frac{m + 1}{m}) - \log ((\frac{1}{m}) + 1) = 0$
21	20	mpteq2ia	$⊢ (m \in ℕ ⟼ 1 \log (\frac{m + 1}{m}) - \log ((\frac{1}{m}) + 1)) = (m \in ℕ ⟼ 0)$
22		fconstmpt	$⊢ ℕ \times \{0\} = (m \in ℕ ⟼ 0)$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	23	xpeq1i	$⊢ ℕ \times \{0\} = ℤ_{\geq 1} \times \{0\}$
25	21 22 24	3eqtr2ri	$⊢ ℤ_{\geq 1} \times \{0\} = (m \in ℕ ⟼ 1 \log (\frac{m + 1}{m}) - \log ((\frac{1}{m}) + 1))$
26		ax-1cn	$⊢ 1 \in ℂ$
27		1nn	$⊢ 1 \in ℕ$
28		eldifn	$⊢ 1 \in (ℤ ∖ ℕ) \to \neg 1 \in ℕ$
29	27 28	mt2	$⊢ \neg 1 \in (ℤ ∖ ℕ)$
30		eldif	$⊢ 1 \in (ℂ ∖ (ℤ ∖ ℕ)) \leftrightarrow (1 \in ℂ \land \neg 1 \in (ℤ ∖ ℕ))$
31	26 29 30	mpbir2an	$⊢ 1 \in (ℂ ∖ (ℤ ∖ ℕ))$
32	31	a1i	$⊢ ⊤ \to 1 \in (ℂ ∖ (ℤ ∖ ℕ))$
33	25 32	lgamcvg	$⊢ ⊤ \to seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ (\log Γ (1) + \log 1)$
34	33	mptru	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ (\log Γ (1) + \log 1)$
35		log1	$⊢ \log 1 = 0$
36	35	oveq2i	$⊢ \log Γ (1) + \log 1 = \log Γ (1) + 0$
37		lgamcl	$⊢ 1 \in (ℂ ∖ (ℤ ∖ ℕ)) \to \log Γ (1) \in ℂ$
38	31 37	ax-mp	$⊢ \log Γ (1) \in ℂ$
39	38	addridi	$⊢ \log Γ (1) + 0 = \log Γ (1)$
40	36 39	eqtri	$⊢ \log Γ (1) + \log 1 = \log Γ (1)$
41	34 40	breqtri	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ \log Γ (1)$
42		1z	$⊢ 1 \in ℤ$
43		serclim0	$⊢ 1 \in ℤ \to seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0$
44	42 43	ax-mp	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0$
45		climuni	$⊢ (seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ \log Γ (1) \land seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0) \to \log Γ (1) = 0$
46	41 44 45	mp2an	$⊢ \log Γ (1) = 0$

Metamath Proof Explorer

Theorem lgam1

Proof