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

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 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 𝑁 ) ‘ 𝑋 ) ∈ ℂ )