mulogsumlem - Metamath Proof Explorer

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

Theorem mulogsumlem 27704

Description: Lemma for mulogsum 27705. (Contributed by Mario Carneiro, 14-May-2016.)

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

Distinct variable group: 𝑚,𝑛,𝑥

**Proof of Theorem mulogsumlem**
Step	Hyp	Ref	Expression
1		fzfid 14014	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (1...(⌊‘𝑥)) ∈ Fin)
2		elfznn 13586	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3	2	adantl 486	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
4		mucl 27314	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
5	3, 4	syl 18	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
6	5	zred 12704	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
7	6, 3	nndivred 12294	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
8	7	recnd 11241	. . . . . 6 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
9	1, 8	fsumcl 15789	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
10	9	adantl 486	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
11		emre 27179	. . . . . 6 ⊢ γ ∈ ℝ
12	11	recni 11227	. . . . 5 ⊢ γ ∈ ℂ
13	12	a1i 11	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → γ ∈ ℂ)
14		mudivsum 27703	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
15	14	a1i 11	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
16		rpssre 13028	. . . . . 6 ⊢ ℝ⁺ ⊆ ℝ
17		o1const 15676	. . . . . 6 ⊢ ((ℝ⁺ ⊆ ℝ ∧ γ ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ γ) ∈ 𝑂(1))
18	16, 12, 17	mp2an 704	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ γ) ∈ 𝑂(1)
19	18	a1i 11	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ γ) ∈ 𝑂(1))
20	10, 13, 15, 19	o1mul2 15681	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ)) ∈ 𝑂(1))
21		fzfid 14014	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
22		elfznn 13586	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
23	22	adantl 486	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
24	23	nnrecred 12291	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℝ)
25	21, 24	fsumrecl 15790	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ∈ ℝ)
26	2	nnrpd 13062	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
27		rpdivcl 13047	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
28	26, 27	sylan2 604	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
29	28	relogcld 26797	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
30	25, 29	resubcld 11646	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ)
31	7, 30	remulcld 11243	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
32	1, 31	fsumrecl 15790	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
33	32	recnd 11241	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
34	33	adantl 486	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
35		mulcl 11188	. . . . . 6 ⊢ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ ∧ γ ∈ ℂ) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ) ∈ ℂ)
36	9, 12, 35	sylancl 597	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ) ∈ ℂ)
37	36	adantl 486	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ) ∈ ℂ)
38		nnrecre 12282	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
39	38	recnd 11241	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℂ)
40	23, 39	syl 18	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℂ)
41	21, 40	fsumcl 15789	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ∈ ℂ)
42	29	recnd 11241	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
43	41, 42	subcld 11573	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℂ)
44	8, 43	mulcld 11233	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
45		mulcl 11188	. . . . . . . . 9 ⊢ ((((μ‘𝑛) / 𝑛) ∈ ℂ ∧ γ ∈ ℂ) → (((μ‘𝑛) / 𝑛) · γ) ∈ ℂ)
46	8, 12, 45	sylancl 597	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · γ) ∈ ℂ)
47	1, 44, 46	fsumsub 15844	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · γ)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · γ)))
48	12	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → γ ∈ ℂ)
49	41, 42, 48	subsub4d 11604	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) − γ) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))
50	49	oveq2d 7426	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) − γ)) = (((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))))
51	8, 43, 48	subdid 11674	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) − γ)) = ((((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · γ)))
52	50, 51	eqtr3d 2800	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) = ((((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · γ)))
53	52	sumeq2dv 15758	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (((μ‘𝑛) / 𝑛) · γ)))
54	12	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → γ ∈ ℂ)
55	1, 54, 8	fsummulc1 15841	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · γ))
56	55	oveq2d 7426	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · γ)))
57	47, 53, 56	3eqtr4d 2808	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ)))
58	57	mpteq2ia 5206	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ)))
59	16	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ⁺ ⊆ ℝ)
60	42, 48	addcld 11232	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) + γ) ∈ ℂ)
61	41, 60	subcld 11573	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)) ∈ ℂ)
62	8, 61	mulcld 11233	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ∈ ℂ)
63	1, 62	fsumcl 15789	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ∈ ℂ)
64	63	adantl 486	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ∈ ℂ)
65		1red 11213	. . . . . 6 ⊢ (⊤ → 1 ∈ ℝ)
66	63	abscld 15495	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ∈ ℝ)
67	62	abscld 15495	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ∈ ℝ)
68	1, 67	fsumrecl 15790	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ∈ ℝ)
69		1red 11213	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → 1 ∈ ℝ)
70	1, 62	fsumabs 15858	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))))
71		rprege0 13036	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
72		flge0nn0 13858	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
73	71, 72	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℕ₀)
74	73	nn0red 12570	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℝ)
75		rerpdivcl 13052	. . . . . . . . . 10 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) / 𝑥) ∈ ℝ)
76	74, 75	mpancom 700	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → ((⌊‘𝑥) / 𝑥) ∈ ℝ)
77		rpreccl 13048	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ⁺ → (1 / 𝑥) ∈ ℝ⁺)
78	77	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑥) ∈ ℝ⁺)
79	78	rpred 13064	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑥) ∈ ℝ)
80	8	abscld 15495	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) / 𝑛)) ∈ ℝ)
81	3	nnrecred 12291	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
82	61	abscld 15495	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ∈ ℝ)
83		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ⁺)
84		rpdivcl 13047	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (𝑛 / 𝑥) ∈ ℝ⁺)
85	26, 83, 84	syl2anr 608	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 / 𝑥) ∈ ℝ⁺)
86	85	rpred 13064	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 / 𝑥) ∈ ℝ)
87	8	absge0d 15503	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((μ‘𝑛) / 𝑛)))
88	61	absge0d 15503	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))))
89	6	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
90	3	nncnd 12253	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
91	3	nnne0d 12290	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
92	89, 90, 91	absdivd 15514	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) / 𝑛)) = ((abs‘(μ‘𝑛)) / (abs‘𝑛)))
93	3	nnrpd 13062	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
94		rprege0 13036	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
95	93, 94	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
96		absid 15352	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) → (abs‘𝑛) = 𝑛)
97	95, 96	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛) = 𝑛)
98	97	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) / (abs‘𝑛)) = ((abs‘(μ‘𝑛)) / 𝑛))
99	92, 98	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) / 𝑛)) = ((abs‘(μ‘𝑛)) / 𝑛))
100	89	abscld 15495	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
101		1red 11213	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
102		mule1 27321	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
103	3, 102	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
104	100, 101, 93, 103	lediv1dd 13122	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) / 𝑛) ≤ (1 / 𝑛))
105	99, 104	eqbrtrd 5133	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) / 𝑛)) ≤ (1 / 𝑛))
106		harmonicbnd4 27184	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ≤ (1 / (𝑥 / 𝑛)))
107	28, 106	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ≤ (1 / (𝑥 / 𝑛)))
108		rpcnne0 13039	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
109	108	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
110		rpcnne0 13039	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111	93, 110	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
112		recdiv 11925	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (1 / (𝑥 / 𝑛)) = (𝑛 / 𝑥))
113	109, 111, 112	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑥 / 𝑛)) = (𝑛 / 𝑥))
114	107, 113	breqtrd 5137	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ))) ≤ (𝑛 / 𝑥))
115	80, 81, 82, 86, 87, 88, 105, 114	lemul12ad 12161	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((μ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ ((1 / 𝑛) · (𝑛 / 𝑥)))
116	8, 61	absmuld 15513	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) = ((abs‘((μ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))))
117		1cnd 11206	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
118		dmdcan 11929	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ) → ((𝑛 / 𝑥) · (1 / 𝑛)) = (1 / 𝑥))
119	111, 109, 117, 118	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 / 𝑥) · (1 / 𝑛)) = (1 / 𝑥))
120	85	rpcnd 13066	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 / 𝑥) ∈ ℂ)
121	81	recnd 11241	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
122	120, 121	mulcomd 11234	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 / 𝑥) · (1 / 𝑛)) = ((1 / 𝑛) · (𝑛 / 𝑥)))
123	119, 122	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑥) = ((1 / 𝑛) · (𝑛 / 𝑥)))
124	115, 116, 123	3brtr4d 5143	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ (1 / 𝑥))
125	1, 67, 79, 124	fsumle 15856	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑥))
126		hashfz1 14387	. . . . . . . . . . . . 13 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
127	73, 126	syl 18	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
128	127	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)) = ((⌊‘𝑥) · (1 / 𝑥)))
129	77	rpcnd 13066	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (1 / 𝑥) ∈ ℂ)
130		fsumconst 15846	. . . . . . . . . . . 12 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ (1 / 𝑥) ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)))
131	1, 129, 130	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)))
132	73	nn0cnd 12571	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℂ)
133		rpcn 13031	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
134		rpne0 13037	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
135	132, 133, 134	divrecd 11998	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → ((⌊‘𝑥) / 𝑥) = ((⌊‘𝑥) · (1 / 𝑥)))
136	128, 131, 135	3eqtr4d 2808	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((⌊‘𝑥) / 𝑥))
137	125, 136	breqtrd 5137	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ ((⌊‘𝑥) / 𝑥))
138		rpre 13029	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
139		flle 13837	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
140	138, 139	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ≤ 𝑥)
141	133	mulridd 11230	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 · 1) = 𝑥)
142	140, 141	breqtrrd 5139	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ≤ (𝑥 · 1))
143		reflcl 13834	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
144	138, 143	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℝ)
145		rpregt0 13035	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
146		ledivmul 12095	. . . . . . . . . . 11 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1)))
147	144, 69, 145, 146	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1)))
148	142, 147	mpbird 260	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → ((⌊‘𝑥) / 𝑥) ≤ 1)
149	68, 76, 69, 137, 148	letrd 11371	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ 1)
150	66, 68, 69, 70, 149	letrd 11371	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ 1)
151	150	ad2antrl 740	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ≤ 1)
152	59, 64, 65, 65, 151	elo1d 15592	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − ((log‘(𝑥 / 𝑛)) + γ)))) ∈ 𝑂(1))
153	58, 152	eqeltrrid 2868	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ))) ∈ 𝑂(1))
154	34, 37, 153	o1dif 15686	. . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) · γ)) ∈ 𝑂(1)))
155	20, 154	mpbird 260	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1))
156	155	mptru 1577	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 400 = wceq 1570 ⊤wtru 1571 ∈ wcel 2143 ≠ wne 2958 ⊆ wss 3905 class class class wbr 5109 ↦ cmpt 5192 ‘cfv 6536 (class class class)co 7410 Fincfn 8939 ℂcc 11102 ℝcr 11103 0cc0 11104 1c1 11105 + caddc 11107 · cmul 11109 < clt 11247 ≤ cle 11248 − cmin 11445 / cdiv 11875 ℕcn 12237 ℕ₀cn0 12508 ℤcz 12595 ℝ⁺crp 13020 ...cfz 13539 ⌊cfl 13828 ♯chash 14371 abscabs 15290 𝑂(1)co1 15542 Σcsu 15742 logclog 26728 γcem 27165 μcmu 27268

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-pre-sup 11182 ax-addf 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-disj 5077 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-oadd 8453 df-er 8690 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-dju 9892 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-div 11876 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-6 12311 df-7 12312 df-8 12313 df-9 12314 df-n0 12509 df-xnn0 12582 df-z 12596 df-dec 12716 df-uz 12867 df-q 12977 df-rp 13021 df-xneg 13141 df-xadd 13142 df-xmul 13143 df-ioo 13380 df-ioc 13381 df-ico 13382 df-icc 13383 df-fz 13540 df-fzo 13688 df-fl 13830 df-mod 13908 df-seq 14043 df-exp 14103 df-fac 14315 df-bc 14344 df-hash 14372 df-shft 15109 df-cj 15155 df-re 15156 df-im 15157 df-sqrt 15291 df-abs 15292 df-limsup 15527 df-clim 15544 df-rlim 15545 df-o1 15546 df-lo1 15547 df-sum 15743 df-ef 16125 df-e 16126 df-sin 16127 df-cos 16128 df-tan 16129 df-pi 16130 df-dvds 16315 df-gcd 16557 df-prm 16734 df-pc 16901 df-struct 17211 df-sets 17228 df-slot 17246 df-ndx 17258 df-base 17274 df-ress 17295 df-plusg 17327 df-mulr 17328 df-starv 17329 df-sca 17330 df-vsca 17331 df-ip 17332 df-tset 17333 df-ple 17334 df-ds 17336 df-unif 17337 df-hom 17338 df-cco 17339 df-rest 17479 df-topn 17480 df-0g 17498 df-gsum 17499 df-topgen 17500 df-pt 17501 df-prds 17504 df-xrs 17560 df-qtop 17565 df-imas 17566 df-xps 17568 df-mre 17642 df-mrc 17643 df-acs 17645 df-mgm 18702 df-sgrp 18781 df-mnd 18797 df-submnd 18846 df-mulg 19138 df-cntz 19391 df-cmn 19856 df-psmet 21523 df-xmet 21524 df-met 21525 df-bl 21526 df-mopn 21527 df-fbas 21528 df-fg 21529 df-cnfld 21532 df-top 23060 df-topon 23077 df-topsp 23099 df-bases 23112 df-cld 23185 df-ntr 23186 df-cls 23187 df-nei 23264 df-lp 23302 df-perf 23303 df-cn 23393 df-cnp 23394 df-haus 23481 df-cmp 23553 df-tx 23728 df-hmeo 23921 df-fil 24012 df-fm 24104 df-flim 24105 df-flf 24106 df-xms 24486 df-ms 24487 df-tms 24488 df-cncf 25046 df-limc 26034 df-dv 26035 df-ulm 26549 df-log 26730 df-atan 27041 df-em 27166 df-mu 27274

This theorem is used by: mulogsum 27705

W3C validator