Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
rpvmasum.l |
⊢ 𝐿 = ( ℤRHom ‘ 𝑍 ) |
3 |
|
rpvmasum.a |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
rpvmasum2.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
5 |
|
rpvmasum2.d |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
6 |
|
rpvmasum2.1 |
⊢ 1 = ( 0g ‘ 𝐺 ) |
7 |
|
dchrisum0f.f |
⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) ) |
8 |
|
dchrisum0f.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
9 |
|
dchrisum0flb.r |
⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ) |
10 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin ) |
11 |
|
dvdsssfz1 |
⊢ ( 𝑛 ∈ ℕ → { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) ) |
13 |
10 12
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ∈ Fin ) |
14 |
9
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ) |
15 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
16 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
17 |
1 16 2
|
znzrhfo |
⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) ) |
18 |
|
fof |
⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
19 |
15 17 18
|
3syl |
⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
20 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
21 |
|
elrabi |
⊢ ( 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } → 𝑚 ∈ ℕ ) |
22 |
21
|
nnzd |
⊢ ( 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } → 𝑚 ∈ ℤ ) |
23 |
|
ffvelrn |
⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) ) |
24 |
20 22 23
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) ) |
25 |
14 24
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℝ ) |
26 |
13 25
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℝ ) |
27 |
|
breq2 |
⊢ ( 𝑏 = 𝑛 → ( 𝑞 ∥ 𝑏 ↔ 𝑞 ∥ 𝑛 ) ) |
28 |
27
|
rabbidv |
⊢ ( 𝑏 = 𝑛 → { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } = { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) |
29 |
28
|
sumeq1d |
⊢ ( 𝑏 = 𝑛 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) ) |
30 |
|
2fveq3 |
⊢ ( 𝑣 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
31 |
30
|
cbvsumv |
⊢ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) |
32 |
29 31
|
eqtrdi |
⊢ ( 𝑏 = 𝑛 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
33 |
32
|
cbvmptv |
⊢ ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
34 |
7 33
|
eqtri |
⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) |
35 |
26 34
|
fmptd |
⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ ) |