selberg2lem

Description: Lemma for selberg2 . Equation 10.4.12 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

		Ref	Expression
	Assertion	selberg2lem	$⊢ (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
2		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
3	1 2	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
4	3	recnd	$⊢ x \in ℝ^{+} \to ψ (x) \in ℂ$
5		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
6		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
7	5 6	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℕ_{0}$
8		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
9	7 8	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ + 1 \in ℕ$
10	9	nnrpd	$⊢ x \in ℝ^{+} \to ⌊x⌋ + 1 \in ℝ^{+}$
11	10	relogcld	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) \in ℝ$
12	11	recnd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) \in ℂ$
13		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
14	13	recnd	$⊢ x \in ℝ^{+} \to \log x \in ℂ$
15	12 14	subcld	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) - \log x \in ℂ$
16	4 15	mulcld	$⊢ x \in ℝ^{+} \to ψ (x) (\log (⌊x⌋ + 1) - \log x) \in ℂ$
17		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
18		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
19	18	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
20	19	nnrpd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
21		1rp	$⊢ 1 \in ℝ^{+}$
22		rpaddcl	$⊢ (n \in ℝ^{+} \land 1 \in ℝ^{+}) \to n + 1 \in ℝ^{+}$
23	21 22	mpan2	$⊢ n \in ℝ^{+} \to n + 1 \in ℝ^{+}$
24	23	relogcld	$⊢ n \in ℝ^{+} \to \log (n + 1) \in ℝ$
25		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
26	24 25	resubcld	$⊢ n \in ℝ^{+} \to \log (n + 1) - \log n \in ℝ$
27		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
28		chpcl	$⊢ n \in ℝ \to ψ (n) \in ℝ$
29	27 28	syl	$⊢ n \in ℝ^{+} \to ψ (n) \in ℝ$
30	26 29	remulcld	$⊢ n \in ℝ^{+} \to (\log (n + 1) - \log n) ψ (n) \in ℝ$
31	30	recnd	$⊢ n \in ℝ^{+} \to (\log (n + 1) - \log n) ψ (n) \in ℂ$
32	20 31	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\log (n + 1) - \log n) ψ (n) \in ℂ$
33	17 32	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) \in ℂ$
34		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
35		divsubdir	$⊢ (ψ (x) (\log (⌊x⌋ + 1) - \log x) \in ℂ \land \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{ψ (x) (\log (⌊x⌋ + 1) - \log x) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x} = (\frac{ψ (x) (\log (⌊x⌋ + 1) - \log x)}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x})$
36	16 33 34 35	syl3anc	$⊢ x \in ℝ^{+} \to \frac{ψ (x) (\log (⌊x⌋ + 1) - \log x) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x} = (\frac{ψ (x) (\log (⌊x⌋ + 1) - \log x)}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x})$
37	4 12	mulcld	$⊢ x \in ℝ^{+} \to ψ (x) \log (⌊x⌋ + 1) \in ℂ$
38	4 14	mulcld	$⊢ x \in ℝ^{+} \to ψ (x) \log x \in ℂ$
39	37 38 33	sub32d	$⊢ x \in ℝ^{+} \to ψ (x) \log (⌊x⌋ + 1) - ψ (x) \log x - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) = ψ (x) \log (⌊x⌋ + 1) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) - ψ (x) \log x$
40	4 12 14	subdid	$⊢ x \in ℝ^{+} \to ψ (x) (\log (⌊x⌋ + 1) - \log x) = ψ (x) \log (⌊x⌋ + 1) - ψ (x) \log x$
41	40	oveq1d	$⊢ x \in ℝ^{+} \to ψ (x) (\log (⌊x⌋ + 1) - \log x) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) = ψ (x) \log (⌊x⌋ + 1) - ψ (x) \log x - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)$
42		fveq2	$⊢ m = n \to \log m = \log n$
43		fvoveq1	$⊢ m = n \to ψ (m - 1) = ψ (n - 1)$
44	42 43	jca	$⊢ m = n \to (\log m = \log n \land ψ (m - 1) = ψ (n - 1))$
45		fveq2	$⊢ m = n + 1 \to \log m = \log (n + 1)$
46		fvoveq1	$⊢ m = n + 1 \to ψ (m - 1) = ψ (n + 1 - 1)$
47	45 46	jca	$⊢ m = n + 1 \to (\log m = \log (n + 1) \land ψ (m - 1) = ψ (n + 1 - 1))$
48		fveq2	$⊢ m = 1 \to \log m = \log 1$
49		log1	$⊢ \log 1 = 0$
50	48 49	eqtrdi	$⊢ m = 1 \to \log m = 0$
51		oveq1	$⊢ m = 1 \to m - 1 = 1 - 1$
52		1m1e0	$⊢ 1 - 1 = 0$
53	51 52	eqtrdi	$⊢ m = 1 \to m - 1 = 0$
54	53	fveq2d	$⊢ m = 1 \to ψ (m - 1) = ψ (0)$
55		2pos	$⊢ 0 < 2$
56		0re	$⊢ 0 \in ℝ$
57		chpeq0	$⊢ 0 \in ℝ \to (ψ (0) = 0 \leftrightarrow 0 < 2)$
58	56 57	ax-mp	$⊢ ψ (0) = 0 \leftrightarrow 0 < 2$
59	55 58	mpbir	$⊢ ψ (0) = 0$
60	54 59	eqtrdi	$⊢ m = 1 \to ψ (m - 1) = 0$
61	50 60	jca	$⊢ m = 1 \to (\log m = 0 \land ψ (m - 1) = 0)$
62		fveq2	$⊢ m = ⌊x⌋ + 1 \to \log m = \log (⌊x⌋ + 1)$
63		fvoveq1	$⊢ m = ⌊x⌋ + 1 \to ψ (m - 1) = ψ (⌊x⌋ + 1 - 1)$
64	62 63	jca	$⊢ m = ⌊x⌋ + 1 \to (\log m = \log (⌊x⌋ + 1) \land ψ (m - 1) = ψ (⌊x⌋ + 1 - 1))$
65		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
66	9 65	eleqtrdi	$⊢ x \in ℝ^{+} \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
67		elfznn	$⊢ m \in (1 \dots ⌊x⌋ + 1) \to m \in ℕ$
68	67	adantl	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℕ$
69	68	nnrpd	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℝ^{+}$
70	69	relogcld	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to \log m \in ℝ$
71	70	recnd	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to \log m \in ℂ$
72	68	nnred	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to m \in ℝ$
73		peano2rem	$⊢ m \in ℝ \to m - 1 \in ℝ$
74	72 73	syl	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to m - 1 \in ℝ$
75		chpcl	$⊢ m - 1 \in ℝ \to ψ (m - 1) \in ℝ$
76	74 75	syl	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (m - 1) \in ℝ$
77	76	recnd	$⊢ (x \in ℝ^{+} \land m \in (1 \dots ⌊x⌋ + 1)) \to ψ (m - 1) \in ℂ$
78	44 47 61 64 66 71 77	fsumparts	$⊢ x \in ℝ^{+} \to \sum_{n \in (1 ..^⌊x⌋ + 1)} \log n (ψ (n + 1 - 1) - ψ (n - 1)) = \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) - 0 \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} (\log (n + 1) - \log n) ψ (n + 1 - 1)$
79	7	nn0zd	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℤ$
80		fzval3	$⊢ ⌊x⌋ \in ℤ \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
81	79 80	syl	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) = (1 ..^⌊x⌋ + 1)$
82	81	eqcomd	$⊢ x \in ℝ^{+} \to (1 ..^⌊x⌋ + 1) = (1 \dots ⌊x⌋)$
83		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
84	19 83	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℕ_{0}$
85	84	nn0red	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n - 1 \in ℝ$
86		chpcl	$⊢ n - 1 \in ℝ \to ψ (n - 1) \in ℝ$
87	85 86	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) \in ℝ$
88	87	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) \in ℂ$
89		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
90	19 89	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
91	90	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
92	19	nncnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
93		ax-1cn	$⊢ 1 \in ℂ$
94		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
95	92 93 94	sylancl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 = n$
96		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
97	92 93 96	sylancl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n - 1 + 1 = n$
98	95 97	eqtr4d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n + 1 - 1 = n - 1 + 1$
99	98	fveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) = ψ (n - 1 + 1)$
100		chpp1	$⊢ n - 1 \in ℕ_{0} \to ψ (n - 1 + 1) = ψ (n - 1) + Λ (n - 1 + 1)$
101	84 100	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1 + 1) = ψ (n - 1) + Λ (n - 1 + 1)$
102	97	fveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n - 1 + 1) = Λ (n)$
103	102	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n - 1) + Λ (n - 1 + 1) = ψ (n - 1) + Λ (n)$
104	99 101 103	3eqtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) = ψ (n - 1) + Λ (n)$
105	88 91 104	mvrladdd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) - ψ (n - 1) = Λ (n)$
106	105	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n (ψ (n + 1 - 1) - ψ (n - 1)) = \log n Λ (n)$
107	20	relogcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
108	107	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
109	91 108	mulcomd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n = \log n Λ (n)$
110	106 109	eqtr4d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n (ψ (n + 1 - 1) - ψ (n - 1)) = Λ (n) \log n$
111	82 110	sumeq12rdv	$⊢ x \in ℝ^{+} \to \sum_{n \in (1 ..^⌊x⌋ + 1)} \log n (ψ (n + 1 - 1) - ψ (n - 1)) = \sum_{n = 1}^{⌊x⌋} Λ (n) \log n$
112	7	nn0cnd	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℂ$
113		pncan	$⊢ (⌊x⌋ \in ℂ \land 1 \in ℂ) \to ⌊x⌋ + 1 - 1 = ⌊x⌋$
114	112 93 113	sylancl	$⊢ x \in ℝ^{+} \to ⌊x⌋ + 1 - 1 = ⌊x⌋$
115	114	fveq2d	$⊢ x \in ℝ^{+} \to ψ (⌊x⌋ + 1 - 1) = ψ (⌊x⌋)$
116		chpfl	$⊢ x \in ℝ \to ψ (⌊x⌋) = ψ (x)$
117	1 116	syl	$⊢ x \in ℝ^{+} \to ψ (⌊x⌋) = ψ (x)$
118	115 117	eqtrd	$⊢ x \in ℝ^{+} \to ψ (⌊x⌋ + 1 - 1) = ψ (x)$
119	118	oveq2d	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) = \log (⌊x⌋ + 1) ψ (x)$
120	12 4	mulcomd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (x) = ψ (x) \log (⌊x⌋ + 1)$
121	119 120	eqtrd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) = ψ (x) \log (⌊x⌋ + 1)$
122		0cn	$⊢ 0 \in ℂ$
123	122	mul01i	$⊢ 0 \cdot 0 = 0$
124	123	a1i	$⊢ x \in ℝ^{+} \to 0 \cdot 0 = 0$
125	121 124	oveq12d	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) - 0 \cdot 0 = ψ (x) \log (⌊x⌋ + 1) - 0$
126	37	subid1d	$⊢ x \in ℝ^{+} \to ψ (x) \log (⌊x⌋ + 1) - 0 = ψ (x) \log (⌊x⌋ + 1)$
127	125 126	eqtrd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) - 0 \cdot 0 = ψ (x) \log (⌊x⌋ + 1)$
128	95	fveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (n + 1 - 1) = ψ (n)$
129	128	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\log (n + 1) - \log n) ψ (n + 1 - 1) = (\log (n + 1) - \log n) ψ (n)$
130	82 129	sumeq12rdv	$⊢ x \in ℝ^{+} \to \sum_{n \in (1 ..^⌊x⌋ + 1)} (\log (n + 1) - \log n) ψ (n + 1 - 1) = \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)$
131	127 130	oveq12d	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) ψ (⌊x⌋ + 1 - 1) - 0 \cdot 0 - \sum_{n \in (1 ..^⌊x⌋ + 1)} (\log (n + 1) - \log n) ψ (n + 1 - 1) = ψ (x) \log (⌊x⌋ + 1) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)$
132	78 111 131	3eqtr3d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) \log n = ψ (x) \log (⌊x⌋ + 1) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)$
133	132	oveq1d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x = ψ (x) \log (⌊x⌋ + 1) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) - ψ (x) \log x$
134	39 41 133	3eqtr4d	$⊢ x \in ℝ^{+} \to ψ (x) (\log (⌊x⌋ + 1) - \log x) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n) = \sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x$
135	134	oveq1d	$⊢ x \in ℝ^{+} \to \frac{ψ (x) (\log (⌊x⌋ + 1) - \log x) - \sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x} = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}$
136		div23	$⊢ (ψ (x) \in ℂ \land \log (⌊x⌋ + 1) - \log x \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{ψ (x) (\log (⌊x⌋ + 1) - \log x)}{x} = (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x)$
137	4 15 34 136	syl3anc	$⊢ x \in ℝ^{+} \to \frac{ψ (x) (\log (⌊x⌋ + 1) - \log x)}{x} = (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x)$
138	137	oveq1d	$⊢ x \in ℝ^{+} \to (\frac{ψ (x) (\log (⌊x⌋ + 1) - \log x)}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x}) = (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x})$
139	36 135 138	3eqtr3rd	$⊢ x \in ℝ^{+} \to (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x}) = \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}$
140	139	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x})) = (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x})$
141		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x) \in V$
142		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x} \in V$
143		reex	$⊢ ℝ \in V$
144		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
145	143 144	ssexi	$⊢ ℝ^{+} \in V$
146	145	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
147		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in V$
148	15	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log (⌊x⌋ + 1) - \log x \in ℂ$
149		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) = (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x})$
150		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) = (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x)$
151	146 147 148 149 150	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \times_{f} (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) = (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x))$
152		chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
153		0red	$⊢ ⊤ \to 0 \in ℝ$
154		1red	$⊢ ⊤ \to 1 \in ℝ$
155		divrcnv	$⊢ 1 \in ℂ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
156	93 155	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
157		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
158	157	rpred	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ$
159	158	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ$
160	11 13	resubcld	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) - \log x \in ℝ$
161	160	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log (⌊x⌋ + 1) - \log x \in ℝ$
162		rpaddcl	$⊢ (x \in ℝ^{+} \land 1 \in ℝ^{+}) \to x + 1 \in ℝ^{+}$
163	21 162	mpan2	$⊢ x \in ℝ^{+} \to x + 1 \in ℝ^{+}$
164	163	relogcld	$⊢ x \in ℝ^{+} \to \log (x + 1) \in ℝ$
165	164 13	resubcld	$⊢ x \in ℝ^{+} \to \log (x + 1) - \log x \in ℝ$
166	7	nn0red	$⊢ x \in ℝ^{+} \to ⌊x⌋ \in ℝ$
167		1red	$⊢ x \in ℝ^{+} \to 1 \in ℝ$
168		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
169	1 168	syl	$⊢ x \in ℝ^{+} \to ⌊x⌋ \leq x$
170	166 1 167 169	leadd1dd	$⊢ x \in ℝ^{+} \to ⌊x⌋ + 1 \leq x + 1$
171	10 163	logled	$⊢ x \in ℝ^{+} \to (⌊x⌋ + 1 \leq x + 1 \leftrightarrow \log (⌊x⌋ + 1) \leq \log (x + 1))$
172	170 171	mpbid	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) \leq \log (x + 1)$
173	11 164 13 172	lesub1dd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) - \log x \leq \log (x + 1) - \log x$
174		logdifbnd	$⊢ x \in ℝ^{+} \to \log (x + 1) - \log x \leq \frac{1}{x}$
175	160 165 158 173 174	letrd	$⊢ x \in ℝ^{+} \to \log (⌊x⌋ + 1) - \log x \leq \frac{1}{x}$
176	175	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log (⌊x⌋ + 1) - \log x \leq \frac{1}{x}$
177		fllep1	$⊢ x \in ℝ \to x \leq ⌊x⌋ + 1$
178	1 177	syl	$⊢ x \in ℝ^{+} \to x \leq ⌊x⌋ + 1$
179		logleb	$⊢ (x \in ℝ^{+} \land ⌊x⌋ + 1 \in ℝ^{+}) \to (x \leq ⌊x⌋ + 1 \leftrightarrow \log x \leq \log (⌊x⌋ + 1))$
180	10 179	mpdan	$⊢ x \in ℝ^{+} \to (x \leq ⌊x⌋ + 1 \leftrightarrow \log x \leq \log (⌊x⌋ + 1))$
181	178 180	mpbid	$⊢ x \in ℝ^{+} \to \log x \leq \log (⌊x⌋ + 1)$
182	11 13	subge0d	$⊢ x \in ℝ^{+} \to (0 \leq \log (⌊x⌋ + 1) - \log x \leftrightarrow \log x \leq \log (⌊x⌋ + 1))$
183	181 182	mpbird	$⊢ x \in ℝ^{+} \to 0 \leq \log (⌊x⌋ + 1) - \log x$
184	183	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \log (⌊x⌋ + 1) - \log x$
185	153 154 156 159 161 176 184	rlimsqz2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \underset{ℝ}{⇝} 0$
186		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \underset{ℝ}{⇝} 0 \to (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \in 𝑂 (1)$
187	185 186	syl	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \in 𝑂 (1)$
188		o1mul	$⊢ ((x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \times_{f} (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \in 𝑂 (1)$
189	152 187 188	sylancr	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \times_{f} (x \in ℝ^{+} ⟼ \log (⌊x⌋ + 1) - \log x) \in 𝑂 (1)$
190	151 189	eqeltrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x)) \in 𝑂 (1)$
191		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
192	191	ssriv	$⊢ ℕ \subseteq ℝ^{+}$
193	192	a1i	$⊢ ⊤ \to ℕ \subseteq ℝ^{+}$
194	193	sselda	$⊢ (⊤ \land n \in ℕ) \to n \in ℝ^{+}$
195	194 31	syl	$⊢ (⊤ \land n \in ℕ) \to (\log (n + 1) - \log n) ψ (n) \in ℂ$
196		chpo1ub	$⊢ (n \in ℝ^{+} ⟼ \frac{ψ (n)}{n}) \in 𝑂 (1)$
197	196	a1i	$⊢ ⊤ \to (n \in ℝ^{+} ⟼ \frac{ψ (n)}{n}) \in 𝑂 (1)$
198		rerpdivcl	$⊢ (ψ (n) \in ℝ \land n \in ℝ^{+}) \to \frac{ψ (n)}{n} \in ℝ$
199	29 198	mpancom	$⊢ n \in ℝ^{+} \to \frac{ψ (n)}{n} \in ℝ$
200	199	adantl	$⊢ (⊤ \land n \in ℝ^{+}) \to \frac{ψ (n)}{n} \in ℝ$
201	31	adantl	$⊢ (⊤ \land n \in ℝ^{+}) \to (\log (n + 1) - \log n) ψ (n) \in ℂ$
202		rpreccl	$⊢ n \in ℝ^{+} \to \frac{1}{n} \in ℝ^{+}$
203	202	rpred	$⊢ n \in ℝ^{+} \to \frac{1}{n} \in ℝ$
204		chpge0	$⊢ n \in ℝ \to 0 \leq ψ (n)$
205	27 204	syl	$⊢ n \in ℝ^{+} \to 0 \leq ψ (n)$
206		logdifbnd	$⊢ n \in ℝ^{+} \to \log (n + 1) - \log n \leq \frac{1}{n}$
207	26 203 29 205 206	lemul1ad	$⊢ n \in ℝ^{+} \to (\log (n + 1) - \log n) ψ (n) \leq (\frac{1}{n}) ψ (n)$
208	27	lep1d	$⊢ n \in ℝ^{+} \to n \leq n + 1$
209		logleb	$⊢ (n \in ℝ^{+} \land n + 1 \in ℝ^{+}) \to (n \leq n + 1 \leftrightarrow \log n \leq \log (n + 1))$
210	23 209	mpdan	$⊢ n \in ℝ^{+} \to (n \leq n + 1 \leftrightarrow \log n \leq \log (n + 1))$
211	208 210	mpbid	$⊢ n \in ℝ^{+} \to \log n \leq \log (n + 1)$
212	24 25	subge0d	$⊢ n \in ℝ^{+} \to (0 \leq \log (n + 1) - \log n \leftrightarrow \log n \leq \log (n + 1))$
213	211 212	mpbird	$⊢ n \in ℝ^{+} \to 0 \leq \log (n + 1) - \log n$
214	26 29 213 205	mulge0d	$⊢ n \in ℝ^{+} \to 0 \leq (\log (n + 1) - \log n) ψ (n)$
215	30 214	absidd	$⊢ n \in ℝ^{+} \to \|(\log (n + 1) - \log n) ψ (n)\| = (\log (n + 1) - \log n) ψ (n)$
216		rpregt0	$⊢ n \in ℝ^{+} \to (n \in ℝ \land 0 < n)$
217		divge0	$⊢ ((ψ (n) \in ℝ \land 0 \leq ψ (n)) \land (n \in ℝ \land 0 < n)) \to 0 \leq \frac{ψ (n)}{n}$
218	29 205 216 217	syl21anc	$⊢ n \in ℝ^{+} \to 0 \leq \frac{ψ (n)}{n}$
219	199 218	absidd	$⊢ n \in ℝ^{+} \to \|\frac{ψ (n)}{n}\| = \frac{ψ (n)}{n}$
220	29	recnd	$⊢ n \in ℝ^{+} \to ψ (n) \in ℂ$
221		rpcn	$⊢ n \in ℝ^{+} \to n \in ℂ$
222		rpne0	$⊢ n \in ℝ^{+} \to n \neq 0$
223	220 221 222	divrec2d	$⊢ n \in ℝ^{+} \to \frac{ψ (n)}{n} = (\frac{1}{n}) ψ (n)$
224	219 223	eqtrd	$⊢ n \in ℝ^{+} \to \|\frac{ψ (n)}{n}\| = (\frac{1}{n}) ψ (n)$
225	207 215 224	3brtr4d	$⊢ n \in ℝ^{+} \to \|(\log (n + 1) - \log n) ψ (n)\| \leq \|\frac{ψ (n)}{n}\|$
226	225	ad2antrl	$⊢ (⊤ \land (n \in ℝ^{+} \land 1 \leq n)) \to \|(\log (n + 1) - \log n) ψ (n)\| \leq \|\frac{ψ (n)}{n}\|$
227	154 197 200 201 226	o1le	$⊢ ⊤ \to (n \in ℝ^{+} ⟼ (\log (n + 1) - \log n) ψ (n)) \in 𝑂 (1)$
228	193 227	o1res2	$⊢ ⊤ \to (n \in ℕ ⟼ (\log (n + 1) - \log n) ψ (n)) \in 𝑂 (1)$
229	195 228	o1fsum	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x}) \in 𝑂 (1)$
230	141 142 190 229	o1sub2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x)}{x}) (\log (⌊x⌋ + 1) - \log x) - (\frac{\sum_{n = 1}^{⌊x⌋} (\log (n + 1) - \log n) ψ (n)}{x})) \in 𝑂 (1)$
231	140 230	eqeltrrid	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$
232	231	mptru	$⊢ (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg2lem

Proof