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	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
51	29 50	sselid	⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 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	mulridd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 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	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
196	29 195	sselid	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 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 𝑥 )