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	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )