pntrsumo1

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 25-May-2016)

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntrsumo1	$⊢ (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		1re	$⊢ 1 \in ℝ$
3		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
4	2 3	ax-mp	$⊢ x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x)$
5	4	simplbi	$⊢ x \in [1, +∞) \to x \in ℝ$
6		0red	$⊢ x \in [1, +∞) \to 0 \in ℝ$
7		1red	$⊢ x \in [1, +∞) \to 1 \in ℝ$
8		0lt1	$⊢ 0 < 1$
9	8	a1i	$⊢ x \in [1, +∞) \to 0 < 1$
10	4	simprbi	$⊢ x \in [1, +∞) \to 1 \leq x$
11	6 7 5 9 10	ltletrd	$⊢ x \in [1, +∞) \to 0 < x$
12	5 11	elrpd	$⊢ x \in [1, +∞) \to x \in ℝ^{+}$
13	12	ssriv	$⊢ [1, +∞) \subseteq ℝ^{+}$
14	13	a1i	$⊢ ⊤ \to [1, +∞) \subseteq ℝ^{+}$
15		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
16	14 15	sstrdi	$⊢ ⊤ \to [1, +∞) \subseteq ℝ$
17	16	resmptd	$⊢ ⊤ \to {(x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) ↾}_{[1, +∞)} = (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}))$
18		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
19	5 18	syl	$⊢ x \in [1, +∞) \to ψ (x) \in ℝ$
20		peano2re	$⊢ ψ (x) \in ℝ \to ψ (x) + 1 \in ℝ$
21	19 20	syl	$⊢ x \in [1, +∞) \to ψ (x) + 1 \in ℝ$
22	12	rprege0d	$⊢ x \in [1, +∞) \to (x \in ℝ \land 0 \leq x)$
23		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
24	22 23	syl	$⊢ x \in [1, +∞) \to ⌊x⌋ \in ℕ_{0}$
25		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
26	24 25	syl	$⊢ x \in [1, +∞) \to ⌊x⌋ + 1 \in ℕ$
27	21 26	nndivred	$⊢ x \in [1, +∞) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℝ$
28	27	recnd	$⊢ x \in [1, +∞) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℂ$
29		ax-1cn	$⊢ 1 \in ℂ$
30		subcl	$⊢ (\frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℂ \land 1 \in ℂ) \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 \in ℂ$
31	28 29 30	sylancl	$⊢ x \in [1, +∞) \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 \in ℂ$
32		fzfid	$⊢ x \in ℝ \to (1 \dots ⌊x⌋) \in Fin$
33		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
34	33	adantl	$⊢ (x \in ℝ \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
35		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
36	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
37	36	ffvelcdmi	$⊢ n \in ℝ^{+} \to R (n) \in ℝ$
38	35 37	syl	$⊢ n \in ℕ \to R (n) \in ℝ$
39		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
40		nnmulcl	$⊢ (n \in ℕ \land n + 1 \in ℕ) \to n (n + 1) \in ℕ$
41	39 40	mpdan	$⊢ n \in ℕ \to n (n + 1) \in ℕ$
42	38 41	nndivred	$⊢ n \in ℕ \to \frac{R (n)}{n (n + 1)} \in ℝ$
43	34 42	syl	$⊢ (x \in ℝ \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
44	32 43	fsumrecl	$⊢ x \in ℝ \to \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}) \in ℝ$
45	44	recnd	$⊢ x \in ℝ \to \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}) \in ℂ$
46	5 45	syl	$⊢ x \in [1, +∞) \to \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}) \in ℂ$
47		oveq2	$⊢ m = n \to \frac{1}{m} = \frac{1}{n}$
48		fvoveq1	$⊢ m = n \to ψ (m - 1) = ψ (n - 1)$
49		oveq1	$⊢ m = n \to m - 1 = n - 1$
50	48 49	oveq12d	$⊢ m = n \to ψ (m - 1) - (m - 1) = ψ (n - 1) - (n - 1)$
51	47 50	jca	$⊢ m = n \to (\frac{1}{m} = \frac{1}{n} \land ψ (m - 1) - (m - 1) = ψ (n - 1) - (n - 1))$
52		oveq2	$⊢ m = n + 1 \to \frac{1}{m} = \frac{1}{n + 1}$
53		fvoveq1	$⊢ m = n + 1 \to ψ (m - 1) = ψ (n + 1 - 1)$
54		oveq1	$⊢ m = n + 1 \to m - 1 = n + 1 - 1$
55	53 54	oveq12d	$⊢ m = n + 1 \to ψ (m - 1) - (m - 1) = ψ (n + 1 - 1) - (n + 1 - 1)$
56	52 55	jca	$⊢ m = n + 1 \to (\frac{1}{m} = \frac{1}{n + 1} \land ψ (m - 1) - (m - 1) = ψ (n + 1 - 1) - (n + 1 - 1))$
57		oveq2	$⊢ m = 1 \to \frac{1}{m} = \frac{1}{1}$
58		1div1e1	$⊢ \frac{1}{1} = 1$
59	57 58	eqtrdi	$⊢ m = 1 \to \frac{1}{m} = 1$
60		oveq1	$⊢ m = 1 \to m - 1 = 1 - 1$
61		1m1e0	$⊢ 1 - 1 = 0$
62	60 61	eqtrdi	$⊢ m = 1 \to m - 1 = 0$
63	62	fveq2d	$⊢ m = 1 \to ψ (m - 1) = ψ (0)$
64		2pos	$⊢ 0 < 2$
65		0re	$⊢ 0 \in ℝ$
66		chpeq0	$⊢ 0 \in ℝ \to (ψ (0) = 0 \leftrightarrow 0 < 2)$
67	65 66	ax-mp	$⊢ ψ (0) = 0 \leftrightarrow 0 < 2$
68	64 67	mpbir	$⊢ ψ (0) = 0$
69	63 68	eqtrdi	$⊢ m = 1 \to ψ (m - 1) = 0$
70	69 62	oveq12d	$⊢ m = 1 \to ψ (m - 1) - (m - 1) = 0 - 0$
71		0m0e0	$⊢ 0 - 0 = 0$
72	70 71	eqtrdi	$⊢ m = 1 \to ψ (m - 1) - (m - 1) = 0$
73	59 72	jca	$⊢ m = 1 \to (\frac{1}{m} = 1 \land ψ (m - 1) - (m - 1) = 0)$
74		oveq2	$⊢ m = ⌊x⌋ + 1 \to \frac{1}{m} = \frac{1}{⌊x⌋ + 1}$
75		fvoveq1	$⊢ m = ⌊x⌋ + 1 \to ψ (m - 1) = ψ (⌊x⌋ + 1 - 1)$
76		oveq1	$⊢ m = ⌊x⌋ + 1 \to m - 1 = ⌊x⌋ + 1 - 1$
77	75 76	oveq12d	$⊢ m = ⌊x⌋ + 1 \to ψ (m - 1) - (m - 1) = ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)$
78	74 77	jca	$⊢ m = ⌊x⌋ + 1 \to (\frac{1}{m} = \frac{1}{⌊x⌋ + 1} \land ψ (m - 1) - (m - 1) = ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1))$
79		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
80	26 79	eleqtrdi	$⊢ x \in [1, +∞) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
81		elfznn	$⊢ m \in (1 \dots ⌊x⌋ + 1) \to m \in ℕ$
82	81	adantl	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℕ$
83	82	nnrecred	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to \frac{1}{m} \in ℝ$
84	83	recnd	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to \frac{1}{m} \in ℂ$
85	82	nnred	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℝ$
86		peano2rem	$⊢ m \in ℝ \to m - 1 \in ℝ$
87	85 86	syl	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to m - 1 \in ℝ$
88		chpcl	$⊢ m - 1 \in ℝ \to ψ (m - 1) \in ℝ$
89	87 88	syl	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (m - 1) \in ℝ$
90	89 87	resubcld	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (m - 1) - (m - 1) \in ℝ$
91	90	recnd	$⊢ (x \in [1, +∞) \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (m - 1) - (m - 1) \in ℂ$
92	51 56 73 78 80 84 91	fsumparts	$⊢ x \in [1, +∞) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (\frac{1}{n}) (ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1))) = (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) - 1 \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1))$
93	5	flcld	$⊢ x \in [1, +∞) \to ⌊x⌋ \in ℤ$
94		fzval3	$⊢ ⌊x⌋ \in ℤ \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
95	93 94	syl	$⊢ x \in [1, +∞) \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
96	95	eqcomd	$⊢ x \in [1, +∞) \to (1 ..^⌊x⌋ + 1) = (1 \dots ⌊x⌋)$
97	33	adantl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
98	97	nncnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
99		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
100	98 29 99	sylancl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 = n$
101	97	nnred	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
102	100 101	eqeltrd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 \in ℝ$
103		chpcl	$⊢ n + 1 - 1 \in ℝ \to ψ (n + 1 - 1) \in ℝ$
104	102 103	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) \in ℝ$
105	104	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) \in ℂ$
106	102	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 \in ℂ$
107		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
108	101 107	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℝ$
109		chpcl	$⊢ n - 1 \in ℝ \to ψ (n - 1) \in ℝ$
110	108 109	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) \in ℝ$
111	110	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) \in ℂ$
112		1cnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
113	98 112	subcld	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℂ$
114	105 106 111 113	sub4d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1)) = ψ (n + 1 - 1) - ψ (n - 1) - ((n + 1) - 1 - (n - 1))$
115		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
116	97 115	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
117	116	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
118		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
119	97 118	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℕ_{0}$
120		chpp1	$⊢ n - 1 \in ℕ_{0} \to ψ (n - 1 + 1) = ψ (n - 1) + Λ (n - 1 + 1)$
121	119 120	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1 + 1) = ψ (n - 1) + Λ (n - 1 + 1)$
122		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
123	98 29 122	sylancl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n - 1 + 1 = n$
124	123 100	eqtr4d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n - 1 + 1 = n + 1 - 1$
125	124	fveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1 + 1) = ψ (n + 1 - 1)$
126	123	fveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to Λ (n - 1 + 1) = Λ (n)$
127	126	oveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) + Λ (n - 1 + 1) = ψ (n - 1) + Λ (n)$
128	121 125 127	3eqtr3d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) = ψ (n - 1) + Λ (n)$
129	111 117 128	mvrladdd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - ψ (n - 1) = Λ (n)$
130		peano2cn	$⊢ n \in ℂ \to n + 1 \in ℂ$
131	98 130	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℂ$
132	131 98 112	nnncan2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (n + 1) - 1 - (n - 1) = n + 1 - n$
133		pncan2	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - n = 1$
134	98 29 133	sylancl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - n = 1$
135	132 134	eqtrd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (n + 1) - 1 - (n - 1) = 1$
136	129 135	oveq12d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - ψ (n - 1) - ((n + 1) - 1 - (n - 1)) = Λ (n) - 1$
137	114 136	eqtrd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1)) = Λ (n) - 1$
138	137	oveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (\frac{1}{n}) (ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1))) = (\frac{1}{n}) (Λ (n) - 1)$
139		peano2rem	$⊢ Λ (n) \in ℝ \to Λ (n) - 1 \in ℝ$
140	116 139	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) - 1 \in ℝ$
141	140	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) - 1 \in ℂ$
142	97	nnne0d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
143	141 98 142	divrec2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) - 1}{n} = (\frac{1}{n}) (Λ (n) - 1)$
144	138 143	eqtr4d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (\frac{1}{n}) (ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1))) = \frac{Λ (n) - 1}{n}$
145	96 144	sumeq12rdv	$⊢ x \in [1, +∞) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (\frac{1}{n}) (ψ (n + 1 - 1) - (n + 1 - 1) - (ψ (n - 1) - (n - 1))) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n})$
146	24	nn0cnd	$⊢ x \in [1, +∞) \to ⌊x⌋ \in ℂ$
147		pncan	$⊢ (⌊x⌋ \in ℂ \land 1 \in ℂ) \to ⌊x⌋ + 1 - 1 = ⌊x⌋$
148	146 29 147	sylancl	$⊢ x \in [1, +∞) \to ⌊x⌋ + 1 - 1 = ⌊x⌋$
149	148	fveq2d	$⊢ x \in [1, +∞) \to ψ (⌊x⌋ + 1 - 1) = ψ (⌊x⌋)$
150		chpfl	$⊢ x \in ℝ \to ψ (⌊x⌋) = ψ (x)$
151	5 150	syl	$⊢ x \in [1, +∞) \to ψ (⌊x⌋) = ψ (x)$
152	149 151	eqtrd	$⊢ x \in [1, +∞) \to ψ (⌊x⌋ + 1 - 1) = ψ (x)$
153	152	oveq1d	$⊢ x \in [1, +∞) \to ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1) = ψ (x) - (⌊x⌋ + 1 - 1)$
154	19	recnd	$⊢ x \in [1, +∞) \to ψ (x) \in ℂ$
155	26	nncnd	$⊢ x \in [1, +∞) \to ⌊x⌋ + 1 \in ℂ$
156		1cnd	$⊢ x \in [1, +∞) \to 1 \in ℂ$
157	154 155 156	subsub3d	$⊢ x \in [1, +∞) \to ψ (x) - (⌊x⌋ + 1 - 1) = ψ (x) + 1 - (⌊x⌋ + 1)$
158	153 157	eqtrd	$⊢ x \in [1, +∞) \to ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1) = ψ (x) + 1 - (⌊x⌋ + 1)$
159	158	oveq2d	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) = (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1 - (⌊x⌋ + 1))$
160	26	nnrecred	$⊢ x \in [1, +∞) \to \frac{1}{⌊x⌋ + 1} \in ℝ$
161	160	recnd	$⊢ x \in [1, +∞) \to \frac{1}{⌊x⌋ + 1} \in ℂ$
162		peano2cn	$⊢ ψ (x) \in ℂ \to ψ (x) + 1 \in ℂ$
163	154 162	syl	$⊢ x \in [1, +∞) \to ψ (x) + 1 \in ℂ$
164	161 163 155	subdid	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1 - (⌊x⌋ + 1)) = (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1) - (\frac{1}{⌊x⌋ + 1}) (⌊x⌋ + 1)$
165	26	nnne0d	$⊢ x \in [1, +∞) \to ⌊x⌋ + 1 \neq 0$
166	163 155 165	divrec2d	$⊢ x \in [1, +∞) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} = (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1)$
167	166	eqcomd	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1) = \frac{ψ (x) + 1}{⌊x⌋ + 1}$
168	155 165	recid2d	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (⌊x⌋ + 1) = 1$
169	167 168	oveq12d	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (x) + 1) - (\frac{1}{⌊x⌋ + 1}) (⌊x⌋ + 1) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1$
170	159 164 169	3eqtrd	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1$
171	29	mul01i	$⊢ 1 \cdot 0 = 0$
172	171	a1i	$⊢ x \in [1, +∞) \to 1 \cdot 0 = 0$
173	170 172	oveq12d	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) - 1 \cdot 0 = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 - 0$
174	31	subid1d	$⊢ x \in [1, +∞) \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 - 0 = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1$
175	173 174	eqtrd	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) - 1 \cdot 0 = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1$
176	97 41	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n (n + 1) \in ℕ$
177	176	nnrecred	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n (n + 1)} \in ℝ$
178	177	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n (n + 1)} \in ℂ$
179	97 38	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to R (n) \in ℝ$
180	179	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to R (n) \in ℂ$
181	178 180	mulneg1d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (- \frac{1}{n (n + 1)}) R (n) = - (\frac{1}{n (n + 1)}) R (n)$
182	98 112	mulcld	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \cdot 1 \in ℂ$
183	98 131	mulcld	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n (n + 1) \in ℂ$
184	176	nnne0d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n (n + 1) \neq 0$
185	131 182 183 184	divsubdird	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{n + 1 - n \cdot 1}{n (n + 1)} = (\frac{n + 1}{n (n + 1)}) - (\frac{n \cdot 1}{n (n + 1)})$
186	98	mulridd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \cdot 1 = n$
187	186	oveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - n \cdot 1 = n + 1 - n$
188	187 134	eqtrd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - n \cdot 1 = 1$
189	188	oveq1d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{n + 1 - n \cdot 1}{n (n + 1)} = \frac{1}{n (n + 1)}$
190	131	mulridd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (n + 1) \cdot 1 = n + 1$
191	131 98	mulcomd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (n + 1) n = n (n + 1)$
192	190 191	oveq12d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{(n + 1) \cdot 1}{(n + 1) n} = \frac{n + 1}{n (n + 1)}$
193	97 39	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \in ℕ$
194	193	nnne0d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 \neq 0$
195	112 98 131 142 194	divcan5d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{(n + 1) \cdot 1}{(n + 1) n} = \frac{1}{n}$
196	192 195	eqtr3d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{n + 1}{n (n + 1)} = \frac{1}{n}$
197	112 131 98 194 142	divcan5d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{n \cdot 1}{n (n + 1)} = \frac{1}{n + 1}$
198	196 197	oveq12d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (\frac{n + 1}{n (n + 1)}) - (\frac{n \cdot 1}{n (n + 1)}) = (\frac{1}{n}) - (\frac{1}{n + 1})$
199	185 189 198	3eqtr3d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n (n + 1)} = (\frac{1}{n}) - (\frac{1}{n + 1})$
200	199	negeqd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to - \frac{1}{n (n + 1)} = - ((\frac{1}{n}) - (\frac{1}{n + 1}))$
201	97	nnrecred	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
202	201	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
203	193	nnrecred	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n + 1} \in ℝ$
204	203	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n + 1} \in ℂ$
205	202 204	negsubdi2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to - ((\frac{1}{n}) - (\frac{1}{n + 1})) = (\frac{1}{n + 1}) - (\frac{1}{n})$
206	200 205	eqtr2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to (\frac{1}{n + 1}) - (\frac{1}{n}) = - \frac{1}{n (n + 1)}$
207	97	nnrpd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
208	100 207	eqeltrd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 \in ℝ^{+}$
209	1	pntrval	$⊢ n + 1 - 1 \in ℝ^{+} \to R (n + 1 - 1) = ψ (n + 1 - 1) - (n + 1 - 1)$
210	208 209	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to R (n + 1 - 1) = ψ (n + 1 - 1) - (n + 1 - 1)$
211	100	fveq2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to R (n + 1 - 1) = R (n)$
212	210 211	eqtr3d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - (n + 1 - 1) = R (n)$
213	206 212	oveq12d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1)) = (- \frac{1}{n (n + 1)}) R (n)$
214	180 183 184	divrec2d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} = (\frac{1}{n (n + 1)}) R (n)$
215	214	negeqd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to - \frac{R (n)}{n (n + 1)} = - (\frac{1}{n (n + 1)}) R (n)$
216	181 213 215	3eqtr4d	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1)) = - \frac{R (n)}{n (n + 1)}$
217	96 216	sumeq12rdv	$⊢ x \in [1, +∞) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1)) = \sum_{n = 1}^{⌊x⌋} (- \frac{R (n)}{n (n + 1)})$
218		fzfid	$⊢ x \in [1, +∞) \to (1 \dots ⌊x⌋) \in Fin$
219	97 42	syl	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
220	219	recnd	$⊢ (x \in [1, +∞) \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
221	218 220	fsumneg	$⊢ x \in [1, +∞) \to \sum_{n = 1}^{⌊x⌋} (- \frac{R (n)}{n (n + 1)}) = - \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})$
222	217 221	eqtrd	$⊢ x \in [1, +∞) \to \sum_{n \in (1 ..^⌊x⌋ + 1)} ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1)) = - \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})$
223	175 222	oveq12d	$⊢ x \in [1, +∞) \to (\frac{1}{⌊x⌋ + 1}) (ψ (⌊x⌋ + 1 - 1) - (⌊x⌋ + 1 - 1)) - 1 \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} ((\frac{1}{n + 1}) - (\frac{1}{n})) (ψ (n + 1 - 1) - (n + 1 - 1)) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 - (- \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}))$
224	92 145 223	3eqtr3d	$⊢ x \in [1, +∞) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 - (- \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}))$
225	31 46	subnegd	$⊢ x \in [1, +∞) \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 - (- \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 + \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})$
226	224 225	eqtrd	$⊢ x \in [1, +∞) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) = (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 + \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})$
227	31 46 226	mvrladdd	$⊢ x \in [1, +∞) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) - ((\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1) = \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})$
228	227	mpteq2ia	$⊢ (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) - ((\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1)) = (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}))$
229		fzfid	$⊢ (⊤ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
230	33	adantl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
231	230 115	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
232	231 139	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) - 1 \in ℝ$
233	232 230	nndivred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) - 1}{n} \in ℝ$
234	229 233	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) \in ℝ$
235		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
236	235	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ$
237	236 18	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ψ (x) \in ℝ$
238	237 20	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ψ (x) + 1 \in ℝ$
239		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
240	239 23	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℕ_{0}$
241	240	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℕ_{0}$
242	241 25	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℕ$
243	238 242	nndivred	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℝ$
244		peano2rem	$⊢ \frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℝ \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 \in ℝ$
245	243 244	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1 \in ℝ$
246		reex	$⊢ ℝ \in V$
247	246 15	ssexi	$⊢ ℝ^{+} \in V$
248	247	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
249	231 230	nndivred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
250	249	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
251	229 250	fsumcl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
252		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
253	252	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℝ$
254	253	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℂ$
255	251 254	subcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
256	230	nnrecred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℝ$
257	229 256	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℝ$
258	257 253	resubcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x \in ℝ$
259		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x)$
260		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x)$
261	248 255 258 259 260	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x))$
262	256	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{1}{n} \in ℂ$
263	229 250 262	fsumsub	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) - (\frac{1}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{1}{n})$
264	231	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
265		1cnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
266	230	nncnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
267	230	nnne0d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
268	264 265 266 267	divsubdird	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) - 1}{n} = (\frac{Λ (n)}{n}) - (\frac{1}{n})$
269	268	sumeq2dv	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) = \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) - (\frac{1}{n}))$
270	257	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \in ℂ$
271	251 270 254	nnncan2d	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{1}{n})$
272	263 269 271	3eqtr4rd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n})$
273	272	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}))$
274	261 273	eqtrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}))$
275		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
276	15	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
277	258	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x \in ℂ$
278		1red	$⊢ ⊤ \to 1 \in ℝ$
279		harmoniclbnd	$⊢ x \in ℝ^{+} \to \log x \leq \sum_{n = 1}^{⌊x⌋} (\frac{1}{n})$
280	279	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \leq \sum_{n = 1}^{⌊x⌋} (\frac{1}{n})$
281	253 257 280	abssubge0d	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x\| = \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x$
282	281	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x\| = \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x$
283	235	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
284		simprr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
285		harmonicubnd	$⊢ (x \in ℝ \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
286	283 284 285	syl2anc	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1$
287		1red	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℝ$
288	257 253 287	lesubadd2d	$⊢ (⊤ \land x \in ℝ^{+}) \to (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x \leq 1 \leftrightarrow \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1)$
289	288	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x \leq 1 \leftrightarrow \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) \leq \log x + 1)$
290	286 289	mpbird	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x \leq 1$
291	282 290	eqbrtrd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x\| \leq 1$
292	276 277 278 278 291	elo1d	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) \in 𝑂 (1)$
293		o1sub	$⊢ ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) \in 𝑂 (1)$
294	275 292 293	sylancr	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{n}) - \log x) \in 𝑂 (1)$
295	274 294	eqeltrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n})) \in 𝑂 (1)$
296	243	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \in ℂ$
297		1cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℂ$
298	237	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to ψ (x) \in ℂ$
299		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
300	299	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℂ \land x \neq 0)$
301		divdir	$⊢ (ψ (x) \in ℂ \land 1 \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{ψ (x) + 1}{x} = (\frac{ψ (x)}{x}) + (\frac{1}{x})$
302	298 297 300 301	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{x} = (\frac{ψ (x)}{x}) + (\frac{1}{x})$
303	302	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x) + 1}{x}) = (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) + (\frac{1}{x}))$
304		simpr	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
305	237 304	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
306		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
307	306	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{+}$
308		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) = (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x})$
309		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) = (x \in ℝ^{+} ⟼ \frac{1}{x})$
310	248 305 307 308 309	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) = (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) + (\frac{1}{x}))$
311		chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
312		divrcnv	$⊢ 1 \in ℂ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
313	29 312	ax-mp	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
314		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0 \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
315	313 314	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
316		o1add	$⊢ ((x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
317	311 315 316	sylancr	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) +_{f} (x \in ℝ^{+} ⟼ \frac{1}{x}) \in 𝑂 (1)$
318	310 317	eqeltrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) + (\frac{1}{x})) \in 𝑂 (1)$
319	303 318	eqeltrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x) + 1}{x}) \in 𝑂 (1)$
320	238 304	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{x} \in ℝ$
321		chpge0	$⊢ x \in ℝ \to 0 \leq ψ (x)$
322	236 321	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to 0 \leq ψ (x)$
323	237 322	ge0p1rpd	$⊢ (⊤ \land x \in ℝ^{+}) \to ψ (x) + 1 \in ℝ^{+}$
324	323	rprege0d	$⊢ (⊤ \land x \in ℝ^{+}) \to (ψ (x) + 1 \in ℝ \land 0 \leq ψ (x) + 1)$
325	242	nnrpd	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℝ^{+}$
326	325	rpregt0d	$⊢ (⊤ \land x \in ℝ^{+}) \to (⌊x⌋ + 1 \in ℝ \land 0 < ⌊x⌋ + 1)$
327		divge0	$⊢ ((ψ (x) + 1 \in ℝ \land 0 \leq ψ (x) + 1) \land (⌊x⌋ + 1 \in ℝ \land 0 < ⌊x⌋ + 1)) \to 0 \leq \frac{ψ (x) + 1}{⌊x⌋ + 1}$
328	324 326 327	syl2anc	$⊢ (⊤ \land x \in ℝ^{+}) \to 0 \leq \frac{ψ (x) + 1}{⌊x⌋ + 1}$
329	243 328	absidd	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\frac{ψ (x) + 1}{⌊x⌋ + 1}\| = \frac{ψ (x) + 1}{⌊x⌋ + 1}$
330	320	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{x} \in ℂ$
331	330	abscld	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\frac{ψ (x) + 1}{x}\| \in ℝ$
332		fllep1	$⊢ x \in ℝ \to x \leq ⌊x⌋ + 1$
333	236 332	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to x \leq ⌊x⌋ + 1$
334		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
335	334	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 < x)$
336	323	rpregt0d	$⊢ (⊤ \land x \in ℝ^{+}) \to (ψ (x) + 1 \in ℝ \land 0 < ψ (x) + 1)$
337		lediv2	$⊢ ((x \in ℝ \land 0 < x) \land (⌊x⌋ + 1 \in ℝ \land 0 < ⌊x⌋ + 1) \land (ψ (x) + 1 \in ℝ \land 0 < ψ (x) + 1)) \to (x \leq ⌊x⌋ + 1 \leftrightarrow \frac{ψ (x) + 1}{⌊x⌋ + 1} \leq \frac{ψ (x) + 1}{x})$
338	335 326 336 337	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \leq ⌊x⌋ + 1 \leftrightarrow \frac{ψ (x) + 1}{⌊x⌋ + 1} \leq \frac{ψ (x) + 1}{x})$
339	333 338	mpbid	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \leq \frac{ψ (x) + 1}{x}$
340	320	leabsd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{x} \leq \|\frac{ψ (x) + 1}{x}\|$
341	243 320 331 339 340	letrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x) + 1}{⌊x⌋ + 1} \leq \|\frac{ψ (x) + 1}{x}\|$
342	329 341	eqbrtrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\frac{ψ (x) + 1}{⌊x⌋ + 1}\| \leq \|\frac{ψ (x) + 1}{x}\|$
343	342	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{ψ (x) + 1}{⌊x⌋ + 1}\| \leq \|\frac{ψ (x) + 1}{x}\|$
344	278 319 320 296 343	o1le	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x) + 1}{⌊x⌋ + 1}) \in 𝑂 (1)$
345		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 1 \in ℂ) \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
346	15 29 345	mp2an	$⊢ (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
347	346	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
348	296 297 344 347	o1sub2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1) \in 𝑂 (1)$
349	234 245 295 348	o1sub2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) - ((\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1)) \in 𝑂 (1)$
350	14 349	o1res2	$⊢ ⊤ \to (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) - 1}{n}) - ((\frac{ψ (x) + 1}{⌊x⌋ + 1}) - 1)) \in 𝑂 (1)$
351	228 350	eqeltrrid	$⊢ ⊤ \to (x \in [1, +∞) ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$
352	17 351	eqeltrd	$⊢ ⊤ \to {(x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) ↾}_{[1, +∞)} \in 𝑂 (1)$
353		eqid	$⊢ (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) = (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)}))$
354	353 45	fmpti	$⊢ (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) : ℝ ⟶ ℂ$
355	354	a1i	$⊢ ⊤ \to (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) : ℝ ⟶ ℂ$
356		ssidd	$⊢ ⊤ \to ℝ \subseteq ℝ$
357	355 356 278	o1resb	$⊢ ⊤ \to ((x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1) \leftrightarrow {(x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) ↾}_{[1, +∞)} \in 𝑂 (1))$
358	352 357	mpbird	$⊢ ⊤ \to (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$
359	358	mptru	$⊢ (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem pntrsumo1

Proof