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 27590

Description: Lemma for selberg 27592. (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 11246	. . . . . . 7 ⊢ ℝ ∈ V
2		rpssre 13042	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5322	. . . . . 6 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
5		fzfid 14014	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13593	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 481	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		mucl 27184	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
10	9	zred 12722	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
11	10	recnd 11289	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
12		fzfid 14014	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
13		elfznn 13593	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
14	13	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
15	14	nnrpd 13075	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
16	15	relogcld 26665	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
17	16	resqcld 14165	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ)
18	12, 17	fsumrecl 15770	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℝ)
19		simplr 769	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
20	18, 19	rerpdivcld 13108	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ)
21	20	recnd 11289	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ)
22		selberglem1.t	. . . . . . . . . 10 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
23		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
24	6	nnrpd 13075	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
25		rpdivcl 13060	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
26	23, 24, 25	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
27	26	relogcld 26665	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
28	27	resqcld 14165	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
29		2re 12340	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
30		remulcl 11240	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
31	29, 27, 30	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
32		resubcl 11573	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
33	29, 31, 32	sylancr 587	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
34	28, 33	readdcld 11290	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
35	34, 7	nndivred 12320	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ)
36	22, 35	eqeltrid 2845	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ)
37	36	recnd 11289	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
38	21, 37	subcld 11620	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ)
39	11, 38	mulcld 11281	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
40	5, 39	fsumcl 15769	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
41	11, 37	mulcld 11281	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ)
42	5, 41	fsumcl 15769	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ)
43		2cn 12341	. . . . . . 7 ⊢ 2 ∈ ℂ
44		relogcl 26617	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
45	44	adantl 481	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
46	45	recnd 11289	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
47		mulcl 11239	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 · (log‘𝑥)) ∈ ℂ)
48	43, 46, 47	sylancr 587	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 · (log‘𝑥)) ∈ ℂ)
49	42, 48	subcld 11620	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈ ℂ)
50		eqidd 2738	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
51		eqidd 2738	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
52	4, 40, 49, 50, 51	offval2 7717	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))))
53	40, 42, 48	addsubassd 11640	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
54		rpcnne0 13053	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
55	54	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
56	55	simpld 494	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
57	10	adantr 480	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ)
58	57, 17	remulcld 11291	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
59	12, 58	fsumrecl 15770	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
60	59	recnd 11289	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℂ)
61	55	simprd 495	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
62	5, 56, 60, 61	fsumdivc 15822	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
63	17	recnd 11289	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ)
64	12, 63	fsumcl 15769	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ)
65	55	adantr 480	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66		divass 11940	. . . . . . . . . . 11 ⊢ (((μ‘𝑛) ∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
67	11, 64, 65, 66	syl3anc 1373	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
68	12, 11, 63	fsummulc2 15820	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)))
69	68	oveq1d 7446	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
70	21, 37	npcand 11624	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))
71	70	oveq2d 7447	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
72	11, 38, 37	adddid 11285	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
73	71, 72	eqtr3d 2779	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
74	67, 69, 73	3eqtr3d 2785	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
75	74	sumeq2dv 15738	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
76	5, 39, 41	fsumadd 15776	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)))
77	62, 75, 76	3eqtrrd 2782	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
78	77	oveq1d 7446	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
79	53, 78	eqtr3d 2779	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
80	79	mpteq2dva 5242	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
81	52, 80	eqtrd 2777	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
82		1red 11262	. . . . 5 ⊢ (⊤ → 1 ∈ ℝ)
83	5, 28	fsumrecl 15770	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
84	83, 23	rerpdivcld 13108	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ)
85	84	recnd 11289	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ)
86		2cnd 12344	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
87		2nn0 12543	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
88		logexprlim 27269	. . . . . . . 8 ⊢ (2 ∈ ℕ₀ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
89	87, 88	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
90		2cnd 12344	. . . . . . . 8 ⊢ (⊤ → 2 ∈ ℂ)
91		rlimconst 15580	. . . . . . . 8 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
92	2, 90, 91	sylancr 587	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
93	85, 86, 89, 92	rlimadd 15679	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2))
94		rlimo1 15653	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2) → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
95	93, 94	syl 17	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1))
96		readdcl 11238	. . . . . 6 ⊢ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
97	84, 29, 96	sylancl 586	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
98	40	abscld 15475	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
99	97	recnd 11289	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ)
100	99	abscld 15475	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ)
101	39	abscld 15475	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
102	5, 101	fsumrecl 15770	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
103	5, 39	fsumabs 15837	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
104		readdcl 11238	. . . . . . . . . . . 12 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
105	28, 29, 104	sylancl 586	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
106	105, 19	rerpdivcld 13108	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
107	5, 106	fsumrecl 15770	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
108	38	abscld 15475	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ)
109	11, 38	absmuld 15493	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
110	11	abscld 15475	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
111		1red 11262	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
112	38	absge0d 15483	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
113		mule1 27191	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
114	7, 113	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
115	110, 111, 108, 112, 114	lemul1ad 12207	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
116	108	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
117	116	mullidd 11279	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
118	115, 117	breqtrd 5169	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
119	109, 118	eqbrtrd 5165	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
120	65	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
121	120, 38	absmuld 15493	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
122	120, 21, 37	subdid 11719	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)))
123	65	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
124	64, 120, 123	divcan2d 12045	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2))
125	34	recnd 11289	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
126	7	nnrpd 13075	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
127		rpcnne0 13053	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
129		divass 11940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)))
130	22	oveq2i 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛))
131	129, 130	eqtr4di 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇))
132		div23 11941	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
133	131, 132	eqtr3d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
134	120, 125, 128, 133	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
135	124, 134	oveq12d 7449	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
136	122, 135	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
137	136	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))))
138		rprege0 13050	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
139		absid 15335	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
140	19, 138, 139	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥)
141	140	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
142	121, 137, 141	3eqtr3d 2785	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
143	7	nncnd 12282	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
144	143	mullidd 11279	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
145		rpre 13043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
147		fznnfl 13902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
149	148	simplbda 499	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
150	144, 149	eqbrtrd 5165	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
151	19	rpred 13077	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
152	111, 151, 126	lemuldivd 13126	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
153	150, 152	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
154		log2sumbnd 27588	. . . . . . . . . . . . . 14 ⊢ (((𝑥 / 𝑛) ∈ ℝ⁺ ∧ 1 ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
155	26, 153, 154	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
156	142, 155	eqbrtrrd 5167	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
157	108, 105, 19	lemuldiv2d 13127	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)))
158	156, 157	mpbid 232	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
159	101, 108, 106, 119, 158	letrd 11418	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
160	5, 101, 106, 159	fsumle 15835	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
161	5, 105	fsumrecl 15770	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
162		remulcl 11240	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
163	146, 29, 162	sylancl 586	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℝ)
164	83, 163	readdcld 11290	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈ ℝ)
165	28	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
166		2cnd 12344	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
167	5, 165, 166	fsumadd 15776	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2))
168		fsumconst 15826	. . . . . . . . . . . . . . . 16 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
169	5, 43, 168	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
170	138	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
171		flge0nn0 13860	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
172		hashfz1 14385	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
173	170, 171, 172	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
174	173	oveq1d 7446	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((♯‘(1...(⌊‘𝑥))) · 2) = ((⌊‘𝑥) · 2))
175	169, 174	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2))
176	175	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
177	167, 176	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
178		reflcl 13836	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
179	146, 178	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ∈ ℝ)
180	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℝ)
181	179, 180	remulcld 11291	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ∈ ℝ)
182		flle 13839	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
183	146, 182	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ≤ 𝑥)
184		2pos 12369	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
185	29, 184	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
186	185	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 ∈ ℝ ∧ 0 < 2))
187		lemul1 12119	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
188	179, 146, 186, 187	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
189	183, 188	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))
190	181, 163, 83, 189	leadd2dd 11878	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
191	177, 190	eqbrtrd 5165	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
192	161, 164, 23, 191	lediv1dd 13135	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥))
193	105	recnd 11289	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℂ)
194	5, 56, 193, 61	fsumdivc 15822	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
195	83	recnd 11289	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
196	56, 86	mulcld 11281	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℂ)
197		divdir 11947	. . . . . . . . . . . 12 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
198	195, 196, 55, 197	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
199	86, 56, 61	divcan3d 12048	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((𝑥 · 2) / 𝑥) = 2)
200	199	oveq2d 7447	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
201	198, 200	eqtrd 2777	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
202	192, 194, 201	3brtr3d 5174	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
203	102, 107, 97, 160, 202	letrd 11418	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
204	98, 102, 97, 103, 203	letrd 11418	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
205	97	leabsd 15453	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
206	98, 97, 100, 204, 205	letrd 11418	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
207	206	adantrr 717	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
208	82, 95, 97, 40, 207	o1le 15689	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1))
209	22	selberglem1 27589	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
210		o1add 15650	. . . 4 ⊢ (((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
211	208, 209, 210	sylancl 586	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
212	81, 211	eqeltrrd 2842	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
213	212	mptru 1547	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ⊤wtru 1541 ∈ wcel 2108 ≠ wne 2940 Vcvv 3480 ⊆ wss 3951 class class class wbr 5143 ↦ cmpt 5225 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 ℤcz 12613 ℝ⁺crp 13034 ...cfz 13547 ⌊cfl 13830 ↑cexp 14102 !cfa 14312 ♯chash 14369 abscabs 15273 ⇝_𝑟 crli 15521 𝑂(1)co1 15522 Σcsu 15722 logclog 26596 μcmu 27138

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-xnn0 12600 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-shft 15106 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-o1 15526 df-lo1 15527 df-sum 15723 df-ef 16103 df-e 16104 df-sin 16105 df-cos 16106 df-tan 16107 df-pi 16108 df-dvds 16291 df-gcd 16532 df-prm 16709 df-pc 16875 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-limc 25901 df-dv 25902 df-ulm 26420 df-log 26598 df-cxp 26599 df-atan 26910 df-em 27036 df-mu 27144

This theorem is referenced by: selberglem3 27591 selberg 27592

W3C validator