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 = Base G
rpvmasum2.1 ⊢ 1 ˙ = 0 G
dchrisum0f.f ⊢ F = b ∈ ℕ ⟼ ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v
dchrisum0f.x ⊢ φ → X ∈ D
dchrisum0flb.r ⊢ φ → X : Base Z ⟶ ℝ
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 = Base G
6 rpvmasum2.1 ⊢ 1 ˙ = 0 G
7 dchrisum0f.f ⊢ F = b ∈ ℕ ⟼ ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v
8 dchrisum0f.x ⊢ φ → X ∈ D
9 dchrisum0flb.r ⊢ φ → X : Base Z ⟶ ℝ
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 : Base Z ⟶ ℝ
15 3 nnnn0d ⊢ φ → N ∈ ℕ 0
16 eqid ⊢ Base Z = Base Z
17 1 16 2 znzrhfo ⊢ N ∈ ℕ 0 → L : ℤ ⟶ onto Base Z
18 fof ⊢ L : ℤ ⟶ onto Base Z → L : ℤ ⟶ Base Z
19 15 17 18 3syl ⊢ φ → L : ℤ ⟶ Base Z
20 19 adantr ⊢ φ ∧ n ∈ ℕ → L : ℤ ⟶ Base Z
21 elrabi ⊢ m ∈ q ∈ ℕ | q ∥ n → m ∈ ℕ
22 21 nnzd ⊢ m ∈ q ∈ ℕ | q ∥ n → m ∈ ℤ
23 ffvelrn ⊢ L : ℤ ⟶ Base Z ∧ m ∈ ℤ → L ⁡ m ∈ Base Z
24 20 22 23 syl2an ⊢ φ ∧ n ∈ ℕ ∧ m ∈ q ∈ ℕ | q ∥ n → L ⁡ m ∈ Base Z
25 14 24 ffvelrnd ⊢ φ ∧ n ∈ ℕ ∧ m ∈ q ∈ ℕ | q ∥ n → X ⁡ L ⁡ m ∈ ℝ
26 13 25 fsumrecl ⊢ φ ∧ n ∈ ℕ → ∑ m ∈ q ∈ ℕ | q ∥ n X ⁡ 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 ∥ b X ⁡ L ⁡ v = ∑ v ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ v
30 2fveq3 ⊢ v = m → X ⁡ L ⁡ v = X ⁡ L ⁡ m
31 30 cbvsumv ⊢ ∑ v ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ v = ∑ m ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ m
32 29 31 syl6eq ⊢ b = n → ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v = ∑ m ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ m
33 32 cbvmptv ⊢ b ∈ ℕ ⟼ ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v = n ∈ ℕ ⟼ ∑ m ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ m
34 7 33 eqtri ⊢ F = n ∈ ℕ ⟼ ∑ m ∈ q ∈ ℕ | q ∥ n X ⁡ L ⁡ m
35 26 34 fmptd ⊢ φ → F : ℕ ⟶ ℝ