Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
rpvmasum.l |
⊢ 𝐿 = ( ℤRHom ‘ 𝑍 ) |
3 |
|
rpvmasum.a |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
dchrmusum.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
5 |
|
dchrmusum.d |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
6 |
|
dchrmusum.1 |
⊢ 1 = ( 0g ‘ 𝐺 ) |
7 |
|
dchrmusum.b |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
8 |
|
dchrmusum.n1 |
⊢ ( 𝜑 → 𝑋 ≠ 1 ) |
9 |
|
dchrmusum.f |
⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) |
10 |
|
dchrmusum.c |
⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) ) |
11 |
|
dchrmusum.t |
⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 ) |
12 |
|
dchrmusum.2 |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) ) |
13 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
14 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 ) |
15 |
|
elfzelz |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ ) |
17 |
4 1 5 2 14 16
|
dchrzrhcl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ) |
18 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
19 |
18
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
20 |
|
mucl |
⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ ) |
21 |
19 20
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ ) |
22 |
21
|
zred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ ) |
23 |
22 19
|
nndivred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
24 |
23
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
25 |
17 24
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
26 |
13 25
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) |
27 |
|
climcl |
⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝑇 → 𝑇 ∈ ℂ ) |
28 |
11 27
|
syl |
⊢ ( 𝜑 → 𝑇 ∈ ℂ ) |
29 |
28
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑇 ∈ ℂ ) |
30 |
26 29
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ∈ ℂ ) |
31 |
1 2 3 4 5 6 7 8 9 10 11 12
|
dchrisumn0 |
⊢ ( 𝜑 → 𝑇 ≠ 0 ) |
32 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑇 ≠ 0 ) |
33 |
30 29 32
|
divrecd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) |
34 |
26 29 32
|
divcan4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) |
35 |
33 34
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) |
36 |
35
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ) |
37 |
28 31
|
reccld |
⊢ ( 𝜑 → ( 1 / 𝑇 ) ∈ ℂ ) |
38 |
37
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑇 ) ∈ ℂ ) |
39 |
1 2 3 4 5 6 7 8 9 10 11 12
|
dchrmusum2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ) ∈ 𝑂(1) ) |
40 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
41 |
|
o1const |
⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 1 / 𝑇 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) ) |
42 |
40 37 41
|
sylancr |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) ) |
43 |
30 38 39 42
|
o1mul2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) ∈ 𝑂(1) ) |
44 |
36 43
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) ) |