logfacrlim2

		Ref	Expression
	Assertion	logfacrlim2	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		logexprlim	$⊢ 1 \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1}}{x}) \underset{ℝ}{⇝} 1!$
3	1 2	ax-mp	$⊢ (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1}}{x}) \underset{ℝ}{⇝} 1!$
4		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
5	4	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
6		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
7	5 6	sylan2	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
8	7	relogcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
9	8	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
10	9	exp1d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{1} = \log (\frac{x}{n})$
11	10	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1} = \sum_{n = 1}^{⌊x⌋} \log (\frac{x}{n})$
12	11	oveq1d	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1}}{x} = \frac{\sum_{n = 1}^{⌊x⌋} \log (\frac{x}{n})}{x}$
13		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
14		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
15		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
16	13 14 9 15	fsumdivc	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} \log (\frac{x}{n})}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})$
17	12 16	eqtrd	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1}}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})$
18	17	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{1}}{x}) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}))$
19		fac1	$⊢ 1! = 1$
20	3 18 19	3brtr3i	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem logfacrlim2

Proof