vtscl

Description: Closure of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 14-Dec-2021)

Step	Hyp	Ref	Expression
1		vtsval.n	$⊢ φ \to N \in ℕ_{0}$
2		vtsval.x	$⊢ φ \to X \in ℂ$
3		vtsval.l	$⊢ φ \to L : ℕ ⟶ ℂ$
4	1 2 3	vtsval	$⊢ φ \to (L vts N) (X) = \sum_{a = 1}^{N} L (a) e^{i 2 π a X}$
5		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
6	3	adantr	$⊢ (φ \land a \in (1 \dots N)) \to L : ℕ ⟶ ℂ$
7		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
8	7	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
9	8	sselda	$⊢ (φ \land a \in (1 \dots N)) \to a \in ℕ$
10	6 9	ffvelcdmd	$⊢ (φ \land a \in (1 \dots N)) \to L (a) \in ℂ$
11		ax-icn	$⊢ i \in ℂ$
12		2cn	$⊢ 2 \in ℂ$
13		picn	$⊢ π \in ℂ$
14	12 13	mulcli	$⊢ 2 π \in ℂ$
15	11 14	mulcli	$⊢ i 2 π \in ℂ$
16	15	a1i	$⊢ (φ \land a \in (1 \dots N)) \to i 2 π \in ℂ$
17	9	nncnd	$⊢ (φ \land a \in (1 \dots N)) \to a \in ℂ$
18	2	adantr	$⊢ (φ \land a \in (1 \dots N)) \to X \in ℂ$
19	17 18	mulcld	$⊢ (φ \land a \in (1 \dots N)) \to a X \in ℂ$
20	16 19	mulcld	$⊢ (φ \land a \in (1 \dots N)) \to i 2 π a X \in ℂ$
21	20	efcld	$⊢ (φ \land a \in (1 \dots N)) \to e^{i 2 π a X} \in ℂ$
22	10 21	mulcld	$⊢ (φ \land a \in (1 \dots N)) \to L (a) e^{i 2 π a X} \in ℂ$
23	5 22	fsumcl	$⊢ φ \to \sum_{a = 1}^{N} L (a) e^{i 2 π a X} \in ℂ$
24	4 23	eqeltrd	$⊢ φ \to (L vts N) (X) \in ℂ$

Metamath Proof Explorer