Theorem relgamcl

Description: The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	relgamcl	⊢ ( 𝐴 ∈ ℝ+ → ( log Γ ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rpdmgm	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
2		lgamcl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( log Γ ‘ 𝐴 ) ∈ ℂ )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ+ → ( log Γ ‘ 𝐴 ) ∈ ℂ )
4		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
6	3 5	pncand	⊢ ( 𝐴 ∈ ℝ+ → ( ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) − ( log ‘ 𝐴 ) ) = ( log Γ ‘ 𝐴 ) )
7		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
8		1zzd	⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℤ )
9		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) )
10	9 1	lgamcvg	⊢ ( 𝐴 ∈ ℝ+ → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ⇝ ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) )
11		simpl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ℝ+ )
12	11	rpred	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ℝ )
13		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
14	13	peano2nnd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
15	14	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℝ+ )
16	13	nnrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
17	15 16	rpdivcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ+ )
18	17	relogcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ∈ ℝ )
19	12 18	remulcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) ∈ ℝ )
20	11 16	rpdivcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( 𝐴 / 𝑚 ) ∈ ℝ+ )
21		1rp	⊢ 1 ∈ ℝ+
22	21	a1i	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ+ )
23	20 22	rpaddcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 / 𝑚 ) + 1 ) ∈ ℝ+ )
24	23	relogcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ∈ ℝ )
25	19 24	resubcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ∈ ℝ )
26	25	fmpttd	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) : ℕ ⟶ ℝ )
27	26	ffvelrnda	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
28	7 8 27	serfre	⊢ ( 𝐴 ∈ ℝ+ → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) : ℕ ⟶ ℝ )
29	28	ffvelrnda	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( ( 𝐴 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
30	7 8 10 29	climrecl	⊢ ( 𝐴 ∈ ℝ+ → ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) ∈ ℝ )
31	30 4	resubcld	⊢ ( 𝐴 ∈ ℝ+ → ( ( ( log Γ ‘ 𝐴 ) + ( log ‘ 𝐴 ) ) − ( log ‘ 𝐴 ) ) ∈ ℝ )
32	6 31	eqeltrrd	⊢ ( 𝐴 ∈ ℝ+ → ( log Γ ‘ 𝐴 ) ∈ ℝ )