This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisum0ff

Description: The function F is a real function. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum0f.f ⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
dchrisum0f.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum0flb.r ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
Assertion dchrisum0ff ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )

Proof

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 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
24 20 22 23 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
25 14 24 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑛 } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℝ )
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 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )