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

Metamath Proof Explorer

Theorem vtsprod

Description: Express the Vinogradov trigonometric sums to the power of S (Contributed by Thierry Arnoux, 12-Dec-2021)

Ref Expression
Hypotheses vtsval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
vtsval.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
vtsprod.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
vtsprod.l ⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
Assertion vtsprod ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 vtsval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 vtsval.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3 vtsprod.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 vtsprod.l ⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
5 ax-icn ⊢ i ∈ ℂ
6 5 a1i ⊢ ( 𝜑 → i ∈ ℂ )
7 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
8 picn ⊢ π ∈ ℂ
9 8 a1i ⊢ ( 𝜑 → π ∈ ℂ )
10 7 9 mulcld ⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ )
11 6 10 mulcld ⊢ ( 𝜑 → ( i · ( 2 · π ) ) ∈ ℂ )
12 11 2 mulcld ⊢ ( 𝜑 → ( ( i · ( 2 · π ) ) · 𝑋 ) ∈ ℂ )
13 12 efcld ⊢ ( 𝜑 → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ∈ ℂ )
14 1 3 13 4 breprexp ⊢ ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑋 ∈ ℂ )
17 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐿 ‘ 𝑎 ) ∈ ( ℂ ↑m ℕ ) )
18 elmapi ⊢ ( ( 𝐿 ‘ 𝑎 ) ∈ ( ℂ ↑m ℕ ) → ( 𝐿 ‘ 𝑎 ) : ℕ ⟶ ℂ )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝐿 ‘ 𝑎 ) : ℕ ⟶ ℂ )
20 15 16 19 vtsval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) ) ) )
21 fzssz ⊢ ( 1 ... 𝑁 ) ⊆ ℤ
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 1 ... 𝑁 ) )
23 21 22 sselid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ℤ )
24 23 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ℂ )
25 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( i · ( 2 · π ) ) ∈ ℂ )
26 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
27 24 25 26 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝑏 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) = ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) )
28 27 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( exp ‘ ( 𝑏 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) ) )
29 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( i · ( 2 · π ) ) · 𝑋 ) ∈ ℂ )
30 efexp ⊢ ( ( ( ( i · ( 2 · π ) ) · 𝑋 ) ∈ ℂ ∧ 𝑏 ∈ ℤ ) → ( exp ‘ ( 𝑏 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) )
31 29 23 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( exp ‘ ( 𝑏 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) )
32 28 31 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) )
33 32 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) ) ) = ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) ) )
34 33 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑏 · 𝑋 ) ) ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) ) )
35 20 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) ) )
36 35 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑋 ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑏 ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑏 ) ) )
37 fzssz ⊢ ( 0 ... ( 𝑆 · 𝑁 ) ) ⊆ ℤ
38 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) )
39 37 38 sselid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℤ )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑚 ∈ ℤ )
41 40 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑚 ∈ ℂ )
42 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( i · ( 2 · π ) ) ∈ ℂ )
43 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑋 ∈ ℂ )
44 41 42 43 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 𝑚 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) = ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) )
45 44 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( 𝑚 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) )
46 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ( i · ( 2 · π ) ) · 𝑋 ) ∈ ℂ )
47 efexp ⊢ ( ( ( ( i · ( 2 · π ) ) · 𝑋 ) ∈ ℂ ∧ 𝑚 ∈ ℤ ) → ( exp ‘ ( 𝑚 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) )
48 46 40 47 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( 𝑚 · ( ( i · ( 2 · π ) ) · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) )
49 45 48 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) )
50 49 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) ) )
51 50 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) ) )
52 51 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑋 ) ) ↑ 𝑚 ) ) )
53 14 36 52 3eqtr4d ⊢ ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑋 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑋 ) ) ) ) )