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