Theorem logfacrlim2

Description: Write out logfacrlim as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016) (Revised by Mario Carneiro, 22-May-2016)

	Ref	Expression
Assertion	logfacrlim2	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) ) ⇝𝑟 1

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		logexprlim	⊢ ( 1 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 1 ) )
3	1 2	ax-mp	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 1 )
4		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
5	4	nnrpd	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
6		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
7	5 6	sylan2	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
8	7	relogcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
9	8	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
10	9	exp1d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) = ( log ‘ ( 𝑥 / 𝑛 ) ) )
11	10	sumeq2dv	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( log ‘ ( 𝑥 / 𝑛 ) ) )
12	11	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) / 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) )
13		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
14		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
15		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
16	13 14 9 15	fsumdivc	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) )
17	12 16	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) )
18	17	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 1 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) )
19		fac1	⊢ ( ! ‘ 1 ) = 1
20	3 18 19	3brtr3i	⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑥 ) ) ⇝𝑟 1