logfacrlim2

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

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ₀
2		logexprlim	⊢ ( 1 ∈ ℕ₀ → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 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

Metamath Proof Explorer

Theorem logfacrlim2

Proof