rpvmasum

Description: The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 2-May-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.u	$⊢ U = Unit (Z)$
	rpvmasum.b	$⊢ φ \to A \in U$
	rpvmasum.t	$⊢ T = L^{-1} [\{A\}]$
Assertion	rpvmasum	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.u	$⊢ U = Unit (Z)$
5		rpvmasum.b	$⊢ φ \to A \in U$
6		rpvmasum.t	$⊢ T = L^{-1} [\{A\}]$
7	3	adantr	$⊢ (φ \land f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}) \to N \in ℕ$
8		eqid	$⊢ DChr (N) = DChr (N)$
9		eqid	$⊢ {Base}_{DChr (N)} = {Base}_{DChr (N)}$
10		eqid	$⊢ 0_{DChr (N)} = 0_{DChr (N)}$
11		2fveq3	$⊢ m = n \to y (L (m)) = y (L (n))$
12		id	$⊢ m = n \to m = n$
13	11 12	oveq12d	$⊢ m = n \to \frac{y (L (m))}{m} = \frac{y (L (n))}{n}$
14	13	cbvsumv	$⊢ \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = \sum_{n \in ℕ} (\frac{y (L (n))}{n})$
15	14	eqeq1i	$⊢ \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0 \leftrightarrow \sum_{n \in ℕ} (\frac{y (L (n))}{n}) = 0$
16	15	rabbii	$⊢ \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\} = \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{n \in ℕ} (\frac{y (L (n))}{n}) = 0\}$
17		simpr	$⊢ (φ \land f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}) \to f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
18	1 2 7 8 9 10 16 17	dchrisum0	$⊢ \neg (φ \land f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\})$
19	18	imnani	$⊢ φ \to \neg f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
20	19	eq0rdv	$⊢ φ \to \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\} = \emptyset$
21	20	fveq2d	$⊢ φ \to \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\| = \|\emptyset\|$
22		hash0	$⊢ \|\emptyset\| = 0$
23	21 22	eqtrdi	$⊢ φ \to \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\| = 0$
24	23	oveq2d	$⊢ φ \to 1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\| = 1 - 0$
25		1m0e1	$⊢ 1 - 0 = 1$
26	24 25	eqtrdi	$⊢ φ \to 1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\| = 1$
27	26	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\| = 1$
28	27	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \log x (1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\|) = \log x \cdot 1$
29		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
30	29	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
31	30	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
32	31	mulridd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \cdot 1 = \log x$
33	28 32	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \log x (1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\|) = \log x$
34	33	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\|) = ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x$
35	34	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\|)) = (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x)$
36		eqid	$⊢ \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\} = \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
37	18	pm2.21i	$⊢ (φ \land f \in \{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}) \to A = 1_{Z}$
38	1 2 3 8 9 10 36 4 5 6 37	rpvmasum2	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|\{y \in ({Base}_{DChr (N)} ∖ \{0_{DChr (N)}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}\|)) \in 𝑂 (1)$
39	35 38	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem rpvmasum

Proof