pntrlog2bndlem3

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

	Ref	Expression
Hypotheses	pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
	pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntrlog2bndlem3.1	$⊢ φ \to A \in ℝ^{+}$
	pntrlog2bndlem3.2	$⊢ φ \to \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq A$
Assertion	pntrlog2bndlem3	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
2		pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
3		pntrlog2bndlem3.1	$⊢ φ \to A \in ℝ^{+}$
4		pntrlog2bndlem3.2	$⊢ φ \to \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq A$
5		1red	$⊢ φ \to 1 \in ℝ$
6	3	rpred	$⊢ φ \to A \in ℝ$
7	6	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ$
8		fzfid	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
9		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
10	9	adantl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
11	10	nnred	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
12		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
13	12	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
14		1rp	$⊢ 1 \in ℝ^{+}$
15	14	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
16		1red	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
17		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
18	17	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
19	18	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
20	16 13 19	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
21	13 15 20	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
22	21	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
23	10	nnrpd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
24	14	a1i	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ^{+}$
25	23 24	rpaddcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℝ^{+}$
26	22 25	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n + 1} \in ℝ^{+}$
27	2	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
28	27	ffvelcdmi	$⊢ \frac{x}{n + 1} \in ℝ^{+} \to R (\frac{x}{n + 1}) \in ℝ$
29	26 28	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℝ$
30	29	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) \in ℂ$
31	22 23	rpdivcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
32	27	ffvelcdmi	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
33	31 32	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
34	33	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
35	30 34	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n + 1}) - R (\frac{x}{n}) \in ℂ$
36	35	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
37	11 36	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
38	8 37	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
39	13 19	rplogcld	$⊢ (φ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
40	21 39	rpmulcld	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
41	38 40	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} \in ℝ$
42		ioossre	$⊢ (1, +∞) \subseteq ℝ$
43	3	rpcnd	$⊢ φ \to A \in ℂ$
44		o1const	$⊢ ((1, +∞) \subseteq ℝ \land A \in ℂ) \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
45	42 43 44	sylancr	$⊢ φ \to (x \in (1, +∞) ⟼ A) \in 𝑂 (1)$
46		chpo1ubb	$⊢ \exists c \in ℝ^{+} \forall y \in ℝ^{+} ψ (y) \leq c y$
47		simpl	$⊢ (c \in ℝ^{+} \land \forall y \in ℝ^{+} ψ (y) \leq c y) \to c \in ℝ^{+}$
48		simpr	$⊢ (c \in ℝ^{+} \land \forall y \in ℝ^{+} ψ (y) \leq c y) \to \forall y \in ℝ^{+} ψ (y) \leq c y$
49	1 2 47 48	pntrlog2bndlem2	$⊢ (c \in ℝ^{+} \land \forall y \in ℝ^{+} ψ (y) \leq c y) \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in 𝑂 (1)$
50	49	rexlimiva	$⊢ \exists c \in ℝ^{+} \forall y \in ℝ^{+} ψ (y) \leq c y \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in 𝑂 (1)$
51	46 50	mp1i	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in 𝑂 (1)$
52	7 41 45 51	o1mul2	$⊢ φ \to (x \in (1, +∞) ⟼ A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})) \in 𝑂 (1)$
53	7 41	remulcld	$⊢ (φ \land x \in (1, +∞)) \to A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in ℝ$
54	34	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
55	30	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1})\| \in ℝ$
56	54 55	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\| \in ℝ$
57	1	pntsf	$⊢ S : ℝ ⟶ ℝ$
58	57	ffvelcdmi	$⊢ n \in ℝ \to S (n) \in ℝ$
59	11 58	syl	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) \in ℝ$
60		2re	$⊢ 2 \in ℝ$
61	60	a1i	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℝ$
62	23	relogcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
63	11 62	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \log n \in ℝ$
64	61 63	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 n \log n \in ℝ$
65	59 64	resubcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - 2 n \log n \in ℝ$
66	56 65	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℝ$
67	8 66	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℝ$
68	67 40	rerpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} \in ℝ$
69	68	recnd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x} \in ℂ$
70	69	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\| \in ℝ$
71	53	recnd	$⊢ (φ \land x \in (1, +∞)) \to A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \in ℂ$
72	71	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})\| \in ℝ$
73	67	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℂ$
74	73	abscld	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \in ℝ$
75	7 38	remulcld	$⊢ (φ \land x \in (1, +∞)) \to A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
76	66	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n) \in ℂ$
77	76	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \in ℝ$
78	8 77	fsumrecl	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \in ℝ$
79	8 76	fsumabs	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \leq \sum_{n = 1}^{⌊x⌋} \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|$
80	7	adantr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℝ$
81	80 37	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℝ$
82	56	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\| \in ℂ$
83	82	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\| \in ℝ$
84	65	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) - 2 n \log n \in ℂ$
85	84	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|S (n) - 2 n \log n\| \in ℝ$
86	80 11	remulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \in ℝ$
87	82	absge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\|$
88	84	absge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|S (n) - 2 n \log n\|$
89	34 30	abs2difabsd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\| \leq \|R (\frac{x}{n}) - R (\frac{x}{n + 1})\|$
90	34 30	abssubd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n}) - R (\frac{x}{n + 1})\| = \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
91	89 90	breqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\| \leq \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
92	59	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to S (n) \in ℂ$
93	11	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
94	10	nnne0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
95	92 93 94	divcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{S (n)}{n} \in ℂ$
96		2cnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
97	62	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
98	96 97	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \log n \in ℂ$
99	95 98	subcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{S (n)}{n}) - 2 \log n \in ℂ$
100	99 93	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{S (n)}{n}) - 2 \log n) n\| = \|(\frac{S (n)}{n}) - 2 \log n\| \|n\|$
101	95 98 93	subdird	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{S (n)}{n}) - 2 \log n) n = (\frac{S (n)}{n}) n - 2 \log n n$
102	92 93 94	divcan1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{S (n)}{n}) n = S (n)$
103	96 93 97	mul32d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 n \log n = 2 \log n n$
104	96 93 97	mulassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 n \log n = 2 n \log n$
105	103 104	eqtr3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 2 \log n n = 2 n \log n$
106	102 105	oveq12d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{S (n)}{n}) n - 2 \log n n = S (n) - 2 n \log n$
107	101 106	eqtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{S (n)}{n}) - 2 \log n) n = S (n) - 2 n \log n$
108	107	fveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|((\frac{S (n)}{n}) - 2 \log n) n\| = \|S (n) - 2 n \log n\|$
109	23	rpge0d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq n$
110	11 109	absidd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|n\| = n$
111	110	oveq2d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{S (n)}{n}) - 2 \log n\| \|n\| = \|(\frac{S (n)}{n}) - 2 \log n\| n$
112	100 108 111	3eqtr3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|S (n) - 2 n \log n\| = \|(\frac{S (n)}{n}) - 2 \log n\| n$
113	99	abscld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{S (n)}{n}) - 2 \log n\| \in ℝ$
114		fveq2	$⊢ y = n \to S (y) = S (n)$
115		id	$⊢ y = n \to y = n$
116	114 115	oveq12d	$⊢ y = n \to \frac{S (y)}{y} = \frac{S (n)}{n}$
117		fveq2	$⊢ y = n \to \log y = \log n$
118	117	oveq2d	$⊢ y = n \to 2 \log y = 2 \log n$
119	116 118	oveq12d	$⊢ y = n \to (\frac{S (y)}{y}) - 2 \log y = (\frac{S (n)}{n}) - 2 \log n$
120	119	fveq2d	$⊢ y = n \to \|(\frac{S (y)}{y}) - 2 \log y\| = \|(\frac{S (n)}{n}) - 2 \log n\|$
121	120	breq1d	$⊢ y = n \to (\|(\frac{S (y)}{y}) - 2 \log y\| \leq A \leftrightarrow \|(\frac{S (n)}{n}) - 2 \log n\| \leq A)$
122	4	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|(\frac{S (y)}{y}) - 2 \log y\| \leq A$
123	10	nnge1d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq n$
124		1re	$⊢ 1 \in ℝ$
125		elicopnf	$⊢ 1 \in ℝ \to (n \in [1, +∞) \leftrightarrow (n \in ℝ \land 1 \leq n))$
126	124 125	ax-mp	$⊢ n \in [1, +∞) \leftrightarrow (n \in ℝ \land 1 \leq n)$
127	11 123 126	sylanbrc	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in [1, +∞)$
128	121 122 127	rspcdva	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{S (n)}{n}) - 2 \log n\| \leq A$
129	113 80 11 109 128	lemul1ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{S (n)}{n}) - 2 \log n\| n \leq A n$
130	112 129	eqbrtrd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|S (n) - 2 n \log n\| \leq A n$
131	83 36 85 86 87 88 91 130	lemul12ad	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\| \|S (n) - 2 n \log n\| \leq \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| A n$
132	82 84	absmuld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| = \|\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|\| \|S (n) - 2 n \log n\|$
133	43	ad2antrr	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A \in ℂ$
134	36	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℂ$
135	133 93 134	mulassd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| = A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
136	133 93	mulcld	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \in ℂ$
137	136 134	mulcomd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| = \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| A n$
138	135 137	eqtr3d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| = \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| A n$
139	131 132 138	3brtr4d	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \leq A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
140	8 77 81 139	fsumle	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \leq \sum_{n = 1}^{⌊x⌋} A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
141	43	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℂ$
142	37	recnd	$⊢ ((φ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℂ$
143	8 141 142	fsummulc2	$⊢ (φ \land x \in (1, +∞)) \to A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| = \sum_{n = 1}^{⌊x⌋} A n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
144	140 143	breqtrrd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} \|(\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \leq A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
145	74 78 75 79 144	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\| \leq A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|$
146	74 75 40 145	lediv1dd	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|}{x \log x} \leq \frac{A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}$
147	40	rpcnd	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℂ$
148	40	rpne0d	$⊢ (φ \land x \in (1, +∞)) \to x \log x \neq 0$
149	73 147 148	absdivd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\| = \frac{\|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|}{\|x \log x\|}$
150	40	rpred	$⊢ (φ \land x \in (1, +∞)) \to x \log x \in ℝ$
151	40	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq x \log x$
152	150 151	absidd	$⊢ (φ \land x \in (1, +∞)) \to \|x \log x\| = x \log x$
153	152	oveq2d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|}{\|x \log x\|} = \frac{\|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|}{x \log x}$
154	149 153	eqtr2d	$⊢ (φ \land x \in (1, +∞)) \to \frac{\|\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)\|}{x \log x} = \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\|$
155	38	recnd	$⊢ (φ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\| \in ℂ$
156	141 155 147 148	divassd	$⊢ (φ \land x \in (1, +∞)) \to \frac{A \sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x} = A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})$
157	146 154 156	3brtr3d	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\| \leq A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})$
158	53	leabsd	$⊢ (φ \land x \in (1, +∞)) \to A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x}) \leq \|A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})\|$
159	70 53 72 157 158	letrd	$⊢ (φ \land x \in (1, +∞)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\| \leq \|A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})\|$
160	159	adantrr	$⊢ (φ \land (x \in (1, +∞) \land 1 \leq x)) \to \|\frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}\| \leq \|A (\frac{\sum_{n = 1}^{⌊x⌋} n \|R (\frac{x}{n + 1}) - R (\frac{x}{n})\|}{x \log x})\|$
161	5 52 53 69 160	o1le	$⊢ φ \to (x \in (1, +∞) ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\|R (\frac{x}{n})\| - \|R (\frac{x}{n + 1})\|) (S (n) - 2 n \log n)}{x \log x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrlog2bndlem3

Proof