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

Metamath Proof Explorer

Theorem dchrisum0fval

Description: Value of the function F , the divisor sum of a Dirichlet character. (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
Assertion dchrisum0fval ⊢ A ∈ ℕ → F ⁡ A = ∑ t ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ t

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 breq2 ⊢ b = A → q ∥ b ↔ q ∥ A
9 8 rabbidv ⊢ b = A → q ∈ ℕ | q ∥ b = q ∈ ℕ | q ∥ A
10 9 sumeq1d ⊢ b = A → ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v = ∑ v ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ v
11 2fveq3 ⊢ v = t → X ⁡ L ⁡ v = X ⁡ L ⁡ t
12 11 cbvsumv ⊢ ∑ v ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ v = ∑ t ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ t
13 10 12 eqtrdi ⊢ b = A → ∑ v ∈ q ∈ ℕ | q ∥ b X ⁡ L ⁡ v = ∑ t ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ t
14 sumex ⊢ ∑ t ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ t ∈ V
15 13 7 14 fvmpt ⊢ A ∈ ℕ → F ⁡ A = ∑ t ∈ q ∈ ℕ | q ∥ A X ⁡ L ⁡ t