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	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$

Proof

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

Metamath Proof Explorer

Theorem vmadivsum

Proof