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 ⊢Z=ℤ/Nℤ
rpvmasum.l ⊢L=ℤRHom⁡Z
rpvmasum.a ⊢φ→N∈ℕ
rpvmasum2.g ⊢G=DChr⁡N
rpvmasum2.d ⊢D=BaseG
rpvmasum2.1 ⊢1˙=0G
dchrisum0f.f ⊢F=b∈ℕ⟼∑v∈q∈ℕ|q∥bX⁡L⁡v
dchrisum0f.x ⊢φ→X∈D
dchrisum0flb.r ⊢φ→X:BaseZ⟶ℝ
Assertion dchrisum0ff ⊢φ→F:ℕ⟶ℝ

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢Z=ℤ/Nℤ
2 rpvmasum.l ⊢L=ℤRHom⁡Z
3 rpvmasum.a ⊢φ→N∈ℕ
4 rpvmasum2.g ⊢G=DChr⁡N
5 rpvmasum2.d ⊢D=BaseG
6 rpvmasum2.1 ⊢1˙=0G
7 dchrisum0f.f ⊢F=b∈ℕ⟼∑v∈q∈ℕ|q∥bX⁡L⁡v
8 dchrisum0f.x ⊢φ→X∈D
9 dchrisum0flb.r ⊢φ→X:BaseZ⟶ℝ
10 fzfid ⊢φ∧n∈ℕ→1…n∈Fin
11 dvdsssfz1 ⊢n∈ℕ→q∈ℕ|q∥n⊆1…n
12 11 adantl ⊢φ∧n∈ℕ→q∈ℕ|q∥n⊆1…n
13 10 12 ssfid ⊢φ∧n∈ℕ→q∈ℕ|q∥n∈Fin
14 9 ad2antrr ⊢φ∧n∈ℕ∧m∈q∈ℕ|q∥n→X:BaseZ⟶ℝ
15 3 nnnn0d ⊢φ→N∈ℕ0
16 eqid ⊢BaseZ=BaseZ
17 1 16 2 znzrhfo ⊢N∈ℕ0→L:ℤ⟶ontoBaseZ
18 fof ⊢L:ℤ⟶ontoBaseZ→L:ℤ⟶BaseZ
19 15 17 18 3syl ⊢φ→L:ℤ⟶BaseZ
20 19 adantr ⊢φ∧n∈ℕ→L:ℤ⟶BaseZ
21 elrabi ⊢m∈q∈ℕ|q∥n→m∈ℕ
22 21 nnzd ⊢m∈q∈ℕ|q∥n→m∈ℤ
23 ffvelcdm ⊢L:ℤ⟶BaseZ∧m∈ℤ→L⁡m∈BaseZ
24 20 22 23 syl2an ⊢φ∧n∈ℕ∧m∈q∈ℕ|q∥n→L⁡m∈BaseZ
25 14 24 ffvelcdmd ⊢φ∧n∈ℕ∧m∈q∈ℕ|q∥n→X⁡L⁡m∈ℝ
26 13 25 fsumrecl ⊢φ∧n∈ℕ→∑m∈q∈ℕ|q∥nX⁡L⁡m∈ℝ
27 breq2 ⊢b=n→q∥b↔q∥n
28 27 rabbidv ⊢b=n→q∈ℕ|q∥b=q∈ℕ|q∥n
29 28 sumeq1d ⊢b=n→∑v∈q∈ℕ|q∥bX⁡L⁡v=∑v∈q∈ℕ|q∥nX⁡L⁡v
30 2fveq3 ⊢v=m→X⁡L⁡v=X⁡L⁡m
31 30 cbvsumv ⊢∑v∈q∈ℕ|q∥nX⁡L⁡v=∑m∈q∈ℕ|q∥nX⁡L⁡m
32 29 31 eqtrdi ⊢b=n→∑v∈q∈ℕ|q∥bX⁡L⁡v=∑m∈q∈ℕ|q∥nX⁡L⁡m
33 32 cbvmptv ⊢b∈ℕ⟼∑v∈q∈ℕ|q∥bX⁡L⁡v=n∈ℕ⟼∑m∈q∈ℕ|q∥nX⁡L⁡m
34 7 33 eqtri ⊢F=n∈ℕ⟼∑m∈q∈ℕ|q∥nX⁡L⁡m
35 26 34 fmptd ⊢φ→F:ℕ⟶ℝ