rplogsum

Description: The sum of log p / p over the primes p == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 16-Apr-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	rplogsum	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \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	1 2 3 4 5 6	rpvmasum	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x) \in 𝑂 (1)$
8	3	phicld	$⊢ φ \to ϕ (N) \in ℕ$
9	8	adantr	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℕ$
10	9	nncnd	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℂ$
11		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
12		inss1	$⊢ (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)$
13		ssfi	$⊢ ((1 \dots ⌊x⌋) \in Fin \land (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \cap T \in Fin$
14	11 12 13	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap T \in Fin$
15		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to p \in ((1 \dots ⌊x⌋) \cap T)$
16	15	elin1d	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to p \in (1 \dots ⌊x⌋)$
17		elfznn	$⊢ p \in (1 \dots ⌊x⌋) \to p \in ℕ$
18	16 17	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to p \in ℕ$
19		vmacl	$⊢ p \in ℕ \to Λ (p) \in ℝ$
20		nndivre	$⊢ (Λ (p) \in ℝ \land p \in ℕ) \to \frac{Λ (p)}{p} \in ℝ$
21	19 20	mpancom	$⊢ p \in ℕ \to \frac{Λ (p)}{p} \in ℝ$
22	18 21	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{Λ (p)}{p} \in ℝ$
23	14 22	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) \in ℝ$
24	23	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) \in ℂ$
25	10 24	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) \in ℂ$
26		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
27	26	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
28	27	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
29	25 28	subcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x \in ℂ$
30		inss1	$⊢ (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq (1 \dots ⌊x⌋)$
31		ssfi	$⊢ ((1 \dots ⌊x⌋) \in Fin \land (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \cap (ℙ \cap T) \in Fin$
32	11 30 31	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap (ℙ \cap T) \in Fin$
33		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))$
34	33	elin1d	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to p \in (1 \dots ⌊x⌋)$
35	34 17	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to p \in ℕ$
36		nnrp	$⊢ p \in ℕ \to p \in ℝ^{+}$
37	36	relogcld	$⊢ p \in ℕ \to \log p \in ℝ$
38	37 36	rerpdivcld	$⊢ p \in ℕ \to \frac{\log p}{p} \in ℝ$
39	35 38	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to \frac{\log p}{p} \in ℝ$
40	32 39	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) \in ℝ$
41	40	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) \in ℂ$
42	10 41	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) \in ℂ$
43	42 28	subcld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x \in ℂ$
44	10 24 41	subdid	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) (\sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})) = ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
45	19	recnd	$⊢ p \in ℕ \to Λ (p) \in ℂ$
46		0re	$⊢ 0 \in ℝ$
47		ifcl	$⊢ (\log p \in ℝ \land 0 \in ℝ) \to if (p \in ℙ, \log p, 0) \in ℝ$
48	37 46 47	sylancl	$⊢ p \in ℕ \to if (p \in ℙ, \log p, 0) \in ℝ$
49	48	recnd	$⊢ p \in ℕ \to if (p \in ℙ, \log p, 0) \in ℂ$
50	36	rpcnne0d	$⊢ p \in ℕ \to (p \in ℂ \land p \neq 0)$
51		divsubdir	$⊢ (Λ (p) \in ℂ \land if (p \in ℙ, \log p, 0) \in ℂ \land (p \in ℂ \land p \neq 0)) \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} = (\frac{Λ (p)}{p}) - (\frac{if (p \in ℙ, \log p, 0)}{p})$
52	45 49 50 51	syl3anc	$⊢ p \in ℕ \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} = (\frac{Λ (p)}{p}) - (\frac{if (p \in ℙ, \log p, 0)}{p})$
53	18 52	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} = (\frac{Λ (p)}{p}) - (\frac{if (p \in ℙ, \log p, 0)}{p})$
54	53	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap T} ((\frac{Λ (p)}{p}) - (\frac{if (p \in ℙ, \log p, 0)}{p}))$
55	21	recnd	$⊢ p \in ℕ \to \frac{Λ (p)}{p} \in ℂ$
56	18 55	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{Λ (p)}{p} \in ℂ$
57	48 36	rerpdivcld	$⊢ p \in ℕ \to \frac{if (p \in ℙ, \log p, 0)}{p} \in ℝ$
58	57	recnd	$⊢ p \in ℕ \to \frac{if (p \in ℙ, \log p, 0)}{p} \in ℂ$
59	18 58	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{if (p \in ℙ, \log p, 0)}{p} \in ℂ$
60	14 56 59	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} ((\frac{Λ (p)}{p}) - (\frac{if (p \in ℙ, \log p, 0)}{p})) = \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{if (p \in ℙ, \log p, 0)}{p})$
61		inss2	$⊢ ℙ \cap T \subseteq T$
62		sslin	$⊢ ℙ \cap T \subseteq T \to (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq (1 \dots ⌊x⌋) \cap T$
63	61 62	mp1i	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq (1 \dots ⌊x⌋) \cap T$
64	35 58	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to \frac{if (p \in ℙ, \log p, 0)}{p} \in ℂ$
65		eldif	$⊢ p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \leftrightarrow (p \in ((1 \dots ⌊x⌋) \cap T) \land \neg p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))$
66		incom	$⊢ ℙ \cap T = T \cap ℙ$
67	66	ineq2i	$⊢ (1 \dots ⌊x⌋) \cap (ℙ \cap T) = (1 \dots ⌊x⌋) \cap (T \cap ℙ)$
68		inass	$⊢ ((1 \dots ⌊x⌋) \cap T) \cap ℙ = (1 \dots ⌊x⌋) \cap (T \cap ℙ)$
69	67 68	eqtr4i	$⊢ (1 \dots ⌊x⌋) \cap (ℙ \cap T) = ((1 \dots ⌊x⌋) \cap T) \cap ℙ$
70	69	elin2	$⊢ p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T)) \leftrightarrow (p \in ((1 \dots ⌊x⌋) \cap T) \land p \in ℙ)$
71	70	simplbi2	$⊢ p \in ((1 \dots ⌊x⌋) \cap T) \to (p \in ℙ \to p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))$
72	71	con3dimp	$⊢ (p \in ((1 \dots ⌊x⌋) \cap T) \land \neg p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to \neg p \in ℙ$
73	65 72	sylbi	$⊢ p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to \neg p \in ℙ$
74	73	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to \neg p \in ℙ$
75	74	iffalsed	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to if (p \in ℙ, \log p, 0) = 0$
76	75	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to \frac{if (p \in ℙ, \log p, 0)}{p} = \frac{0}{p}$
77		eldifi	$⊢ p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to p \in ((1 \dots ⌊x⌋) \cap T)$
78	77 18	sylan2	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to p \in ℕ$
79		div0	$⊢ (p \in ℂ \land p \neq 0) \to \frac{0}{p} = 0$
80	50 79	syl	$⊢ p \in ℕ \to \frac{0}{p} = 0$
81	78 80	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to \frac{0}{p} = 0$
82	76 81	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (((1 \dots ⌊x⌋) \cap T) ∖ ((1 \dots ⌊x⌋) \cap (ℙ \cap T)))) \to \frac{if (p \in ℙ, \log p, 0)}{p} = 0$
83	63 64 82 14	fsumss	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{if (p \in ℙ, \log p, 0)}{p})$
84		inss2	$⊢ (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq ℙ \cap T$
85		inss1	$⊢ ℙ \cap T \subseteq ℙ$
86	84 85	sstri	$⊢ (1 \dots ⌊x⌋) \cap (ℙ \cap T) \subseteq ℙ$
87	86 33	sseldi	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to p \in ℙ$
88	87	iftrued	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to if (p \in ℙ, \log p, 0) = \log p$
89	88	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap (ℙ \cap T))) \to \frac{if (p \in ℙ, \log p, 0)}{p} = \frac{\log p}{p}$
90	89	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
91	83 90	eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
92	91	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
93	54 60 92	3eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) = \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
94	93	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) = ϕ (N) (\sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}))$
95	25 42 28	nnncan2d	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x - (ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x) = ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p})$
96	44 94 95	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) = ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x - (ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x)$
97	96	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})) = (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x - (ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x))$
98	19 48	resubcld	$⊢ p \in ℕ \to Λ (p) - if (p \in ℙ, \log p, 0) \in ℝ$
99	98 36	rerpdivcld	$⊢ p \in ℕ \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} \in ℝ$
100	18 99	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} \in ℝ$
101	14 100	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \in ℝ$
102	101	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \in ℂ$
103		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
104	8	nncnd	$⊢ φ \to ϕ (N) \in ℂ$
105		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land ϕ (N) \in ℂ) \to (x \in ℝ^{+} ⟼ ϕ (N)) \in 𝑂 (1)$
106	103 104 105	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N)) \in 𝑂 (1)$
107	103	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
108		1red	$⊢ φ \to 1 \in ℝ$
109		2re	$⊢ 2 \in ℝ$
110	109	a1i	$⊢ φ \to 2 \in ℝ$
111		breq1	$⊢ \log p = if (p \in ℙ, \log p, 0) \to (\log p \leq Λ (p) \leftrightarrow if (p \in ℙ, \log p, 0) \leq Λ (p))$
112		breq1	$⊢ 0 = if (p \in ℙ, \log p, 0) \to (0 \leq Λ (p) \leftrightarrow if (p \in ℙ, \log p, 0) \leq Λ (p))$
113	37	adantr	$⊢ (p \in ℕ \land p \in ℙ) \to \log p \in ℝ$
114		vmaprm	$⊢ p \in ℙ \to Λ (p) = \log p$
115	114	adantl	$⊢ (p \in ℕ \land p \in ℙ) \to Λ (p) = \log p$
116	115	eqcomd	$⊢ (p \in ℕ \land p \in ℙ) \to \log p = Λ (p)$
117	113 116	eqled	$⊢ (p \in ℕ \land p \in ℙ) \to \log p \leq Λ (p)$
118		vmage0	$⊢ p \in ℕ \to 0 \leq Λ (p)$
119	118	adantr	$⊢ (p \in ℕ \land \neg p \in ℙ) \to 0 \leq Λ (p)$
120	111 112 117 119	ifbothda	$⊢ p \in ℕ \to if (p \in ℙ, \log p, 0) \leq Λ (p)$
121	19 48	subge0d	$⊢ p \in ℕ \to (0 \leq Λ (p) - if (p \in ℙ, \log p, 0) \leftrightarrow if (p \in ℙ, \log p, 0) \leq Λ (p))$
122	120 121	mpbird	$⊢ p \in ℕ \to 0 \leq Λ (p) - if (p \in ℙ, \log p, 0)$
123	98 36 122	divge0d	$⊢ p \in ℕ \to 0 \leq \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}$
124	18 123	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in ((1 \dots ⌊x⌋) \cap T)) \to 0 \leq \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}$
125	14 100 124	fsumge0	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})$
126	101 125	absidd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})\| = \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})$
127	17	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (1 \dots ⌊x⌋)) \to p \in ℕ$
128	127 99	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (1 \dots ⌊x⌋)) \to \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p} \in ℝ$
129	11 128	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p = 1}^{⌊x⌋} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \in ℝ$
130	109	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℝ$
131	127 123	syl	$⊢ ((φ \land x \in ℝ^{+}) \land p \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}$
132	12	a1i	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)$
133	11 128 131 132	fsumless	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \leq \sum_{p = 1}^{⌊x⌋} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})$
134	107	sselda	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
135	134	flcld	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℤ$
136		rplogsumlem2	$⊢ ⌊x⌋ \in ℤ \to \sum_{p = 1}^{⌊x⌋} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \leq 2$
137	135 136	syl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p = 1}^{⌊x⌋} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \leq 2$
138	101 129 130 133 137	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p}) \leq 2$
139	126 138	eqbrtrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})\| \leq 2$
140	139	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})\| \leq 2$
141	107 102 108 110 140	elo1d	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})) \in 𝑂 (1)$
142	10 102 106 141	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p) - if (p \in ℙ, \log p, 0)}{p})) \in 𝑂 (1)$
143	97 142	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x - (ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x)) \in 𝑂 (1)$
144	29 43 143	o1dif	$⊢ φ \to ((x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (p)}{p}) - \log x) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x) \in 𝑂 (1))$
145	7 144	mpbid	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{p \in (1 \dots ⌊x⌋) \cap (ℙ \cap T)} (\frac{\log p}{p}) - \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem rplogsum

Proof