Metamath Proof Explorer

Theorem circlemeth

Description: The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypotheses circlemeth.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
circlemeth.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
circlemeth.l ⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
Assertion circlemeth ( 𝜑 → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 circlemeth.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 circlemeth.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3 circlemeth.l ⊢ ( 𝜑 → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
4 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℕ0 )
5 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 5 6 sstri ⊢ ( 0 (,) 1 ) ⊆ ℂ
8 7 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ℂ )
9 8 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℂ )
10 2 nnnn0d ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑆 ∈ ℕ0 )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
13 4 9 11 12 vtsprod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
15 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 0 ... ( 𝑆 · 𝑁 ) ) ∈ Fin )
16 ax-icn ⊢ i ∈ ℂ
17 2cn ⊢ 2 ∈ ℂ
18 picn ⊢ π ∈ ℂ
19 17 18 mulcli ⊢ ( 2 · π ) ∈ ℂ
20 16 19 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( i · ( 2 · π ) ) ∈ ℂ )
22 1 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
23 22 negcld ⊢ ( 𝜑 → - 𝑁 ∈ ℂ )
24 23 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 (,) 1 ) - 𝑁 ∈ ℂ )
25 24 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → - 𝑁 ∈ ℂ )
26 25 9 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( - 𝑁 · 𝑥 ) ∈ ℂ )
27 21 26 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ∈ ℂ )
28 27 efcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ∈ ℂ )
29 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
30 29 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) )
32 31 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℤ )
33 32 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℤ )
34 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑆 ∈ ℕ0 )
35 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
36 30 33 34 35 reprfi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∈ Fin )
37 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
38 37 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
39 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
40 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑆 ∈ ℕ0 )
41 32 zcnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℂ )
42 41 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑚 ∈ ℂ )
43 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
44 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
45 29 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
46 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑚 ∈ ℤ )
47 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑆 ∈ ℕ0 )
48 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) )
49 45 46 47 48 reprf ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
50 49 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
51 29 50 sseldi ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℕ )
52 39 40 42 43 44 51 breprexplemb ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
53 52 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
54 38 53 fprodcl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
55 20 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( i · ( 2 · π ) ) ∈ ℂ )
56 33 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℂ )
57 9 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑥 ∈ ℂ )
58 56 57 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑚 · 𝑥 ) ∈ ℂ )
59 55 58 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ∈ ℂ )
60 59 efcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ∈ ℂ )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ∈ ℂ )
62 54 61 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) ∈ ℂ )
63 36 62 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) ∈ ℂ )
64 15 28 63 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
65 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ∈ ℂ )
66 36 65 62 fsummulc1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
67 65 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ∈ ℂ )
68 54 61 67 mulassd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) ) )
69 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ∈ ℂ )
70 efadd ⊢ ( ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ∈ ℂ ∧ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ∈ ℂ ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) + ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
71 59 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) + ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
72 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( - 𝑁 · 𝑥 ) ∈ ℂ )
73 55 58 72 adddid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( i · ( 2 · π ) ) · ( ( 𝑚 · 𝑥 ) + ( - 𝑁 · 𝑥 ) ) ) = ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) + ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) )
74 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → - 𝑁 ∈ ℂ )
75 56 74 57 adddird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑚 + - 𝑁 ) · 𝑥 ) = ( ( 𝑚 · 𝑥 ) + ( - 𝑁 · 𝑥 ) ) )
76 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑁 ∈ ℂ )
77 56 76 negsubd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑚 + - 𝑁 ) = ( 𝑚 − 𝑁 ) )
78 77 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑚 + - 𝑁 ) · 𝑥 ) = ( ( 𝑚 − 𝑁 ) · 𝑥 ) )
79 75 78 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑚 · 𝑥 ) + ( - 𝑁 · 𝑥 ) ) = ( ( 𝑚 − 𝑁 ) · 𝑥 ) )
80 79 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( i · ( 2 · π ) ) · ( ( 𝑚 · 𝑥 ) + ( - 𝑁 · 𝑥 ) ) ) = ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) )
81 73 80 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) + ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) = ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) )
82 81 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) + ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) )
83 71 82 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) )
84 83 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
85 84 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
86 68 85 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
87 86 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
88 66 87 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
89 88 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑚 · 𝑥 ) ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
90 14 64 89 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) )
91 90 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 )
92 ioombl ⊢ ( 0 (,) 1 ) ∈ dom vol
93 92 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ∈ dom vol )
94 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑆 · 𝑁 ) ) ∈ Fin )
95 sumex ⊢ Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ V
96 95 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 (,) 1 ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ V )
97 93 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 0 (,) 1 ) ∈ dom vol )
98 29 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
99 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑆 ∈ ℕ0 )
100 fzfid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
101 98 32 99 100 reprfi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∈ Fin )
102 37 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
103 52 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
104 102 103 fprodcl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
105 56 76 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑚 − 𝑁 ) ∈ ℂ )
106 105 57 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑚 − 𝑁 ) · 𝑥 ) ∈ ℂ )
107 55 106 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ∈ ℂ )
108 107 an32s ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ∈ ℂ )
109 108 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ∈ ℂ )
110 109 efcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ∈ ℂ )
111 104 110 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ ℂ )
112 111 anasss ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ ( 𝑥 ∈ ( 0 (,) 1 ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ ℂ )
113 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
114 113 52 fprodcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
115 fvex ⊢ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ∈ V
116 115 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ∈ V )
117 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
118 117 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) )
119 92 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 0 (,) 1 ) ∈ dom vol )
120 115 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ∈ V )
121 0red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 0 ∈ ℝ )
122 1red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 1 ∈ ℝ )
123 22 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑁 ∈ ℂ )
124 41 123 subcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑚 − 𝑁 ) ∈ ℂ )
125 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
126 125 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 0 [,] 1 ) ⊆ ℂ )
127 ssidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ℂ ⊆ ℂ )
128 cncfmptc ⊢ ( ( ( 𝑚 − 𝑁 ) ∈ ℂ ∧ ( 0 [,] 1 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑚 − 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
129 124 126 127 128 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑚 − 𝑁 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
130 cncfmptid ⊢ ( ( ( 0 [,] 1 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
131 126 127 130 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
132 129 131 mulcncf ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
133 132 efmul2picn ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
134 cniccibl ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ 𝐿1 )
135 121 122 133 134 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ 𝐿1 )
136 118 119 120 135 iblss ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ 𝐿1 )
137 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ∈ 𝐿1 )
138 114 116 137 iblmulc2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ) ∈ 𝐿1 )
139 97 101 112 138 itgfsum ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ) ∈ 𝐿1 ∧ ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 ) )
140 139 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ) ∈ 𝐿1 )
141 93 94 96 140 itgfsum ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 (,) 1 ) ↦ Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) ) ∈ 𝐿1 ∧ ∫ ( 0 (,) 1 ) Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 ) )
142 141 simprd ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 )
143 oveq2 ⊢ ( if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) = 1 → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) = ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · 1 ) )
144 oveq2 ⊢ ( if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) = 0 → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) = ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · 0 ) )
145 101 114 fsumcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
146 145 mulid1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · 1 ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
147 145 mul01d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · 0 ) = 0 )
148 143 144 146 147 ifeq3da ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → if ( ( 𝑚 − 𝑁 ) = 0 , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) = ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) )
149 velsn ⊢ ( 𝑚 ∈ { 𝑁 } ↔ 𝑚 = 𝑁 )
150 41 123 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 𝑚 − 𝑁 ) = 0 ↔ 𝑚 = 𝑁 ) )
151 149 150 bitr4id ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑚 ∈ { 𝑁 } ↔ ( 𝑚 − 𝑁 ) = 0 ) )
152 151 ifbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → if ( 𝑚 ∈ { 𝑁 } , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) = if ( ( 𝑚 − 𝑁 ) = 0 , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) )
153 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
154 153 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑁 ∈ ℤ )
155 46 154 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 𝑚 − 𝑁 ) ∈ ℤ )
156 itgexpif ⊢ ( ( 𝑚 − 𝑁 ) ∈ ℤ → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 = if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) )
157 155 156 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 = if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) )
158 157 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) )
159 158 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) )
160 1cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 1 ∈ ℂ )
161 0cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 0 ∈ ℂ )
162 160 161 ifcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ∈ ℂ )
163 101 162 114 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) )
164 159 163 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · if ( ( 𝑚 − 𝑁 ) = 0 , 1 , 0 ) ) )
165 148 152 164 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = if ( 𝑚 ∈ { 𝑁 } , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) )
166 165 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) if ( 𝑚 ∈ { 𝑁 } , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) )
167 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
168 10 nn0zd ⊢ ( 𝜑 → 𝑆 ∈ ℤ )
169 168 153 zmulcld ⊢ ( 𝜑 → ( 𝑆 · 𝑁 ) ∈ ℤ )
170 1 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
171 nnmulge ⊢ ( ( 𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑆 · 𝑁 ) )
172 2 1 171 syl2anc ⊢ ( 𝜑 → 𝑁 ≤ ( 𝑆 · 𝑁 ) )
173 167 169 153 170 172 elfzd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) )
174 173 snssd ⊢ ( 𝜑 → { 𝑁 } ⊆ ( 0 ... ( 𝑆 · 𝑁 ) ) )
175 174 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑁 } ) → 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) )
176 175 145 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 𝑁 } ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
177 176 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
178 94 olcd ⊢ ( 𝜑 → ( ( 0 ... ( 𝑆 · 𝑁 ) ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... ( 𝑆 · 𝑁 ) ) ∈ Fin ) )
179 sumss2 ⊢ ( ( ( { 𝑁 } ⊆ ( 0 ... ( 𝑆 · 𝑁 ) ) ∧ ∀ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ ) ∧ ( ( 0 ... ( 𝑆 · 𝑁 ) ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... ( 𝑆 · 𝑁 ) ) ∈ Fin ) ) → Σ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) if ( 𝑚 ∈ { 𝑁 } , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) )
180 174 177 178 179 syl21anc ⊢ ( 𝜑 → Σ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) if ( 𝑚 ∈ { 𝑁 } , Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) , 0 ) )
181 29 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
182 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
183 181 153 10 182 reprfi ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∈ Fin )
184 37 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
185 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
186 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑆 ∈ ℕ0 )
187 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑁 ∈ ℂ )
188 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
189 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
190 29 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
191 153 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → 𝑁 ∈ ℤ )
192 10 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → 𝑆 ∈ ℕ0 )
193 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) )
194 190 191 192 193 reprf ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
195 194 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
196 29 195 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℕ )
197 185 186 187 188 189 196 breprexplemb ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
198 184 197 fprodcl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
199 183 198 fsumcl ⊢ ( 𝜑 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ )
200 oveq2 ⊢ ( 𝑚 = 𝑁 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) )
201 200 sumeq1d ⊢ ( 𝑚 = 𝑁 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
202 201 sumsn ⊢ ( ( 𝑁 ∈ ℕ0 ∧ Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) ∈ ℂ ) → Σ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
203 1 199 202 syl2anc ⊢ ( 𝜑 → Σ 𝑚 ∈ { 𝑁 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
204 166 180 203 3eqtr2d ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
205 139 simprd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 )
206 110 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ∈ ℂ )
207 114 206 137 itgmulc2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 )
208 207 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 )
209 205 208 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) )
210 209 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) d 𝑥 ) )
211 1 10 reprfz1 ⊢ ( 𝜑 → ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) )
212 211 sumeq1d ⊢ ( 𝜑 → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
213 204 210 212 3eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ∫ ( 0 (,) 1 ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( ( 𝑚 − 𝑁 ) · 𝑥 ) ) ) ) d 𝑥 = Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
214 91 142 213 3eqtrrd ⊢ ( 𝜑 → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝐿 ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )