Theorem vmadivsum

Description: The sum of the von Mangoldt function over n is asymptotic to log x + O(1) . Equation 9.2.13 of Shapiro, p. 331. (Contributed by Mario Carneiro, 16-Apr-2016)

	Ref	Expression
Assertion	vmadivsum	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\log x\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
3	1 2	ssexi	$$⊢{ℝ}^{+}\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to {ℝ}^{+}\in \mathrm{V}$$
5		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\in \mathrm{V}$$
6		ovexd	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \log x-\left(\frac{\log ⌊x⌋!}{x}\right)\in \mathrm{V}$$
7		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right)$$
8		eqidd	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)$$
9	4 5 6 7 8	offval2	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right){-}_f\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)-\left(\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\right)$$
10	9	mptru	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right){-}_f\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)-\left(\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\right)$$
11		fzfid	$$⊢x\in {ℝ}^{+}\to \left(1\dots ⌊x⌋\right)\in \mathrm{Fin}$$
12		elfznn	$$⊢n\in \left(1\dots ⌊x⌋\right)\to n\in \mathbb{N}$$
13	12	adantl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to n\in \mathbb{N}$$
14		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
15	13 14	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\in ℝ$$
16	15 13	nndivred	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \frac{\Lambda \left(n\right)}{n}\in ℝ$$
17	11 16	fsumrecl	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\in ℝ$$
18	17	recnd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\in ℂ$$
19		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
20	19	recnd	$$⊢x\in {ℝ}^{+}\to \log x\in ℂ$$
21		rprege0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℝ\wedge 0\le x\right)$$
22		flge0nn0	$$⊢\left(x\in ℝ\wedge 0\le x\right)\to ⌊x⌋\in {\mathbb{N}}_0$$
23		faccl	$$⊢⌊x⌋\in {\mathbb{N}}_0\to ⌊x⌋!\in \mathbb{N}$$
24	21 22 23	3syl	$$⊢x\in {ℝ}^{+}\to ⌊x⌋!\in \mathbb{N}$$
25	24	nnrpd	$$⊢x\in {ℝ}^{+}\to ⌊x⌋!\in {ℝ}^{+}$$
26	25	relogcld	$$⊢x\in {ℝ}^{+}\to \log ⌊x⌋!\in ℝ$$
27		rerpdivcl	$$⊢\left(\log ⌊x⌋!\in ℝ\wedge x\in {ℝ}^{+}\right)\to \frac{\log ⌊x⌋!}{x}\in ℝ$$
28	26 27	mpancom	$$⊢x\in {ℝ}^{+}\to \frac{\log ⌊x⌋!}{x}\in ℝ$$
29	28	recnd	$$⊢x\in {ℝ}^{+}\to \frac{\log ⌊x⌋!}{x}\in ℂ$$
30	18 20 29	nnncan2d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)-\left(\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\log x$$
31	30	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)-\left(\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\log x\right)$$
32	10 31	eqtri	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right){-}_f\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\log x\right)$$
33		1red	$$⊢\top \to 1\in ℝ$$
34		chpo1ub	$$⊢\left(x\in {ℝ}^{+}⟼\frac{\psi \left(x\right)}{x}\right)\in 𝑂\left(1\right)$$
35	34	a1i	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\frac{\psi \left(x\right)}{x}\right)\in 𝑂\left(1\right)$$
36		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
37		chpcl	$$⊢x\in ℝ\to \psi \left(x\right)\in ℝ$$
38	36 37	syl	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)\in ℝ$$
39		rerpdivcl	$$⊢\left(\psi \left(x\right)\in ℝ\wedge x\in {ℝ}^{+}\right)\to \frac{\psi \left(x\right)}{x}\in ℝ$$
40	38 39	mpancom	$$⊢x\in {ℝ}^{+}\to \frac{\psi \left(x\right)}{x}\in ℝ$$
41	40	recnd	$$⊢x\in {ℝ}^{+}\to \frac{\psi \left(x\right)}{x}\in ℂ$$
42	41	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \frac{\psi \left(x\right)}{x}\in ℂ$$
43	18 29	subcld	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\in ℂ$$
44	43	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{+}\right)\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\in ℂ$$
45	36	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to x\in ℝ$$
46	16 45	remulcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x\in ℝ$$
47		nndivre	$$⊢\left(x\in ℝ\wedge n\in \mathbb{N}\right)\to \frac{x}{n}\in ℝ$$
48	36 12 47	syl2an	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{n}\in ℝ$$
49		reflcl	$$⊢\frac{x}{n}\in ℝ\to ⌊\frac{x}{n}⌋\in ℝ$$
50	48 49	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to ⌊\frac{x}{n}⌋\in ℝ$$
51	15 50	remulcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)⌊\frac{x}{n}⌋\in ℝ$$
52	46 51	resubcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\in ℝ$$
53	48 50	resubcld	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\in ℝ$$
54		1red	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to 1\in ℝ$$
55		vmage0	$$⊢n\in \mathbb{N}\to 0\le \Lambda \left(n\right)$$
56	13 55	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to 0\le \Lambda \left(n\right)$$
57		fracle1	$$⊢\frac{x}{n}\in ℝ\to \left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\le 1$$
58	48 57	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\le 1$$
59	53 54 15 56 58	lemul2ad	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\left(\left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\right)\le \Lambda \left(n\right)\cdot 1$$
60	15	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\in ℂ$$
61	48	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \frac{x}{n}\in ℂ$$
62	50	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to ⌊\frac{x}{n}⌋\in ℂ$$
63	60 61 62	subdid	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\left(\left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\right)=\Lambda \left(n\right)\left(\frac{x}{n}\right)-\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
64		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
65	64	adantr	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to x\in ℂ$$
66	13	nnrpd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to n\in {ℝ}^{+}$$
67		rpcnne0	$$⊢n\in {ℝ}^{+}\to \left(n\in ℂ\wedge n\ne 0\right)$$
68	66 67	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(n\in ℂ\wedge n\ne 0\right)$$
69		div23	$$⊢\left(\Lambda \left(n\right)\in ℂ\wedge x\in ℂ\wedge \left(n\in ℂ\wedge n\ne 0\right)\right)\to \frac{\Lambda \left(n\right)x}{n}=\left(\frac{\Lambda \left(n\right)}{n}\right)x$$
70		divass	$$⊢\left(\Lambda \left(n\right)\in ℂ\wedge x\in ℂ\wedge \left(n\in ℂ\wedge n\ne 0\right)\right)\to \frac{\Lambda \left(n\right)x}{n}=\Lambda \left(n\right)\left(\frac{x}{n}\right)$$
71	69 70	eqtr3d	$$⊢\left(\Lambda \left(n\right)\in ℂ\wedge x\in ℂ\wedge \left(n\in ℂ\wedge n\ne 0\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x=\Lambda \left(n\right)\left(\frac{x}{n}\right)$$
72	60 65 68 71	syl3anc	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x=\Lambda \left(n\right)\left(\frac{x}{n}\right)$$
73	72	oveq1d	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋=\Lambda \left(n\right)\left(\frac{x}{n}\right)-\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
74	63 73	eqtr4d	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\left(\left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\right)=\left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
75	60	mulridd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)\cdot 1=\Lambda \left(n\right)$$
76	59 74 75	3brtr3d	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\le \Lambda \left(n\right)$$
77	11 52 15 76	fsumle	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\right)\le \sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)$$
78	16	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \frac{\Lambda \left(n\right)}{n}\in ℂ$$
79	11 64 78	fsummulc1	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x$$
80		logfac2	$$⊢\left(x\in ℝ\wedge 0\le x\right)\to \log ⌊x⌋!=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
81	21 80	syl	$$⊢x\in {ℝ}^{+}\to \log ⌊x⌋!=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
82	79 81	oveq12d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
83	46	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(\frac{\Lambda \left(n\right)}{n}\right)x\in ℂ$$
84	51	recnd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \Lambda \left(n\right)⌊\frac{x}{n}⌋\in ℂ$$
85	11 83 84	fsumsub	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\right)=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
86	82 85	eqtr4d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!=\sum _{n=1}^{⌊x⌋}\left(\left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\right)$$
87		chpval	$$⊢x\in ℝ\to \psi \left(x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)$$
88	36 87	syl	$$⊢x\in {ℝ}^{+}\to \psi \left(x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)$$
89	77 86 88	3brtr4d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\le \psi \left(x\right)$$
90	17 36	remulcld	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x\in ℝ$$
91	90 26	resubcld	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\in ℝ$$
92		rpregt0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℝ\wedge 0<x\right)$$
93		lediv1	$$⊢\left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\in ℝ\wedge \psi \left(x\right)\in ℝ\wedge \left(x\in ℝ\wedge 0<x\right)\right)\to \left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\le \psi \left(x\right)\leftrightarrow \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\le \frac{\psi \left(x\right)}{x}\right)$$
94	91 38 92 93	syl3anc	$$⊢x\in {ℝ}^{+}\to \left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\le \psi \left(x\right)\leftrightarrow \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\le \frac{\psi \left(x\right)}{x}\right)$$
95	89 94	mpbid	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\le \frac{\psi \left(x\right)}{x}$$
96	90	recnd	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x\in ℂ$$
97	26	recnd	$$⊢x\in {ℝ}^{+}\to \log ⌊x⌋!\in ℂ$$
98		rpcnne0	$$⊢x\in {ℝ}^{+}\to \left(x\in ℂ\wedge x\ne 0\right)$$
99		divsubdir	$$⊢\left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x\in ℂ\wedge \log ⌊x⌋!\in ℂ\wedge \left(x\in ℂ\wedge x\ne 0\right)\right)\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}=\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x}{x}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)$$
100	96 97 98 99	syl3anc	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}=\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x}{x}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)$$
101		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
102	18 64 101	divcan4d	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x}{x}=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)$$
103	102	oveq1d	$$⊢x\in {ℝ}^{+}\to \left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x}{x}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)=\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)$$
104	100 103	eqtr2d	$$⊢x\in {ℝ}^{+}\to \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)=\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}$$
105	104	fveq2d	$$⊢x\in {ℝ}^{+}\to \left|\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right|=\left|\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\right|$$
106		rerpdivcl	$$⊢\left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\in ℝ\wedge x\in {ℝ}^{+}\right)\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\in ℝ$$
107	91 106	mpancom	$$⊢x\in {ℝ}^{+}\to \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\in ℝ$$
108		flle	$$⊢\frac{x}{n}\in ℝ\to ⌊\frac{x}{n}⌋\le \frac{x}{n}$$
109	48 108	syl	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to ⌊\frac{x}{n}⌋\le \frac{x}{n}$$
110	48 50	subge0d	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to \left(0\le \left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\leftrightarrow ⌊\frac{x}{n}⌋\le \frac{x}{n}\right)$$
111	109 110	mpbird	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to 0\le \left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋$$
112	15 53 56 111	mulge0d	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to 0\le \Lambda \left(n\right)\left(\left(\frac{x}{n}\right)-⌊\frac{x}{n}⌋\right)$$
113	112 74	breqtrd	$$⊢\left(x\in {ℝ}^{+}\wedge n\in \left(1\dots ⌊x⌋\right)\right)\to 0\le \left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋$$
114	11 52 113	fsumge0	$$⊢x\in {ℝ}^{+}\to 0\le \sum _{n=1}^{⌊x⌋}\left(\left(\frac{\Lambda \left(n\right)}{n}\right)x-\Lambda \left(n\right)⌊\frac{x}{n}⌋\right)$$
115	114 86	breqtrrd	$$⊢x\in {ℝ}^{+}\to 0\le \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!$$
116		divge0	$$⊢\left(\left(\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\in ℝ\wedge 0\le \sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!\right)\wedge \left(x\in ℝ\wedge 0<x\right)\right)\to 0\le \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}$$
117	91 115 92 116	syl21anc	$$⊢x\in {ℝ}^{+}\to 0\le \frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}$$
118	107 117	absidd	$$⊢x\in {ℝ}^{+}\to \left|\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}\right|=\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}$$
119	105 118	eqtrd	$$⊢x\in {ℝ}^{+}\to \left|\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right|=\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)x-\log ⌊x⌋!}{x}$$
120		chpge0	$$⊢x\in ℝ\to 0\le \psi \left(x\right)$$
121	36 120	syl	$$⊢x\in {ℝ}^{+}\to 0\le \psi \left(x\right)$$
122		divge0	$$⊢\left(\left(\psi \left(x\right)\in ℝ\wedge 0\le \psi \left(x\right)\right)\wedge \left(x\in ℝ\wedge 0<x\right)\right)\to 0\le \frac{\psi \left(x\right)}{x}$$
123	38 121 92 122	syl21anc	$$⊢x\in {ℝ}^{+}\to 0\le \frac{\psi \left(x\right)}{x}$$
124	40 123	absidd	$$⊢x\in {ℝ}^{+}\to \left|\frac{\psi \left(x\right)}{x}\right|=\frac{\psi \left(x\right)}{x}$$
125	95 119 124	3brtr4d	$$⊢x\in {ℝ}^{+}\to \left|\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right|\le \left|\frac{\psi \left(x\right)}{x}\right|$$
126	125	ad2antrl	$$⊢\left(\top \wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to \left|\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right|\le \left|\frac{\psi \left(x\right)}{x}\right|$$
127	33 35 42 44 126	o1le	$$⊢\top \to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
128	127	mptru	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
129		logfacrlim	$$⊢\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\underset{ℝ}{⇝}1$$
130		rlimo1	$$⊢\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\underset{ℝ}{⇝}1\to \left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
131	129 130	ax-mp	$$⊢\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
132		o1sub	$$⊢\left(\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)\wedge \left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right){-}_f\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
133	128 131 132	mp2an	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\left(\frac{\log ⌊x⌋!}{x}\right)\right){-}_f\left(x\in {ℝ}^{+}⟼\log x-\left(\frac{\log ⌊x⌋!}{x}\right)\right)\in 𝑂\left(1\right)$$
134	32 133	eqeltrri	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)-\log x\right)\in 𝑂\left(1\right)$$