Theorem vtscl

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

	Ref	Expression
Hypotheses	vtsval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	vtsval.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	vtsval.l	⊢ ( 𝜑 → 𝐿 : ℕ ⟶ ℂ )
Assertion	vtscl	⊢ ( 𝜑 → ( ( 𝐿 vts 𝑁 ) ‘ 𝑋 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		vtsval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		vtsval.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3		vtsval.l	⊢ ( 𝜑 → 𝐿 : ℕ ⟶ ℂ )
4	1 2 3	vtsval	⊢ ( 𝜑 → ( ( 𝐿 vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) )
5		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → 𝐿 : ℕ ⟶ ℂ )
7		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
8	7	a1i	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
9	8	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → 𝑎 ∈ ℕ )
10	6 9	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( 𝐿 ‘ 𝑎 ) ∈ ℂ )
11		ax-icn	⊢ i ∈ ℂ
12		2cn	⊢ 2 ∈ ℂ
13		picn	⊢ π ∈ ℂ
14	12 13	mulcli	⊢ ( 2 · π ) ∈ ℂ
15	11 14	mulcli	⊢ ( i · ( 2 · π ) ) ∈ ℂ
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( i · ( 2 · π ) ) ∈ ℂ )
17	9	nncnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → 𝑎 ∈ ℂ )
18	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
19	17 18	mulcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( 𝑎 · 𝑋 ) ∈ ℂ )
20	16 19	mulcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ∈ ℂ )
21	20	efcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ∈ ℂ )
22	10 21	mulcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) ∈ ℂ )
23	5 22	fsumcl	⊢ ( 𝜑 → Σ 𝑎 ∈ ( 1 ... 𝑁 ) ( ( 𝐿 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑋 ) ) ) ) ∈ ℂ )
24	4 23	eqeltrd	⊢ ( 𝜑 → ( ( 𝐿 vts 𝑁 ) ‘ 𝑋 ) ∈ ℂ )