| Step |
Hyp |
Ref |
Expression |
| 1 |
|
selberglem1.t |
⊢ 𝑇 = ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) |
| 2 |
|
fzfid |
⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
| 3 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
| 4 |
3
|
adantl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
| 5 |
|
mucl |
⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ ) |
| 6 |
4 5
|
syl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ ) |
| 7 |
6
|
zred |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ ) |
| 8 |
7 4
|
nndivred |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
| 9 |
8
|
recnd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
| 10 |
3
|
nnrpd |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ ) |
| 11 |
|
rpdivcl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ ) |
| 12 |
10 11
|
sylan2 |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ ) |
| 13 |
|
relogcl |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
| 14 |
12 13
|
syl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
| 15 |
14
|
recnd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ ) |
| 16 |
15
|
sqcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℂ ) |
| 17 |
9 16
|
mulcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) ∈ ℂ ) |
| 18 |
2 17
|
fsumcl |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) ∈ ℂ ) |
| 19 |
|
2cn |
⊢ 2 ∈ ℂ |
| 20 |
19
|
a1i |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ ) |
| 21 |
20 15
|
mulcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
| 22 |
20 21
|
subcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ ) |
| 23 |
9 22
|
mulcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ) |
| 24 |
2 23
|
fsumcl |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ) |
| 25 |
|
relogcl |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ ) |
| 26 |
25
|
recnd |
⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ ) |
| 27 |
|
mulcl |
⊢ ( ( 2 ∈ ℂ ∧ ( log ‘ 𝑥 ) ∈ ℂ ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
| 28 |
19 26 27
|
sylancr |
⊢ ( 𝑥 ∈ ℝ+ → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
| 29 |
18 24 28
|
addsubd |
⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 30 |
1
|
oveq2i |
⊢ ( ( μ ‘ 𝑛 ) · 𝑇 ) = ( ( μ ‘ 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) |
| 31 |
6
|
zcnd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ ) |
| 32 |
16 22
|
addcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ) |
| 33 |
4
|
nnrpd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ ) |
| 34 |
33
|
rpcnne0d |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) |
| 35 |
|
divass |
⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( μ ‘ 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / 𝑛 ) = ( ( μ ‘ 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) ) |
| 36 |
|
div23 |
⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( μ ‘ 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / 𝑛 ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 37 |
35 36
|
eqtr3d |
⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( μ ‘ 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 38 |
31 32 34 37
|
syl3anc |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 39 |
9 16 22
|
adddid |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 40 |
38 39
|
eqtrd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 41 |
30 40
|
syl5eq |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · 𝑇 ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 42 |
41
|
sumeq2dv |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 43 |
2 17 23
|
fsumadd |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 44 |
42 43
|
eqtrd |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 45 |
44
|
oveq1d |
⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) |
| 46 |
19
|
a1i |
⊢ ( 𝑥 ∈ ℝ+ → 2 ∈ ℂ ) |
| 47 |
9 15
|
mulcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
| 48 |
9 47
|
subcld |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ ) |
| 49 |
2 46 48
|
fsummulc2 |
⊢ ( 𝑥 ∈ ℝ+ → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 50 |
2 9 47
|
fsumsub |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
| 51 |
50
|
oveq2d |
⊢ ( 𝑥 ∈ ℝ+ → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 52 |
20 9
|
mulcomd |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 2 ) ) |
| 53 |
20 9 15
|
mul12d |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
| 54 |
52 53
|
oveq12d |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) − ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 2 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 55 |
20 9 47
|
subdid |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( 2 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) − ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 56 |
9 20 21
|
subdid |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 2 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 57 |
54 55 56
|
3eqtr4d |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 58 |
57
|
sumeq2dv |
⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( μ ‘ 𝑛 ) / 𝑛 ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 59 |
49 51 58
|
3eqtr3d |
⊢ ( 𝑥 ∈ ℝ+ → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 60 |
59
|
oveq2d |
⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 61 |
29 45 60
|
3eqtr4d |
⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 62 |
61
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
| 63 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ V ) |
| 64 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ V ) |
| 65 |
|
mulog2sum |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) |
| 66 |
65
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
| 67 |
|
2ex |
⊢ 2 ∈ V |
| 68 |
67
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ V ) |
| 69 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ V ) |
| 70 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
| 71 |
|
o1const |
⊢ ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) ) |
| 72 |
70 19 71
|
mp2an |
⊢ ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) |
| 73 |
72
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) ) |
| 74 |
|
reex |
⊢ ℝ ∈ V |
| 75 |
74 70
|
ssexi |
⊢ ℝ+ ∈ V |
| 76 |
75
|
a1i |
⊢ ( ⊤ → ℝ+ ∈ V ) |
| 77 |
|
sumex |
⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ V |
| 78 |
77
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ V ) |
| 79 |
|
sumex |
⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ V |
| 80 |
79
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ V ) |
| 81 |
|
eqidd |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) |
| 82 |
|
eqidd |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
| 83 |
76 78 80 81 82
|
offval2 |
⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
| 84 |
|
mudivsum |
⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) |
| 85 |
|
mulogsum |
⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) |
| 86 |
|
o1sub |
⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ) |
| 87 |
84 85 86
|
mp2an |
⊢ ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) |
| 88 |
83 87
|
eqeltrrdi |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ) |
| 89 |
68 69 73 88
|
o1mul2 |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ 𝑂(1) ) |
| 90 |
63 64 66 89
|
o1add2 |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ∈ 𝑂(1) ) |
| 91 |
90
|
mptru |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ∈ 𝑂(1) |
| 92 |
62 91
|
eqeltri |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) |