Metamath Proof Explorer

Theorem vtsval

Description: Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses vtsval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
vtsval.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
vtsval.l ⊢ ( 𝜑 → 𝐿 : ℕ ⟶ ℂ )
Assertion vtsval ( 𝜑 → ( ( 𝐿 vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 vtsval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 vtsval.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3 vtsval.l ⊢ ( 𝜑 → 𝐿 : ℕ ⟶ ℂ )
4 cnex ⊢ ℂ ∈ V
5 nnex ⊢ ℕ ∈ V
6 4 5 elmap ⊢ ( 𝐿 ∈ ( ℂ ↑m ℕ ) ↔ 𝐿 : ℕ ⟶ ℂ )
7 3 6 sylibr ⊢ ( 𝜑 → 𝐿 ∈ ( ℂ ↑m ℕ ) )
8 fveq1 ⊢ ( 𝑙 = 𝐿 → ( 𝑙 ‘ 𝑎 ) = ( 𝐿 ‘ 𝑎 ) )
9 8 oveq1d ⊢ ( 𝑙 = 𝐿 → ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) )
10 9 sumeq2sdv ⊢ ( 𝑙 = 𝐿 → Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) )
11 10 mpteq2dv ⊢ ( 𝑙 = 𝐿 → ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
12 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
13 12 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) )
14 13 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
15 df-vts ⊢ vts = ( 𝑙 ∈ ( ℂ ↑m ℕ ) , 𝑛 ∈ ℕ0 ↦ ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
16 4 mptex ⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) ∈ V
17 11 14 15 16 ovmpo ⊢ ( ( 𝐿 ∈ ( ℂ ↑m ℕ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 vts 𝑁 ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
18 7 1 17 syl2anc ⊢ ( 𝜑 → ( 𝐿 vts 𝑁 ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
19 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑎 · 𝑥 ) = ( 𝑎 · 𝑋 ) )
20 19 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) = ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) )
21 20 fveq2d ⊢ ( 𝑥 = 𝑋 → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) )
22 21 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )
23 22 sumeq2sdv ⊢ ( 𝑥 = 𝑋 → Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )
25 sumex ⊢ Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) ∈ V
26 25 a1i ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) ∈ V )
27 18 24 2 26 fvmptd ⊢ ( 𝜑 → ( ( 𝐿 vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )