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 27525

Description: Lemma for selberg 27527. (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 11129	. . . . . . 7 ⊢ ℝ ∈ V
2		rpssre 12925	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5269	. . . . . 6 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
5		fzfid 13908	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13481	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 481	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		mucl 27119	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
10	9	zred 12608	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
11	10	recnd 11172	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
12		fzfid 13908	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
13		elfznn 13481	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
14	13	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
15	14	nnrpd 12959	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
16	15	relogcld 26600	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
17	16	resqcld 14060	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ)
18	12, 17	fsumrecl 15669	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℝ)
19		simplr 769	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
20	18, 19	rerpdivcld 12992	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ)
21	20	recnd 11172	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ)
22		selberglem1.t	. . . . . . . . . 10 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
23		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
24	6	nnrpd 12959	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
25		rpdivcl 12944	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
26	23, 24, 25	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
27	26	relogcld 26600	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
28	27	resqcld 14060	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
29		2re 12231	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
30		remulcl 11123	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
31	29, 27, 30	sylancr 588	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
32		resubcl 11457	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
33	29, 31, 32	sylancr 588	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
34	28, 33	readdcld 11173	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
35	34, 7	nndivred 12211	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ)
36	22, 35	eqeltrid 2841	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ)
37	36	recnd 11172	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
38	21, 37	subcld 11504	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ)
39	11, 38	mulcld 11164	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
40	5, 39	fsumcl 15668	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
41	11, 37	mulcld 11164	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ)
42	5, 41	fsumcl 15668	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ)
43		2cn 12232	. . . . . . 7 ⊢ 2 ∈ ℂ
44		relogcl 26552	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
45	44	adantl 481	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
46	45	recnd 11172	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
47		mulcl 11122	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 · (log‘𝑥)) ∈ ℂ)
48	43, 46, 47	sylancr 588	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 · (log‘𝑥)) ∈ ℂ)
49	42, 48	subcld 11504	. . . . 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 7652	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))))
53	40, 42, 48	addsubassd 11524	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
54		rpcnne0 12936	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
55	54	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
56	55	simpld 494	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
57	10	adantr 480	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ)
58	57, 17	remulcld 11174	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
59	12, 58	fsumrecl 15669	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
60	59	recnd 11172	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℂ)
61	55	simprd 495	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
62	5, 56, 60, 61	fsumdivc 15721	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
63	17	recnd 11172	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ)
64	12, 63	fsumcl 15668	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ)
65	55	adantr 480	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66		divass 11826	. . . . . . . . . . 11 ⊢ (((μ‘𝑛) ∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
67	11, 64, 65, 66	syl3anc 1374	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
68	12, 11, 63	fsummulc2 15719	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)))
69	68	oveq1d 7383	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
70	21, 37	npcand 11508	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))
71	70	oveq2d 7384	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
72	11, 38, 37	adddid 11168	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
73	71, 72	eqtr3d 2774	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
74	67, 69, 73	3eqtr3d 2780	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
75	74	sumeq2dv 15637	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
76	5, 39, 41	fsumadd 15675	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)))
77	62, 75, 76	3eqtrrd 2777	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
78	77	oveq1d 7383	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
79	53, 78	eqtr3d 2774	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
80	79	mpteq2dva 5193	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
81	52, 80	eqtrd 2772	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
82		1red 11145	. . . . 5 ⊢ (⊤ → 1 ∈ ℝ)
83	5, 28	fsumrecl 15669	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
84	83, 23	rerpdivcld 12992	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ)
85	84	recnd 11172	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ)
86		2cnd 12235	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
87		2nn0 12430	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
88		logexprlim 27204	. . . . . . . 8 ⊢ (2 ∈ ℕ₀ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
89	87, 88	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
90		2cnd 12235	. . . . . . . 8 ⊢ (⊤ → 2 ∈ ℂ)
91		rlimconst 15479	. . . . . . . 8 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
92	2, 90, 91	sylancr 588	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
93	85, 86, 89, 92	rlimadd 15578	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2))
94		rlimo1 15552	. . . . . 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 11121	. . . . . 6 ⊢ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
97	84, 29, 96	sylancl 587	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
98	40	abscld 15374	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
99	97	recnd 11172	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ)
100	99	abscld 15374	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ)
101	39	abscld 15374	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
102	5, 101	fsumrecl 15669	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
103	5, 39	fsumabs 15736	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
104		readdcl 11121	. . . . . . . . . . . 12 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
105	28, 29, 104	sylancl 587	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
106	105, 19	rerpdivcld 12992	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
107	5, 106	fsumrecl 15669	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
108	38	abscld 15374	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ)
109	11, 38	absmuld 15392	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
110	11	abscld 15374	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
111		1red 11145	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
112	38	absge0d 15382	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
113		mule1 27126	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
114	7, 113	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
115	110, 111, 108, 112, 114	lemul1ad 12093	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
116	108	recnd 11172	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
117	116	mullidd 11162	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
118	115, 117	breqtrd 5126	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
119	109, 118	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
120	65	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
121	120, 38	absmuld 15392	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
122	120, 21, 37	subdid 11605	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)))
123	65	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
124	64, 120, 123	divcan2d 11931	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2))
125	34	recnd 11172	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
126	7	nnrpd 12959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
127		rpcnne0 12936	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
129		divass 11826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)))
130	22	oveq2i 7379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛))
131	129, 130	eqtr4di 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇))
132		div23 11827	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
133	131, 132	eqtr3d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
134	120, 125, 128, 133	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
135	124, 134	oveq12d 7386	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
136	122, 135	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
137	136	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))))
138		rprege0 12933	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
139		absid 15231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
140	19, 138, 139	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥)
141	140	oveq1d 7383	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
142	121, 137, 141	3eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
143	7	nncnd 12173	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
144	143	mullidd 11162	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
145		rpre 12926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
147		fznnfl 13794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
149	148	simplbda 499	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
150	144, 149	eqbrtrd 5122	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
151	19	rpred 12961	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
152	111, 151, 126	lemuldivd 13010	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
153	150, 152	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
154		log2sumbnd 27523	. . . . . . . . . . . . . 14 ⊢ (((𝑥 / 𝑛) ∈ ℝ⁺ ∧ 1 ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
155	26, 153, 154	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
156	142, 155	eqbrtrrd 5124	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
157	108, 105, 19	lemuldiv2d 13011	. . . . . . . . . . . 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 11302	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
160	5, 101, 106, 159	fsumle 15734	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
161	5, 105	fsumrecl 15669	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
162		remulcl 11123	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
163	146, 29, 162	sylancl 587	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℝ)
164	83, 163	readdcld 11173	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈ ℝ)
165	28	recnd 11172	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
166		2cnd 12235	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
167	5, 165, 166	fsumadd 15675	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2))
168		fsumconst 15725	. . . . . . . . . . . . . . . 16 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
169	5, 43, 168	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
170	138	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
171		flge0nn0 13752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
172		hashfz1 14281	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
173	170, 171, 172	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
174	173	oveq1d 7383	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((♯‘(1...(⌊‘𝑥))) · 2) = ((⌊‘𝑥) · 2))
175	169, 174	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2))
176	175	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
177	167, 176	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
178		reflcl 13728	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
179	146, 178	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ∈ ℝ)
180	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℝ)
181	179, 180	remulcld 11174	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ∈ ℝ)
182		flle 13731	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
183	146, 182	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ≤ 𝑥)
184		2pos 12260	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
185	29, 184	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
186	185	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 ∈ ℝ ∧ 0 < 2))
187		lemul1 12005	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
188	179, 146, 186, 187	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
189	183, 188	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))
190	181, 163, 83, 189	leadd2dd 11764	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
191	177, 190	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)))
192	161, 164, 23, 191	lediv1dd 13019	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥))
193	105	recnd 11172	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℂ)
194	5, 56, 193, 61	fsumdivc 15721	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
195	83	recnd 11172	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
196	56, 86	mulcld 11164	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℂ)
197		divdir 11833	. . . . . . . . . . . 12 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
198	195, 196, 55, 197	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
199	86, 56, 61	divcan3d 11934	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((𝑥 · 2) / 𝑥) = 2)
200	199	oveq2d 7384	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
201	198, 200	eqtrd 2772	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
202	192, 194, 201	3brtr3d 5131	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
203	102, 107, 97, 160, 202	letrd 11302	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
204	98, 102, 97, 103, 203	letrd 11302	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
205	97	leabsd 15350	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
206	98, 97, 100, 204, 205	letrd 11302	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
207	206	adantrr 718	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
208	82, 95, 97, 40, 207	o1le 15588	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1))
209	22	selberglem1 27524	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
210		o1add 15549	. . . 4 ⊢ (((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
211	208, 209, 210	sylancl 587	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
212	81, 211	eqeltrrd 2838	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
213	212	mptru 1549	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 ≠ wne 2933 Vcvv 3442 ⊆ wss 3903 class class class wbr 5100 ↦ cmpt 5181 ‘cfv 6500 (class class class)co 7368 ∘_f cof 7630 Fincfn 8895 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 ≤ cle 11179 − cmin 11376 / cdiv 11806 ℕcn 12157 2c2 12212 ℕ₀cn0 12413 ℤcz 12500 ℝ⁺crp 12917 ...cfz 13435 ⌊cfl 13722 ↑cexp 13996 !cfa 14208 ♯chash 14265 abscabs 15169 ⇝_𝑟 crli 15420 𝑂(1)co1 15421 Σcsu 15621 logclog 26531 μcmu 27073

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-disj 5068 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-oadd 8411 df-er 8645 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-fi 9326 df-sup 9357 df-inf 9358 df-oi 9427 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-xnn0 12487 df-z 12501 df-dec 12620 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-ioo 13277 df-ioc 13278 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-fac 14209 df-bc 14238 df-hash 14266 df-shft 15002 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-limsup 15406 df-clim 15423 df-rlim 15424 df-o1 15425 df-lo1 15426 df-sum 15622 df-ef 16002 df-e 16003 df-sin 16004 df-cos 16005 df-tan 16006 df-pi 16007 df-dvds 16192 df-gcd 16434 df-prm 16611 df-pc 16777 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-rest 17354 df-topn 17355 df-0g 17373 df-gsum 17374 df-topgen 17375 df-pt 17376 df-prds 17379 df-xrs 17435 df-qtop 17440 df-imas 17441 df-xps 17443 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-mulg 19010 df-cntz 19258 df-cmn 19723 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-mopn 21317 df-fbas 21318 df-fg 21319 df-cnfld 21322 df-top 22850 df-topon 22867 df-topsp 22889 df-bases 22902 df-cld 22975 df-ntr 22976 df-cls 22977 df-nei 23054 df-lp 23092 df-perf 23093 df-cn 23183 df-cnp 23184 df-haus 23271 df-cmp 23343 df-tx 23518 df-hmeo 23711 df-fil 23802 df-fm 23894 df-flim 23895 df-flf 23896 df-xms 24276 df-ms 24277 df-tms 24278 df-cncf 24839 df-limc 25835 df-dv 25836 df-ulm 26354 df-log 26533 df-cxp 26534 df-atan 26845 df-em 26971 df-mu 27079

This theorem is referenced by: selberglem3 27526 selberg 27527

W3C validator