selberglem3

Description: Lemma for selberg . Estimation of the left-hand side of logsqvma2 . (Contributed by Mario Carneiro, 23-May-2016)

		Ref	Expression
	Assertion	selberglem3	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$⊢ n = d m \to \log (\frac{n}{d}) = \log (\frac{d m}{d})$
2	1	oveq1d	$⊢ n = d m \to {\log (\frac{n}{d})}^{2} = {\log (\frac{d m}{d})}^{2}$
3	2	oveq2d	$⊢ n = d m \to μ (d) {\log (\frac{n}{d})}^{2} = μ (d) {\log (\frac{d m}{d})}^{2}$
4		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
5		ssrab2	$⊢ \{y \in ℕ \| y ∥ n\} \subseteq ℕ$
6		simprr	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in \{y \in ℕ \| y ∥ n\}$
7	5 6	sseldi	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in ℕ$
8		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
9	7 8	syl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℤ$
10	9	zcnd	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℂ$
11		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
12	11	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
13	12	ad2antrl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to n \in ℝ^{+}$
14	7	nnrpd	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in ℝ^{+}$
15	13 14	rpdivcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to \frac{n}{d} \in ℝ^{+}$
16		relogcl	$⊢ \frac{n}{d} \in ℝ^{+} \to \log (\frac{n}{d}) \in ℝ$
17	16	recnd	$⊢ \frac{n}{d} \in ℝ^{+} \to \log (\frac{n}{d}) \in ℂ$
18	15 17	syl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to \log (\frac{n}{d}) \in ℂ$
19	18	sqcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to {\log (\frac{n}{d})}^{2} \in ℂ$
20	10 19	mulcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) {\log (\frac{n}{d})}^{2} \in ℂ$
21	3 4 20	dvdsflsumcom	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log (\frac{d m}{d})}^{2}$
22		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{d}⌋) \to m \in ℕ$
23	22	3ad2ant3	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℕ$
24	23	nncnd	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℂ$
25		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
26	25	3ad2ant2	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℕ$
27	26	nncnd	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℂ$
28	26	nnne0d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \neq 0$
29	24 27 28	divcan3d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{d m}{d} = m$
30	29	fveq2d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \log (\frac{d m}{d}) = \log m$
31	30	oveq1d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to {\log (\frac{d m}{d})}^{2} = {\log m}^{2}$
32	31	oveq2d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) {\log (\frac{d m}{d})}^{2} = μ (d) {\log m}^{2}$
33	32	2sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log (\frac{d m}{d})}^{2} = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}$
34	21 33	eqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}$
35	34	oveq1d	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}}{x} = \frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}$
36	35	oveq1d	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}}{x}) - 2 \log x = (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x$
37	36	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}}{x}) - 2 \log x) = (x \in ℝ^{+} ⟼ (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x)$
38		eqid	$⊢ \frac{{\log (\frac{x}{d})}^{2} + 2 - 2 \log (\frac{x}{d})}{d} = \frac{{\log (\frac{x}{d})}^{2} + 2 - 2 \log (\frac{x}{d})}{d}$
39	38	selberglem2	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$
40	37 39	eqeltri	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberglem3

Proof