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 27607

Description: Lemma for selberg 27609. (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 11164	. . . . . . 7 ⊢ ℝ ∈ V
2		rpssre 13001	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5278	. . . . . 6 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
5		fzfid 13986	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13558	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 485	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		mucl 27202	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
10	9	zred 12677	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
11	10	recnd 11210	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
12		fzfid 13986	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
13		elfznn 13558	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
14	13	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
15	14	nnrpd 13035	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
16	15	relogcld 26685	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
17	16	resqcld 14138	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ)
18	12, 17	fsumrecl 15761	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℝ)
19		simplr 778	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
20	18, 19	rerpdivcld 13068	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ)
21	20	recnd 11210	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ)
22		selberglem1.t	. . . . . . . . . 10 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)
23		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
24	6	nnrpd 13035	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
25		rpdivcl 13020	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
26	23, 24, 25	syl2an 605	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
27	26	relogcld 26685	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
28	27	resqcld 14138	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
29		2re 12292	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
30		remulcl 11158	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
31	29, 27, 30	sylancr 596	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ)
32		resubcl 11495	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
33	29, 31, 32	sylancr 596	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2 · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
34	28, 33	readdcld 11211	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
35	34, 7	nndivred 12267	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ)
36	22, 35	eqeltrid 2866	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ)
37	36	recnd 11210	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
38	21, 37	subcld 11542	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ)
39	11, 38	mulcld 11202	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
40	5, 39	fsumcl 15760	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
41	11, 37	mulcld 11202	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ)
42	5, 41	fsumcl 15760	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ)
43		2cn 12293	. . . . . . 7 ⊢ 2 ∈ ℂ
44		relogcl 26637	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
45	44	adantl 485	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
46	45	recnd 11210	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
47		mulcl 11157	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 · (log‘𝑥)) ∈ ℂ)
48	43, 46, 47	sylancr 596	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 · (log‘𝑥)) ∈ ℂ)
49	42, 48	subcld 11542	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈ ℂ)
50		eqidd 2763	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
51		eqidd 2763	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
52	4, 40, 49, 50, 51	offval2 7680	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))))
53	40, 42, 48	addsubassd 11562	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))
54		rpcnne0 13012	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
55	54	adantl 485	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
56	55	simpld 498	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
57	10	adantr 484	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ)
58	57, 17	remulcld 11212	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
59	12, 58	fsumrecl 15761	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ)
60	59	recnd 11210	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℂ)
61	55	simprd 499	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ≠ 0)
62	5, 56, 60, 61	fsumdivc 15813	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
63	17	recnd 11210	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ)
64	12, 63	fsumcl 15760	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ)
65	55	adantr 484	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
66		divass 11863	. . . . . . . . . . 11 ⊢ (((μ‘𝑛) ∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
67	11, 64, 65, 66	syl3anc 1390	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
68	12, 11, 63	fsummulc2 15811	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)))
69	68	oveq1d 7411	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
70	21, 37	npcand 11546	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))
71	70	oveq2d 7412	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)))
72	11, 38, 37	adddid 11206	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
73	71, 72	eqtr3d 2799	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
74	67, 69, 73	3eqtr3d 2805	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
75	74	sumeq2dv 15729	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)))
76	5, 39, 41	fsumadd 15767	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)))
77	62, 75, 76	3eqtrrd 2802	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥))
78	77	oveq1d 7411	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))
79	53, 78	eqtr3d 2799	. . . . 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 2797	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))))
82		1red 11182	. . . . 5 ⊢ (⊤ → 1 ∈ ℝ)
83	5, 28	fsumrecl 15761	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
84	83, 23	rerpdivcld 13068	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ)
85	84	recnd 11210	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ)
86		2cnd 12296	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
87		2nn0 12498	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
88		logexprlim 27286	. . . . . . . 8 ⊢ (2 ∈ ℕ₀ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
89	87, 88	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝_𝑟 (!‘2))
90		2cnd 12296	. . . . . . . 8 ⊢ (⊤ → 2 ∈ ℂ)
91		rlimconst 15571	. . . . . . . 8 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
92	2, 90, 91	sylancr 596	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ 2) ⇝_𝑟 2)
93	85, 86, 89, 92	rlimadd 15670	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝_𝑟 ((!‘2) + 2))
94		rlimo1 15644	. . . . . 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 11156	. . . . . 6 ⊢ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
97	84, 29, 96	sylancl 595	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ)
98	40	abscld 15466	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
99	97	recnd 11210	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ)
100	99	abscld 15466	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ)
101	39	abscld 15466	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
102	5, 101	fsumrecl 15761	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ)
103	5, 39	fsumabs 15829	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
104		readdcl 11156	. . . . . . . . . . . 12 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
105	28, 29, 104	sylancl 595	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
106	105, 19	rerpdivcld 13068	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
107	5, 106	fsumrecl 15761	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ)
108	38	abscld 15466	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ)
109	11, 38	absmuld 15484	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
110	11	abscld 15466	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
111		1red 11182	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
112	38	absge0d 15474	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))
113		mule1 27209	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
114	7, 113	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
115	110, 111, 108, 112, 114	lemul1ad 12131	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
116	108	recnd 11210	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ)
117	116	mullidd 11200	. . . . . . . . . . . . 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 498	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
121	120, 38	absmuld 15484	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
122	120, 21, 37	subdid 11643	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)))
123	65	simprd 499	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
124	64, 120, 123	divcan2d 11969	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2))
125	34	recnd 11210	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
126	7	nnrpd 13035	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
127		rpcnne0 13012	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
128	126, 127	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
129		divass 11863	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)))
130	22	oveq2i 7407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛))
131	129, 130	eqtr4di 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇))
132		div23 11864	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
133	131, 132	eqtr3d 2799	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
134	120, 125, 128, 133	syl3anc 1390	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))
135	124, 134	oveq12d 7414	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
136	122, 135	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))))))
137	136	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))))
138		rprege0 13009	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
139		absid 15323	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
140	19, 138, 139	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥)
141	140	oveq1d 7411	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
142	121, 137, 141	3eqtr3d 2805	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))))
143	7	nncnd 12226	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
144	143	mullidd 11200	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
145		rpre 13002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
146	145	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
147		fznnfl 13872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
149	148	simplbda 503	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
150	144, 149	eqbrtrd 5122	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
151	19	rpred 13037	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
152	111, 151, 126	lemuldivd 13086	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
153	150, 152	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
154		log2sumbnd 27605	. . . . . . . . . . . . . 14 ⊢ (((𝑥 / 𝑛) ∈ ℝ⁺ ∧ 1 ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛)))))))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2))
155	26, 153, 154	syl2anc 593	. . . . . . . . . . . . 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 13087	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)))
158	156, 157	mpbid 234	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
159	101, 108, 106, 119, 158	letrd 11340	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
160	5, 101, 106, 159	fsumle 15827	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
161	5, 105	fsumrecl 15761	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℝ)
162		remulcl 11158	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
163	146, 29, 162	sylancl 595	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℝ)
164	83, 163	readdcld 11211	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈ ℝ)
165	28	recnd 11210	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
166		2cnd 12296	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
167	5, 165, 166	fsumadd 15767	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2))
168		fsumconst 15817	. . . . . . . . . . . . . . . 16 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
169	5, 43, 168	sylancl 595	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((♯‘(1...(⌊‘𝑥))) · 2))
170	138	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
171		flge0nn0 13830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
172		hashfz1 14359	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
173	170, 171, 172	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
174	173	oveq1d 7411	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((♯‘(1...(⌊‘𝑥))) · 2) = ((⌊‘𝑥) · 2))
175	169, 174	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2))
176	175	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
177	167, 176	eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)))
178		reflcl 13806	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
179	146, 178	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ∈ ℝ)
180	29	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℝ)
181	179, 180	remulcld 11212	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ∈ ℝ)
182		flle 13809	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
183	146, 182	syl 17	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ≤ 𝑥)
184		2pos 12322	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
185	29, 184	pm3.2i 474	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
186	185	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (2 ∈ ℝ ∧ 0 < 2))
187		lemul1 12043	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
188	179, 146, 186, 187	syl3anc 1390	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)))
189	183, 188	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))
190	181, 163, 83, 189	leadd2dd 11802	. . . . . . . . . . . 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 13095	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥))
193	105	recnd 11210	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈ ℂ)
194	5, 56, 193, 61	fsumdivc 15813	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))
195	83	recnd 11210	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
196	56, 86	mulcld 11202	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (𝑥 · 2) ∈ ℂ)
197		divdir 11870	. . . . . . . . . . . 12 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
198	195, 196, 55, 197	syl3anc 1390	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)))
199	86, 56, 61	divcan3d 11972	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((𝑥 · 2) / 𝑥) = 2)
200	199	oveq2d 7412	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
201	198, 200	eqtrd 2797	. . . . . . . . . 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 11340	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
204	98, 102, 97, 103, 203	letrd 11340	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))
205	97	leabsd 15442	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
206	98, 97, 100, 204, 205	letrd 11340	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
207	206	adantrr 727	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)))
208	82, 95, 97, 40, 207	o1le 15680	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1))
209	22	selberglem1 27606	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
210		o1add 15641	. . . 4 ⊢ (((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
211	208, 209, 210	sylancl 595	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘_f + (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈ 𝑂(1))
212	81, 211	eqeltrrd 2863	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
213	212	mptru 1567	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ⊤wtru 1561 ∈ wcel 2142 ≠ wne 2957 Vcvv 3454 ⊆ wss 3904 class class class wbr 5100 ↦ cmpt 5181 ‘cfv 6521 (class class class)co 7396 ∘_f cof 7658 Fincfn 8927 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 < clt 11216 ≤ cle 11217 − cmin 11414 / cdiv 11844 ℕcn 12210 2c2 12272 ℕ₀cn0 12481 ℤcz 12568 ℝ⁺crp 12993 ...cfz 13512 ⌊cfl 13800 ↑cexp 14074 !cfa 14286 ♯chash 14343 abscabs 15261 ⇝_𝑟 crli 15512 𝑂(1)co1 15513 Σcsu 15713 logclog 26616 μcmu 27156

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-disj 5068 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8678 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-fi 9357 df-sup 9388 df-inf 9389 df-oi 9458 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-xnn0 12555 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-ioo 13353 df-ioc 13354 df-ico 13355 df-icc 13356 df-fz 13513 df-fzo 13660 df-fl 13802 df-mod 13880 df-seq 14015 df-exp 14075 df-fac 14287 df-bc 14316 df-hash 14344 df-shft 15080 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-limsup 15498 df-clim 15515 df-rlim 15516 df-o1 15517 df-lo1 15518 df-sum 15714 df-ef 16097 df-e 16098 df-sin 16099 df-cos 16100 df-tan 16101 df-pi 16102 df-dvds 16287 df-gcd 16529 df-prm 16706 df-pc 16873 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-rest 17451 df-topn 17452 df-0g 17470 df-gsum 17471 df-topgen 17472 df-pt 17473 df-prds 17476 df-xrs 17532 df-qtop 17537 df-imas 17538 df-xps 17540 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-submnd 18818 df-mulg 19110 df-cntz 19357 df-cmn 19822 df-psmet 21413 df-xmet 21414 df-met 21415 df-bl 21416 df-mopn 21417 df-fbas 21418 df-fg 21419 df-cnfld 21422 df-top 22951 df-topon 22968 df-topsp 22990 df-bases 23003 df-cld 23076 df-ntr 23077 df-cls 23078 df-nei 23155 df-lp 23193 df-perf 23194 df-cn 23284 df-cnp 23285 df-haus 23372 df-cmp 23444 df-tx 23619 df-hmeo 23812 df-fil 23903 df-fm 23995 df-flim 23996 df-flf 23997 df-xms 24377 df-ms 24378 df-tms 24379 df-cncf 24937 df-limc 25925 df-dv 25926 df-ulm 26437 df-log 26618 df-cxp 26619 df-atan 26929 df-em 27054 df-mu 27162

This theorem is referenced by: selberglem3 27608 selberg 27609

W3C validator