selberglem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > selberglem2		Structured version Visualization version GIF version

Theorem selberglem2 27782

Description: Lemma for selberg 27784. (Contributed by Mario Carneiro, 23-May-2016.)

**Hypothesis**
Ref	Expression
selberglem1.t	⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)

**Assertion**
Ref	Expression
selberglem2	⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Distinct variable group: 𝑚,𝑛,𝑥 Allowed substitution hints: 𝑇(𝑥, 𝑚, 𝑛)

**Proof of Theorem selberglem2**
Step	Hyp	Ref	Expression
1		reex 11215	. . . . . . 7 ⊢ ℝ ∈ V
2		rpssre 13050	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5287	. . . . . 6 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
5		fzfid 14037	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13608	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 487	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		mucl 27377	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
9	7, 8	syl 18	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
10	9	zred 12725	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
11	10	recnd 11261	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
12		fzfid 14037	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
13		elfznn 13608	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
14	13	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
15	14	nnrpd 13084	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
16	15	relogcld 26860	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
17	16	resqcld 14189	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ)
18	12, 17	fsumrecl 15820	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℝ)
19		simplr 781	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
20	18, 19	rerpdivcld 13117	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ)
21	20	recnd 11261	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ)
22		selberglem1.t	. . . . . . . . . 10 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
23		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
24	6	nnrpd 13084	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
25		rpdivcl 13069	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
26	23, 24, 25	syl2an 608	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
27	26	relogcld 26860	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
28	27	resqcld 14189	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
29		2re 12339	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
30		remulcl 11209	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
31	29, 27, 30	sylancr 599	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
32		resubcl 11546	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
33	29, 31, 32	sylancr 599	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
34	28, 33	readdcld 11262	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
35	34, 7	nndivred 12314	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ)
36	22, 35	eqeltrid 2864	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ)
37	36	recnd 11261	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
38	21, 37	subcld 11593	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ)
39	11, 38	mulcld 11253	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
40	5, 39	fsumcl 15819	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
41	11, 37	mulcld 11253	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ)
42	5, 41	fsumcl 15819	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ)
43		2cn 12340	. . . . . . 7 ⊢ 2 ∈ ℂ
44		relogcl 26812	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
45	44	adantl 487	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
46	45	recnd 11261	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
47		mulcl 11208	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 · (log‘𝑥)) ∈ ℂ)
48	43, 46, 47	sylancr 599	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 · (log‘𝑥)) ∈ ℂ)
49	42, 48	subcld 11593	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈ ℂ)
50		eqidd 2761	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
51		eqidd 2761	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
52	4, 40, 49, 50, 51	offval2 7698	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))))
53	40, 42, 48	addsubassd 11613	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
54		rpcnne0 13061	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
55	54	adantl 487	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
56	55	simpld 500	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
57	10	adantr 486	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ)
58	57, 17	remulcld 11263	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
59	12, 58	fsumrecl 15820	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
60	59	recnd 11261	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℂ)
61	55	simprd 501	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
62	5, 56, 60, 61	fsumdivc 15872	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
63	17	recnd 11261	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ)
64	12, 63	fsumcl 15819	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ)
65	55	adantr 486	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66		divass 11914	. . . . . . . . . . 11 ⊢ (((μ‘𝑛) ∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
67	11, 64, 65, 66	syl3anc 1398	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
68	12, 11, 63	fsummulc2 15870	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)))
69	68	oveq1d 7428	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
70	21, 37	npcand 11597	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))
71	70	oveq2d 7429	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
72	11, 38, 37	adddid 11257	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
73	71, 72	eqtr3d 2797	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
74	67, 69, 73	3eqtr3d 2803	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
75	74	sumeq2dv 15789	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
76	5, 39, 41	fsumadd 15826	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)))
77	62, 75, 76	3eqtrrd 2800	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
78	77	oveq1d 7428	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
79	53, 78	eqtr3d 2797	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
80	79	mpteq2dva 5198	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
81	52, 80	eqtrd 2795	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
82		1red 11233	. . . . 5 ⊢ (⊤ → 1 ∈ ℝ)
83	5, 28	fsumrecl 15820	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
84	83, 23	rerpdivcld 13117	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ)
85	84	recnd 11261	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ)
86		2cnd 12343	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
87		2nn0 12545	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
88		logexprlim 27461	. . . . . . . 8 ⊢ (2 ∈ ℕ₀ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
89	87, 88	mp1i 14	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
90		2cnd 12343	. . . . . . . 8 ⊢ (⊤ → 2 ∈ ℂ)
91		rlimconst 15631	. . . . . . . 8 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
92	2, 90, 91	sylancr 599	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
93	85, 86, 89, 92	rlimadd 15730	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2))
94		rlimo1 15704	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2) → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
95	93, 94	syl 18	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
96		readdcl 11207	. . . . . 6 ⊢ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
97	84, 29, 96	sylancl 598	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
98	40	abscld 15526	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
99	97	recnd 11261	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ)
100	99	abscld 15526	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ)
101	39	abscld 15526	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
102	5, 101	fsumrecl 15820	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
103	5, 39	fsumabs 15888	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
104		readdcl 11207	. . . . . . . . . . . 12 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
105	28, 29, 104	sylancl 598	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
106	105, 19	rerpdivcld 13117	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
107	5, 106	fsumrecl 15820	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
108	38	abscld 15526	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ)
109	11, 38	absmuld 15544	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
110	11	abscld 15526	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
111		1red 11233	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
112	38	absge0d 15534	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
113		mule1 27384	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
114	7, 113	syl 18	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
115	110, 111, 108, 112, 114	lemul1ad 12178	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
116	108	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
117	116	mullidd 11251	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
118	115, 117	breqtrd 5131	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
119	109, 118	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
120	65	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
121	120, 38	absmuld 15544	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
122	120, 21, 37	subdid 11694	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)))
123	65	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
124	64, 120, 123	divcan2d 12017	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2))
125	34	recnd 11261	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
126	7	nnrpd 13084	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
127		rpcnne0 13061	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
128	126, 127	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
129		divass 11914	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)))
130	22	oveq2i 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛))
131	129, 130	eqtr4di 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇))
132		div23 11915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
133	131, 132	eqtr3d 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
134	120, 125, 128, 133	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
135	124, 134	oveq12d 7431	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
136	122, 135	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
137	136	fveq2d 6882	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))))
138		rprege0 13058	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
139		absid 15383	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
140	19, 138, 139	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥)
141	140	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
142	121, 137, 141	3eqtr3d 2803	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
143	7	nncnd 12273	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
144	143	mullidd 11251	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
145		rpre 13051	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
146	145	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
147		fznnfl 13923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
148	146, 147	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
149	148	simplbda 505	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
150	144, 149	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
151	19	rpred 13086	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
152	111, 151, 126	lemuldivd 13135	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
153	150, 152	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
154		log2sumbnd 27780	. . . . . . . . . . . . . 14 ⊢ (((𝑥 / 𝑛) ∈ ℝ⁺ ∧ 1 ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
155	26, 153, 154	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
156	142, 155	eqbrtrrd 5129	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
157	108, 105, 19	lemuldiv2d 13136	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)))
158	156, 157	mpbid 235	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
159	101, 108, 106, 119, 158	letrd 11391	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
160	5, 101, 106, 159	fsumle 15886	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
161	5, 105	fsumrecl 15820	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
162		remulcl 11209	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
163	146, 29, 162	sylancl 598	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℝ)
164	83, 163	readdcld 11262	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈ ℝ)
165	28	recnd 11261	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
166		2cnd 12343	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
167	5, 165, 166	fsumadd 15826	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2))
168		fsumconst 15876	. . . . . . . . . . . . . . . 16 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
169	5, 43, 168	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
170	138	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
171		flge0nn0 13881	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
172		hashfz1 14410	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
173	170, 171, 172	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
174	173	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((♯‘(1...(⌊‘𝑥))) · 2) = ((⌊‘𝑥) · 2))
175	169, 174	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2))
176	175	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
177	167, 176	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
178		reflcl 13857	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
179	146, 178	syl 18	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ∈ ℝ)
180	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℝ)
181	179, 180	remulcld 11263	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ∈ ℝ)
182		flle 13860	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
183	146, 182	syl 18	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ≤ 𝑥)
184		2pos 12369	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
185	29, 184	pm3.2i 476	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
186	185	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 ∈ ℝ ∧ 0 < 2))
187		lemul1 12091	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
188	179, 146, 186, 187	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
189	183, 188	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))
190	181, 163, 83, 189	leadd2dd 11853	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
191	177, 190	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
192	161, 164, 23, 191	lediv1dd 13144	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥))
193	105	recnd 11261	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℂ)
194	5, 56, 193, 61	fsumdivc 15872	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
195	83	recnd 11261	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
196	56, 86	mulcld 11253	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℂ)
197		divdir 11921	. . . . . . . . . . . 12 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
198	195, 196, 55, 197	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
199	86, 56, 61	divcan3d 12020	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((𝑥 · 2) / 𝑥) = 2)
200	199	oveq2d 7429	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
201	198, 200	eqtrd 2795	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
202	192, 194, 201	3brtr3d 5136	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
203	102, 107, 97, 160, 202	letrd 11391	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
204	98, 102, 97, 103, 203	letrd 11391	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
205	97	leabsd 15502	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
206	98, 97, 100, 204, 205	letrd 11391	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
207	206	adantrr 730	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
208	82, 95, 97, 40, 207	o1le 15740	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1))
209	22	selberglem1 27781	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
210		o1add 15701	. . . 4 ⊢ (((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
211	208, 209, 210	sylancl 598	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
212	81, 211	eqeltrrd 2861	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
213	212	mptru 1577	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2955 Vcvv 3450 ⊆ wss 3899 class class class wbr 5103 ↦ cmpt 5186 ‘cfv 6533 (class class class)co 7413 ∘_f cof 7676 Fincfn 8952 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 · cmul 11129 < clt 11267 ≤ cle 11268 − cmin 11465 / cdiv 11895 ℕcn 12257 2c2 12319 ℕ₀cn0 12528 ℤcz 12615 ℝ⁺crp 13042 ...cfz 13561 ⌊cfl 13851 ↑cexp 14125 !cfa 14337 ♯chash 14394 abscabs 15321 ⇝_𝑟 crli 15572 𝑂(1)co1 15573 Σcsu 15773 logclog 26791 μcmu 27331

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-inf2 9620 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202 ax-addf 11203

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7678 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12529 df-xnn0 12602 df-z 12616 df-dec 12737 df-uz 12888 df-q 12998 df-rp 13043 df-xneg 13163 df-xadd 13164 df-xmul 13165 df-ioo 13402 df-ioc 13403 df-ico 13404 df-icc 13405 df-fz 13562 df-fzo 13710 df-fl 13853 df-mod 13931 df-seq 14066 df-exp 14126 df-fac 14338 df-bc 14367 df-hash 14395 df-shft 15140 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-limsup 15558 df-clim 15575 df-rlim 15576 df-o1 15577 df-lo1 15578 df-sum 15774 df-ef 16153 df-e 16154 df-sin 16155 df-cos 16156 df-tan 16157 df-pi 16158 df-dvds 16343 df-gcd 16585 df-prm 16762 df-pc 16929 df-struct 17239 df-sets 17256 df-slot 17274 df-ndx 17286 df-base 17302 df-ress 17323 df-plusg 17355 df-mulr 17356 df-starv 17357 df-sca 17358 df-vsca 17359 df-ip 17360 df-tset 17361 df-ple 17362 df-ds 17364 df-unif 17365 df-hom 17366 df-cco 17367 df-rest 17507 df-topn 17508 df-0g 17526 df-gsum 17527 df-topgen 17528 df-pt 17529 df-prds 17532 df-xrs 17588 df-qtop 17593 df-imas 17594 df-xps 17596 df-mre 17670 df-mrc 17671 df-acs 17673 df-mgm 18730 df-sgrp 18821 df-mnd 18837 df-submnd 18892 df-mulg 19191 df-cntz 19444 df-cmn 19909 df-psmet 21577 df-xmet 21578 df-met 21579 df-bl 21580 df-mopn 21581 df-fbas 21582 df-fg 21583 df-cnfld 21586 df-top 23119 df-topon 23136 df-topsp 23158 df-bases 23171 df-cld 23244 df-ntr 23245 df-cls 23246 df-nei 23323 df-lp 23361 df-perf 23362 df-cn 23452 df-cnp 23453 df-haus 23540 df-cmp 23612 df-tx 23788 df-hmeo 23981 df-fil 24072 df-fm 24164 df-flim 24165 df-flf 24166 df-xms 24546 df-ms 24547 df-tms 24548 df-cncf 25106 df-limc 26093 df-dv 26094 df-ulm 26613 df-log 26793 df-cxp 26794 df-atan 27104 df-em 27229 df-mu 27337

This theorem is used by: selberglem3 27783 selberg 27784

W3C validator