pntrlog2bnd

Description: A bound on R ( x ) log ^ 2 ( x ) . Equation 10.6.15 of Shapiro, p. 431. (Contributed by Mario Carneiro, 1-Jun-2016)

		Ref	Expression
	Hypothesis	pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntrlog2bnd	$⊢ (A \in ℝ \land 1 \leq A) \to \exists c \in ℝ^{+} \forall x \in (1, +∞) \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \leq c$

Proof

Step	Hyp	Ref	Expression
1		pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		ioossre	$⊢ (1, +∞) \subseteq ℝ$
3	2	a1i	$⊢ (A \in ℝ \land 1 \leq A) \to (1, +∞) \subseteq ℝ$
4		1red	$⊢ (A \in ℝ \land 1 \leq A) \to 1 \in ℝ$
5	3	sselda	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to x \in ℝ$
6		1rp	$⊢ 1 \in ℝ^{+}$
7	6	a1i	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
8		1red	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to 1 \in ℝ$
9		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
10	9	adantl	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
11	10	simpld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to 1 < x$
12	8 5 11	ltled	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to 1 \leq x$
13	5 7 12	rpgecld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to x \in ℝ^{+}$
14	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
15	14	ffvelrni	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
16	13 15	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to R (x) \in ℝ$
17	16	recnd	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to R (x) \in ℂ$
18	17	abscld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \|R (x)\| \in ℝ$
19	13	relogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \log x \in ℝ$
20	18 19	remulcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \|R (x)\| \log x \in ℝ$
21		2re	$⊢ 2 \in ℝ$
22	21	a1i	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to 2 \in ℝ$
23	5 11	rplogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
24	22 23	rerpdivcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
25		fzfid	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to (1 \dots ⌊\frac{x}{A}⌋) \in Fin$
26	13	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to x \in ℝ^{+}$
27		elfznn	$⊢ n \in (1 \dots ⌊\frac{x}{A}⌋) \to n \in ℕ$
28	27	adantl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℕ$
29	28	nnrpd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℝ^{+}$
30	26 29	rpdivcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \frac{x}{n} \in ℝ^{+}$
31	14	ffvelrni	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
32	30 31	syl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to R (\frac{x}{n}) \in ℝ$
33	32	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to R (\frac{x}{n}) \in ℂ$
34	33	abscld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
35	29	relogcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \log n \in ℝ$
36	34 35	remulcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \|R (\frac{x}{n})\| \log n \in ℝ$
37	25 36	fsumrecl	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
38	24 37	remulcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
39	20 38	resubcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
40	39 13	rerpdivcld	$⊢ ((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \in ℝ$
41	1	pntrmax	$⊢ \exists c \in ℝ^{+} \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c$
42		eqid	$⊢ (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i}))) = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
43		eqid	$⊢ (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0)) = (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0))$
44		simprl	$⊢ ((A \in ℝ \land 1 \leq A) \land (c \in ℝ^{+} \land \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c)) \to c \in ℝ^{+}$
45		simprr	$⊢ ((A \in ℝ \land 1 \leq A) \land (c \in ℝ^{+} \land \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c)) \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c$
46		simpll	$⊢ ((A \in ℝ \land 1 \leq A) \land (c \in ℝ^{+} \land \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c)) \to A \in ℝ$
47		simplr	$⊢ ((A \in ℝ \land 1 \leq A) \land (c \in ℝ^{+} \land \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c)) \to 1 \leq A$
48	42 1 43 44 45 46 47	pntrlog2bndlem6	$⊢ ((A \in ℝ \land 1 \leq A) \land (c \in ℝ^{+} \land \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c)) \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1)$
49	48	rexlimdvaa	$⊢ (A \in ℝ \land 1 \leq A) \to (\exists c \in ℝ^{+} \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq c \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1))$
50	41 49	mpi	$⊢ (A \in ℝ \land 1 \leq A) \to (x \in (1, +∞) ⟼ \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x}) \in \leq 𝑂 (1)$
51		simprl	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ$
52		chpcl	$⊢ y \in ℝ \to ψ (y) \in ℝ$
53	51 52	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to ψ (y) \in ℝ$
54	53 51	readdcld	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to ψ (y) + y \in ℝ$
55	6	a1i	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to 1 \in ℝ^{+}$
56		simprr	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to 1 \leq y$
57	51 55 56	rpgecld	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to y \in ℝ^{+}$
58	57	relogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to \log y \in ℝ$
59	54 58	remulcld	$⊢ ((A \in ℝ \land 1 \leq A) \land (y \in ℝ \land 1 \leq y)) \to (ψ (y) + y) \log y \in ℝ$
60	40	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \in ℝ$
61	53	ad2ant2r	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (y) \in ℝ$
62		simprll	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ$
63	61 62	readdcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (y) + y \in ℝ$
64	57	ad2ant2r	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℝ^{+}$
65	64	relogcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log y \in ℝ$
66	63 65	remulcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (ψ (y) + y) \log y \in ℝ$
67	13	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ^{+}$
68	66 67	rerpdivcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{(ψ (y) + y) \log y}{x} \in ℝ$
69	16	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to R (x) \in ℝ$
70	69	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to R (x) \in ℂ$
71	70	abscld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \in ℝ$
72	67	relogcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℝ$
73	71 72	remulcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \log x \in ℝ$
74	24	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{2}{\log x} \in ℝ$
75	37	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
76	74 75	remulcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
77	73 76	resubcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \in ℝ$
78	21	a1i	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \in ℝ$
79	5	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℝ$
80	11	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 < x$
81	79 80	rplogcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \in ℝ^{+}$
82		2rp	$⊢ 2 \in ℝ^{+}$
83	82	a1i	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 2 \in ℝ^{+}$
84	83	rpge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq 2$
85	78 81 84	divge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \frac{2}{\log x}$
86		fzfid	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (1 \dots ⌊\frac{x}{A}⌋) \in Fin$
87	36	adantlr	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \|R (\frac{x}{n})\| \log n \in ℝ$
88	33	adantlr	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to R (\frac{x}{n}) \in ℂ$
89	88	abscld	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \|R (\frac{x}{n})\| \in ℝ$
90	29	adantlr	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℝ^{+}$
91	90	relogcld	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to \log n \in ℝ$
92	88	absge0d	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to 0 \leq \|R (\frac{x}{n})\|$
93	90	rpred	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℝ$
94	27	adantl	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to n \in ℕ$
95	94	nnge1d	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to 1 \leq n$
96	93 95	logge0d	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to 0 \leq \log n$
97	89 91 92 96	mulge0d	$⊢ ((((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \land n \in (1 \dots ⌊\frac{x}{A}⌋)) \to 0 \leq \|R (\frac{x}{n})\| \log n$
98	86 87 97	fsumge0	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
99	74 75 85 98	mulge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n$
100	73 76	subge02d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (0 \leq (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \leftrightarrow \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \leq \|R (x)\| \log x)$
101	99 100	mpbid	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \leq \|R (x)\| \log x$
102	70	absge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \|R (x)\|$
103	81	rpge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \log x$
104		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
105	79 104	syl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (x) \in ℝ$
106	105 79	readdcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (x) + x \in ℝ$
107	1	pntrval	$⊢ x \in ℝ^{+} \to R (x) = ψ (x) - x$
108	67 107	syl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to R (x) = ψ (x) - x$
109	108	fveq2d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| = \|ψ (x) - x\|$
110	105	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (x) \in ℂ$
111	79	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \in ℂ$
112	110 111	abs2dif2d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|ψ (x) - x\| \leq \|ψ (x)\| + \|x\|$
113		chpge0	$⊢ x \in ℝ \to 0 \leq ψ (x)$
114	79 113	syl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq ψ (x)$
115	105 114	absidd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|ψ (x)\| = ψ (x)$
116	67	rpge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq x$
117	79 116	absidd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|x\| = x$
118	115 117	oveq12d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|ψ (x)\| + \|x\| = ψ (x) + x$
119	112 118	breqtrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|ψ (x) - x\| \leq ψ (x) + x$
120	109 119	eqbrtrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \leq ψ (x) + x$
121		simprr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x < y$
122	79 62 121	ltled	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to x \leq y$
123		chpwordi	$⊢ (x \in ℝ \land y \in ℝ \land x \leq y) \to ψ (x) \leq ψ (y)$
124	79 62 122 123	syl3anc	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (x) \leq ψ (y)$
125	105 79 61 62 124 122	le2addd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (x) + x \leq ψ (y) + y$
126	71 106 63 120 125	letrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \leq ψ (y) + y$
127	67 64	logled	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (x \leq y \leftrightarrow \log x \leq \log y)$
128	122 127	mpbid	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log x \leq \log y$
129	71 63 72 65 102 103 126 128	lemul12ad	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \log x \leq (ψ (y) + y) \log y$
130	77 73 66 101 129	letrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n \leq (ψ (y) + y) \log y$
131	77 66 67 130	lediv1dd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \leq \frac{(ψ (y) + y) \log y}{x}$
132	6	a1i	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \in ℝ^{+}$
133		chpge0	$⊢ y \in ℝ \to 0 \leq ψ (y)$
134	62 133	syl	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq ψ (y)$
135	64	rpge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq y$
136	61 62 134 135	addge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq ψ (y) + y$
137		simprlr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \leq y$
138	62 137	logge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq \log y$
139	63 65 136 138	mulge0d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 0 \leq (ψ (y) + y) \log y$
140	12	adantr	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to 1 \leq x$
141	132 67 66 139 140	lediv2ad	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{(ψ (y) + y) \log y}{x} \leq \frac{(ψ (y) + y) \log y}{1}$
142	61	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (y) \in ℂ$
143	62	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to y \in ℂ$
144	142 143	addcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to ψ (y) + y \in ℂ$
145	65	recnd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \log y \in ℂ$
146	144 145	mulcld	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to (ψ (y) + y) \log y \in ℂ$
147	146	div1d	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{(ψ (y) + y) \log y}{1} = (ψ (y) + y) \log y$
148	141 147	breqtrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{(ψ (y) + y) \log y}{x} \leq (ψ (y) + y) \log y$
149	60 68 66 131 148	letrd	$⊢ (((A \in ℝ \land 1 \leq A) \land x \in (1, +∞)) \land ((y \in ℝ \land 1 \leq y) \land x < y)) \to \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \leq (ψ (y) + y) \log y$
150	3 4 40 50 59 149	lo1bddrp	$⊢ (A \in ℝ \land 1 \leq A) \to \exists c \in ℝ^{+} \forall x \in (1, +∞) \frac{\|R (x)\| \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊\frac{x}{A}⌋} \|R (\frac{x}{n})\| \log n}{x} \leq c$

Metamath Proof Explorer

Theorem pntrlog2bnd

Proof