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 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )