fourierdlem83

Description: The fourier partial sum for F rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem83.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem83.c	$⊢ C = (- π, π)$
	fourierdlem83.fl1	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
	fourierdlem83.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{C} F (x) \cos n x d x}{π})$
	fourierdlem83.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{C} F (x) \sin n x d x}{π})$
	fourierdlem83.x	$⊢ φ \to X \in ℝ$
	fourierdlem83.s	$⊢ S = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
	fourierdlem83.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
	fourierdlem83.n	$⊢ φ \to N \in ℕ$
Assertion	fourierdlem83	$⊢ φ \to S (N) = \int_{C} F (x) D (N) (x - X) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem83.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem83.c	$⊢ C = (- π, π)$
3		fourierdlem83.fl1	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
4		fourierdlem83.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{C} F (x) \cos n x d x}{π})$
5		fourierdlem83.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{C} F (x) \sin n x d x}{π})$
6		fourierdlem83.x	$⊢ φ \to X \in ℝ$
7		fourierdlem83.s	$⊢ S = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
8		fourierdlem83.d	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
9		fourierdlem83.n	$⊢ φ \to N \in ℕ$
10	7	a1i	$⊢ φ \to S = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
11		oveq2	$⊢ m = N \to (1 \dots m) = (1 \dots N)$
12	11	sumeq1d	$⊢ m = N \to \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X)$
13	12	oveq2d	$⊢ m = N \to (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = (\frac{A (0)}{2}) + \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X)$
14	13	adantl	$⊢ (φ \land m = N) \to (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = (\frac{A (0)}{2}) + \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X)$
15		id	$⊢ φ \to φ$
16		0nn0	$⊢ 0 \in ℕ_{0}$
17	16	a1i	$⊢ φ \to 0 \in ℕ_{0}$
18	16	elexi	$⊢ 0 \in V$
19		eleq1	$⊢ n = 0 \to (n \in ℕ_{0} \leftrightarrow 0 \in ℕ_{0})$
20	19	anbi2d	$⊢ n = 0 \to ((φ \land n \in ℕ_{0}) \leftrightarrow (φ \land 0 \in ℕ_{0}))$
21		fveq2	$⊢ n = 0 \to A (n) = A (0)$
22	21	eleq1d	$⊢ n = 0 \to (A (n) \in ℝ \leftrightarrow A (0) \in ℝ)$
23	20 22	imbi12d	$⊢ n = 0 \to (((φ \land n \in ℕ_{0}) \to A (n) \in ℝ) \leftrightarrow ((φ \land 0 \in ℕ_{0}) \to A (0) \in ℝ))$
24	1 2 3 4 5	fourierdlem22	$⊢ φ \to ((n \in ℕ_{0} \to A (n) \in ℝ) \land (n \in ℕ \to B (n) \in ℝ))$
25	24	simpld	$⊢ φ \to (n \in ℕ_{0} \to A (n) \in ℝ)$
26	25	imp	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℝ$
27	18 23 26	vtocl	$⊢ (φ \land 0 \in ℕ_{0}) \to A (0) \in ℝ$
28	15 17 27	syl2anc	$⊢ φ \to A (0) \in ℝ$
29	28	rehalfcld	$⊢ φ \to \frac{A (0)}{2} \in ℝ$
30		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
31		eleq1	$⊢ k = n \to (k \in ℕ_{0} \leftrightarrow n \in ℕ_{0})$
32	31	anbi2d	$⊢ k = n \to ((φ \land k \in ℕ_{0}) \leftrightarrow (φ \land n \in ℕ_{0}))$
33		simpl	$⊢ (k = n \land x \in C) \to k = n$
34	33	oveq1d	$⊢ (k = n \land x \in C) \to k x = n x$
35	34	fveq2d	$⊢ (k = n \land x \in C) \to \cos k x = \cos n x$
36	35	oveq2d	$⊢ (k = n \land x \in C) \to F (x) \cos k x = F (x) \cos n x$
37	36	itgeq2dv	$⊢ k = n \to \int_{C} F (x) \cos k x d x = \int_{C} F (x) \cos n x d x$
38	37	eleq1d	$⊢ k = n \to (\int_{C} F (x) \cos k x d x \in ℝ \leftrightarrow \int_{C} F (x) \cos n x d x \in ℝ)$
39	32 38	imbi12d	$⊢ k = n \to (((φ \land k \in ℕ_{0}) \to \int_{C} F (x) \cos k x d x \in ℝ) \leftrightarrow ((φ \land n \in ℕ_{0}) \to \int_{C} F (x) \cos n x d x \in ℝ))$
40	1	adantr	$⊢ (φ \land k \in ℕ_{0}) \to F : ℝ ⟶ ℝ$
41	3	adantr	$⊢ (φ \land k \in ℕ_{0}) \to {F ↾}_{C} \in 𝐿^{1}$
42		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
43	40 2 41 4 42	fourierdlem16	$⊢ (φ \land k \in ℕ_{0}) \to ((A (k) \in ℝ \land (x \in C ⟼ F (x)) \in 𝐿^{1}) \land \int_{C} F (x) \cos k x d x \in ℝ)$
44	43	simprd	$⊢ (φ \land k \in ℕ_{0}) \to \int_{C} F (x) \cos k x d x \in ℝ$
45	39 44	chvarvv	$⊢ (φ \land n \in ℕ_{0}) \to \int_{C} F (x) \cos n x d x \in ℝ$
46		pire	$⊢ π \in ℝ$
47	46	a1i	$⊢ (φ \land n \in ℕ_{0}) \to π \in ℝ$
48		0re	$⊢ 0 \in ℝ$
49		pipos	$⊢ 0 < π$
50	48 49	gtneii	$⊢ π \neq 0$
51	50	a1i	$⊢ (φ \land n \in ℕ_{0}) \to π \neq 0$
52	45 47 51	redivcld	$⊢ (φ \land n \in ℕ_{0}) \to \frac{\int_{C} F (x) \cos n x d x}{π} \in ℝ$
53	52 4	fmptd	$⊢ φ \to A : ℕ_{0} ⟶ ℝ$
54	53	adantr	$⊢ (φ \land n \in (1 \dots N)) \to A : ℕ_{0} ⟶ ℝ$
55		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
56	55	nnnn0d	$⊢ n \in (1 \dots N) \to n \in ℕ_{0}$
57	56	adantl	$⊢ (φ \land n \in (1 \dots N)) \to n \in ℕ_{0}$
58	54 57	ffvelrnd	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \in ℝ$
59	57	nn0red	$⊢ (φ \land n \in (1 \dots N)) \to n \in ℝ$
60	6	adantr	$⊢ (φ \land n \in (1 \dots N)) \to X \in ℝ$
61	59 60	remulcld	$⊢ (φ \land n \in (1 \dots N)) \to n X \in ℝ$
62	61	recoscld	$⊢ (φ \land n \in (1 \dots N)) \to \cos n X \in ℝ$
63	58 62	remulcld	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X \in ℝ$
64		eleq1	$⊢ k = n \to (k \in ℕ \leftrightarrow n \in ℕ)$
65	64	anbi2d	$⊢ k = n \to ((φ \land k \in ℕ) \leftrightarrow (φ \land n \in ℕ))$
66		oveq1	$⊢ k = n \to k x = n x$
67	66	fveq2d	$⊢ k = n \to \sin k x = \sin n x$
68	67	oveq2d	$⊢ k = n \to F (x) \sin k x = F (x) \sin n x$
69	68	adantr	$⊢ (k = n \land x \in C) \to F (x) \sin k x = F (x) \sin n x$
70	69	itgeq2dv	$⊢ k = n \to \int_{C} F (x) \sin k x d x = \int_{C} F (x) \sin n x d x$
71	70	eleq1d	$⊢ k = n \to (\int_{C} F (x) \sin k x d x \in ℝ \leftrightarrow \int_{C} F (x) \sin n x d x \in ℝ)$
72	65 71	imbi12d	$⊢ k = n \to (((φ \land k \in ℕ) \to \int_{C} F (x) \sin k x d x \in ℝ) \leftrightarrow ((φ \land n \in ℕ) \to \int_{C} F (x) \sin n x d x \in ℝ))$
73	1	adantr	$⊢ (φ \land k \in ℕ) \to F : ℝ ⟶ ℝ$
74	3	adantr	$⊢ (φ \land k \in ℕ) \to {F ↾}_{C} \in 𝐿^{1}$
75		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
76	73 2 74 5 75	fourierdlem21	$⊢ (φ \land k \in ℕ) \to ((B (k) \in ℝ \land (x \in C ⟼ F (x) \sin k x) \in 𝐿^{1}) \land \int_{C} F (x) \sin k x d x \in ℝ)$
77	76	simprd	$⊢ (φ \land k \in ℕ) \to \int_{C} F (x) \sin k x d x \in ℝ$
78	72 77	chvarvv	$⊢ (φ \land n \in ℕ) \to \int_{C} F (x) \sin n x d x \in ℝ$
79	46	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
80	50	a1i	$⊢ (φ \land n \in ℕ) \to π \neq 0$
81	78 79 80	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{\int_{C} F (x) \sin n x d x}{π} \in ℝ$
82	81 5	fmptd	$⊢ φ \to B : ℕ ⟶ ℝ$
83	82	adantr	$⊢ (φ \land n \in (1 \dots N)) \to B : ℕ ⟶ ℝ$
84	55	adantl	$⊢ (φ \land n \in (1 \dots N)) \to n \in ℕ$
85	83 84	ffvelrnd	$⊢ (φ \land n \in (1 \dots N)) \to B (n) \in ℝ$
86	61	resincld	$⊢ (φ \land n \in (1 \dots N)) \to \sin n X \in ℝ$
87	85 86	remulcld	$⊢ (φ \land n \in (1 \dots N)) \to B (n) \sin n X \in ℝ$
88	63 87	readdcld	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X + B (n) \sin n X \in ℝ$
89	30 88	fsumrecl	$⊢ φ \to \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X) \in ℝ$
90	29 89	readdcld	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X) \in ℝ$
91	10 14 9 90	fvmptd	$⊢ φ \to S (N) = (\frac{A (0)}{2}) + \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X)$
92	4	a1i	$⊢ φ \to A = (n \in ℕ_{0} ⟼ \frac{\int_{C} F (x) \cos n x d x}{π})$
93		oveq1	$⊢ n = 0 \to n x = 0 \cdot x$
94	93	fveq2d	$⊢ n = 0 \to \cos n x = \cos 0 \cdot x$
95	94	oveq2d	$⊢ n = 0 \to F (x) \cos n x = F (x) \cos 0 \cdot x$
96	95	adantr	$⊢ (n = 0 \land x \in C) \to F (x) \cos n x = F (x) \cos 0 \cdot x$
97	96	itgeq2dv	$⊢ n = 0 \to \int_{C} F (x) \cos n x d x = \int_{C} F (x) \cos 0 \cdot x d x$
98	97	adantl	$⊢ (φ \land n = 0) \to \int_{C} F (x) \cos n x d x = \int_{C} F (x) \cos 0 \cdot x d x$
99	98	oveq1d	$⊢ (φ \land n = 0) \to \frac{\int_{C} F (x) \cos n x d x}{π} = \frac{\int_{C} F (x) \cos 0 \cdot x d x}{π}$
100	1 2 3 4 17	fourierdlem16	$⊢ φ \to ((A (0) \in ℝ \land (x \in C ⟼ F (x)) \in 𝐿^{1}) \land \int_{C} F (x) \cos 0 \cdot x d x \in ℝ)$
101	100	simprd	$⊢ φ \to \int_{C} F (x) \cos 0 \cdot x d x \in ℝ$
102	46	a1i	$⊢ φ \to π \in ℝ$
103	50	a1i	$⊢ φ \to π \neq 0$
104	101 102 103	redivcld	$⊢ φ \to \frac{\int_{C} F (x) \cos 0 \cdot x d x}{π} \in ℝ$
105	92 99 17 104	fvmptd	$⊢ φ \to A (0) = \frac{\int_{C} F (x) \cos 0 \cdot x d x}{π}$
106		ioosscn	$⊢ (- π, π) \subseteq ℂ$
107		id	$⊢ x \in C \to x \in C$
108	107 2	eleqtrdi	$⊢ x \in C \to x \in (- π, π)$
109	106 108	sseldi	$⊢ x \in C \to x \in ℂ$
110	109	mul02d	$⊢ x \in C \to 0 \cdot x = 0$
111	110	fveq2d	$⊢ x \in C \to \cos 0 \cdot x = \cos 0$
112		cos0	$⊢ \cos 0 = 1$
113	111 112	syl6eq	$⊢ x \in C \to \cos 0 \cdot x = 1$
114	113	oveq2d	$⊢ x \in C \to F (x) \cos 0 \cdot x = F (x) \cdot 1$
115	114	adantl	$⊢ (φ \land x \in C) \to F (x) \cos 0 \cdot x = F (x) \cdot 1$
116	1	adantr	$⊢ (φ \land x \in C) \to F : ℝ ⟶ ℝ$
117		ioossre	$⊢ (- π, π) \subseteq ℝ$
118	117 108	sseldi	$⊢ x \in C \to x \in ℝ$
119	118	adantl	$⊢ (φ \land x \in C) \to x \in ℝ$
120	116 119	ffvelrnd	$⊢ (φ \land x \in C) \to F (x) \in ℝ$
121	120	recnd	$⊢ (φ \land x \in C) \to F (x) \in ℂ$
122	121	mulid1d	$⊢ (φ \land x \in C) \to F (x) \cdot 1 = F (x)$
123	115 122	eqtrd	$⊢ (φ \land x \in C) \to F (x) \cos 0 \cdot x = F (x)$
124	123	itgeq2dv	$⊢ φ \to \int_{C} F (x) \cos 0 \cdot x d x = \int_{C} F (x) d x$
125	124	oveq1d	$⊢ φ \to \frac{\int_{C} F (x) \cos 0 \cdot x d x}{π} = \frac{\int_{C} F (x) d x}{π}$
126	105 125	eqtrd	$⊢ φ \to A (0) = \frac{\int_{C} F (x) d x}{π}$
127	126	oveq1d	$⊢ φ \to \frac{A (0)}{2} = \frac{\frac{\int_{C} F (x) d x}{π}}{2}$
128	1	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
129	128	reseq1d	$⊢ φ \to {F ↾}_{C} = {(x \in ℝ ⟼ F (x)) ↾}_{C}$
130	46	a1i	$⊢ x \in C \to π \in ℝ$
131	130	renegcld	$⊢ x \in C \to - π \in ℝ$
132		ioossicc	$⊢ (- π, π) \subseteq [- π, π]$
133	2 132	eqsstri	$⊢ C \subseteq [- π, π]$
134	133	sseli	$⊢ x \in C \to x \in [- π, π]$
135		eliccre	$⊢ (- π \in ℝ \land π \in ℝ \land x \in [- π, π]) \to x \in ℝ$
136	131 130 134 135	syl3anc	$⊢ x \in C \to x \in ℝ$
137	136	ssriv	$⊢ C \subseteq ℝ$
138		resmpt	$⊢ C \subseteq ℝ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
139	137 138	mp1i	$⊢ φ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
140	129 139	eqtr2d	$⊢ φ \to (x \in C ⟼ F (x)) = {F ↾}_{C}$
141	140 3	eqeltrd	$⊢ φ \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
142	120 141	itgcl	$⊢ φ \to \int_{C} F (x) d x \in ℂ$
143	102	recnd	$⊢ φ \to π \in ℂ$
144		2cnd	$⊢ φ \to 2 \in ℂ$
145		2ne0	$⊢ 2 \neq 0$
146	145	a1i	$⊢ φ \to 2 \neq 0$
147	142 143 144 103 146	divdiv32d	$⊢ φ \to \frac{\frac{\int_{C} F (x) d x}{π}}{2} = \frac{\frac{\int_{C} F (x) d x}{2}}{π}$
148	142 144 146	divrecd	$⊢ φ \to \frac{\int_{C} F (x) d x}{2} = \int_{C} F (x) d x (\frac{1}{2})$
149	144 146	reccld	$⊢ φ \to \frac{1}{2} \in ℂ$
150	142 149	mulcomd	$⊢ φ \to \int_{C} F (x) d x (\frac{1}{2}) = (\frac{1}{2}) \int_{C} F (x) d x$
151	149 120 141	itgmulc2	$⊢ φ \to (\frac{1}{2}) \int_{C} F (x) d x = \int_{C} (\frac{1}{2}) F (x) d x$
152	148 150 151	3eqtrd	$⊢ φ \to \frac{\int_{C} F (x) d x}{2} = \int_{C} (\frac{1}{2}) F (x) d x$
153	152	oveq1d	$⊢ φ \to \frac{\frac{\int_{C} F (x) d x}{2}}{π} = \frac{\int_{C} (\frac{1}{2}) F (x) d x}{π}$
154	127 147 153	3eqtrd	$⊢ φ \to \frac{A (0)}{2} = \frac{\int_{C} (\frac{1}{2}) F (x) d x}{π}$
155	57 52	syldan	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \cos n x d x}{π} \in ℝ$
156	4	fvmpt2	$⊢ (n \in ℕ_{0} \land \frac{\int_{C} F (x) \cos n x d x}{π} \in ℝ) \to A (n) = \frac{\int_{C} F (x) \cos n x d x}{π}$
157	57 155 156	syl2anc	$⊢ (φ \land n \in (1 \dots N)) \to A (n) = \frac{\int_{C} F (x) \cos n x d x}{π}$
158	157	oveq1d	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X = (\frac{\int_{C} F (x) \cos n x d x}{π}) \cos n X$
159	155	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \cos n x d x}{π} \in ℂ$
160	62	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \cos n X \in ℂ$
161	159 160	mulcomd	$⊢ (φ \land n \in (1 \dots N)) \to (\frac{\int_{C} F (x) \cos n x d x}{π}) \cos n X = \cos n X (\frac{\int_{C} F (x) \cos n x d x}{π})$
162	57 45	syldan	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n x d x \in ℝ$
163	162	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n x d x \in ℂ$
164	143	adantr	$⊢ (φ \land n \in (1 \dots N)) \to π \in ℂ$
165	50	a1i	$⊢ (φ \land n \in (1 \dots N)) \to π \neq 0$
166	160 163 164 165	divassd	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\cos n X \int_{C} F (x) \cos n x d x}{π} = \cos n X (\frac{\int_{C} F (x) \cos n x d x}{π})$
167	1	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F : ℝ ⟶ ℝ$
168	118	adantl	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to x \in ℝ$
169	167 168	ffvelrnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℝ$
170		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
171	170	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to n \in ℝ$
172	171 168	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to n x \in ℝ$
173	172	recoscld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x \in ℝ$
174	169 173	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \cos n x \in ℝ$
175	56 174	sylanl2	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n x \in ℝ$
176		ioombl	$⊢ (- π, π) \in dom vol$
177	2 176	eqeltri	$⊢ C \in dom vol$
178	177	elexi	$⊢ C \in V$
179	178	a1i	$⊢ (φ \land n \in ℕ_{0}) \to C \in V$
180		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) = (x \in C ⟼ \cos n x)$
181		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
182	179 173 169 180 181	offval2	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ \cos n x F (x))$
183	173	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x \in ℂ$
184	121	adantlr	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℂ$
185	183 184	mulcomd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x F (x) = F (x) \cos n x$
186	185	mpteq2dva	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x F (x)) = (x \in C ⟼ F (x) \cos n x)$
187	182 186	eqtr2d	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \cos n x) = (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x))$
188		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
189	188	a1i	$⊢ (φ \land n \in ℕ_{0}) \to \cos : ℂ \underset{cn}{⟶} ℂ$
190		ax-resscn	$⊢ ℝ \subseteq ℂ$
191	137 190	sstri	$⊢ C \subseteq ℂ$
192	191	a1i	$⊢ (φ \land n \in ℕ_{0}) \to C \subseteq ℂ$
193	170	recnd	$⊢ n \in ℕ_{0} \to n \in ℂ$
194	193	adantl	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℂ$
195		ssid	$⊢ ℂ \subseteq ℂ$
196	195	a1i	$⊢ (φ \land n \in ℕ_{0}) \to ℂ \subseteq ℂ$
197	192 194 196	constcncfg	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ n) : C \underset{cn}{⟶} ℂ$
198	192 196	idcncfg	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
199	197 198	mulcncf	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
200	189 199	cncfmpt1f	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) : C \underset{cn}{⟶} ℂ$
201		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \cos n x) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \cos n x) \in MblFn$
202	177 200 201	sylancr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \in MblFn$
203	141	adantr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
204		1re	$⊢ 1 \in ℝ$
205		simpr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to y \in dom (x \in C ⟼ \cos n x)$
206	170	adantr	$⊢ (n \in ℕ_{0} \land x \in C) \to n \in ℝ$
207	118	adantl	$⊢ (n \in ℕ_{0} \land x \in C) \to x \in ℝ$
208	206 207	remulcld	$⊢ (n \in ℕ_{0} \land x \in C) \to n x \in ℝ$
209	208	recoscld	$⊢ (n \in ℕ_{0} \land x \in C) \to \cos n x \in ℝ$
210	209	ralrimiva	$⊢ n \in ℕ_{0} \to \forall x \in C \cos n x \in ℝ$
211	210	adantr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to \forall x \in C \cos n x \in ℝ$
212		dmmptg	$⊢ \forall x \in C \cos n x \in ℝ \to dom (x \in C ⟼ \cos n x) = C$
213	211 212	syl	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to dom (x \in C ⟼ \cos n x) = C$
214	205 213	eleqtrd	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to y \in C$
215		eqidd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \cos n x) = (x \in C ⟼ \cos n x)$
216		oveq2	$⊢ x = y \to n x = n y$
217	216	fveq2d	$⊢ x = y \to \cos n x = \cos n y$
218	217	adantl	$⊢ ((n \in ℕ_{0} \land y \in C) \land x = y) \to \cos n x = \cos n y$
219		simpr	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in C$
220	170	adantr	$⊢ (n \in ℕ_{0} \land y \in C) \to n \in ℝ$
221	137 219	sseldi	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in ℝ$
222	220 221	remulcld	$⊢ (n \in ℕ_{0} \land y \in C) \to n y \in ℝ$
223	222	recoscld	$⊢ (n \in ℕ_{0} \land y \in C) \to \cos n y \in ℝ$
224	215 218 219 223	fvmptd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \cos n x) (y) = \cos n y$
225	224	fveq2d	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \cos n x) (y)\| = \|\cos n y\|$
226		abscosbd	$⊢ n y \in ℝ \to \|\cos n y\| \leq 1$
227	222 226	syl	$⊢ (n \in ℕ_{0} \land y \in C) \to \|\cos n y\| \leq 1$
228	225 227	eqbrtrd	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
229	214 228	syldan	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
230	229	ralrimiva	$⊢ n \in ℕ_{0} \to \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
231		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \cos n x) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \cos n x) (y)\| \leq 1)$
232	231	ralbidv	$⊢ b = 1 \to (\forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1)$
233	232	rspcev	$⊢ (1 \in ℝ \land \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
234	204 230 233	sylancr	$⊢ n \in ℕ_{0} \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
235	234	adantl	$⊢ (φ \land n \in ℕ_{0}) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
236		bddmulibl	$⊢ ((x \in C ⟼ \cos n x) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
237	202 203 235 236	syl3anc	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
238	187 237	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \cos n x) \in 𝐿^{1}$
239	57 238	syldan	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \cos n x) \in 𝐿^{1}$
240	160 175 239	itgmulc2	$⊢ (φ \land n \in (1 \dots N)) \to \cos n X \int_{C} F (x) \cos n x d x = \int_{C} \cos n X F (x) \cos n x d x$
241	160	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X \in ℂ$
242	121	adantlr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \in ℂ$
243	56 183	sylanl2	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n x \in ℂ$
244	241 242 243	mul12d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X F (x) \cos n x = F (x) \cos n X \cos n x$
245	241 243	mulcomd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X \cos n x = \cos n x \cos n X$
246	245	oveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n X \cos n x = F (x) \cos n x \cos n X$
247	244 246	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X F (x) \cos n x = F (x) \cos n x \cos n X$
248	247	itgeq2dv	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} \cos n X F (x) \cos n x d x = \int_{C} F (x) \cos n x \cos n X d x$
249	240 248	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to \cos n X \int_{C} F (x) \cos n x d x = \int_{C} F (x) \cos n x \cos n X d x$
250	249	oveq1d	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\cos n X \int_{C} F (x) \cos n x d x}{π} = \frac{\int_{C} F (x) \cos n x \cos n X d x}{π}$
251	166 250	eqtr3d	$⊢ (φ \land n \in (1 \dots N)) \to \cos n X (\frac{\int_{C} F (x) \cos n x d x}{π}) = \frac{\int_{C} F (x) \cos n x \cos n X d x}{π}$
252	158 161 251	3eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X = \frac{\int_{C} F (x) \cos n x \cos n X d x}{π}$
253	84 81	syldan	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \sin n x d x}{π} \in ℝ$
254	5	fvmpt2	$⊢ (n \in ℕ \land \frac{\int_{C} F (x) \sin n x d x}{π} \in ℝ) \to B (n) = \frac{\int_{C} F (x) \sin n x d x}{π}$
255	84 253 254	syl2anc	$⊢ (φ \land n \in (1 \dots N)) \to B (n) = \frac{\int_{C} F (x) \sin n x d x}{π}$
256	255	oveq1d	$⊢ (φ \land n \in (1 \dots N)) \to B (n) \sin n X = (\frac{\int_{C} F (x) \sin n x d x}{π}) \sin n X$
257	253	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \sin n x d x}{π} \in ℂ$
258	86	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \sin n X \in ℂ$
259	257 258	mulcomd	$⊢ (φ \land n \in (1 \dots N)) \to (\frac{\int_{C} F (x) \sin n x d x}{π}) \sin n X = \sin n X (\frac{\int_{C} F (x) \sin n x d x}{π})$
260	84 78	syldan	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \sin n x d x \in ℝ$
261	260	recnd	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \sin n x d x \in ℂ$
262	258 261 164 165	divassd	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\sin n X \int_{C} F (x) \sin n x d x}{π} = \sin n X (\frac{\int_{C} F (x) \sin n x d x}{π})$
263	120	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in C) \to F (x) \in ℝ$
264		nnre	$⊢ n \in ℕ \to n \in ℝ$
265	264	adantr	$⊢ (n \in ℕ \land x \in C) \to n \in ℝ$
266	118	adantl	$⊢ (n \in ℕ \land x \in C) \to x \in ℝ$
267	265 266	remulcld	$⊢ (n \in ℕ \land x \in C) \to n x \in ℝ$
268	267	resincld	$⊢ (n \in ℕ \land x \in C) \to \sin n x \in ℝ$
269	268	adantll	$⊢ ((φ \land n \in ℕ) \land x \in C) \to \sin n x \in ℝ$
270	263 269	remulcld	$⊢ ((φ \land n \in ℕ) \land x \in C) \to F (x) \sin n x \in ℝ$
271	55 270	sylanl2	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \sin n x \in ℝ$
272	178	a1i	$⊢ (φ \land n \in ℕ) \to C \in V$
273		eqidd	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
274		eqidd	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
275	272 269 263 273 274	offval2	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ \sin n x F (x))$
276	269	recnd	$⊢ ((φ \land n \in ℕ) \land x \in C) \to \sin n x \in ℂ$
277	121	adantlr	$⊢ ((φ \land n \in ℕ) \land x \in C) \to F (x) \in ℂ$
278	276 277	mulcomd	$⊢ ((φ \land n \in ℕ) \land x \in C) \to \sin n x F (x) = F (x) \sin n x$
279	278	mpteq2dva	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x F (x)) = (x \in C ⟼ F (x) \sin n x)$
280	275 279	eqtr2d	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ F (x) \sin n x) = (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x))$
281		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
282	281	a1i	$⊢ (φ \land n \in ℕ) \to \sin : ℂ \underset{cn}{⟶} ℂ$
283	191	a1i	$⊢ n \in ℕ \to C \subseteq ℂ$
284	264	recnd	$⊢ n \in ℕ \to n \in ℂ$
285	195	a1i	$⊢ n \in ℕ \to ℂ \subseteq ℂ$
286	283 284 285	constcncfg	$⊢ n \in ℕ \to (x \in C ⟼ n) : C \underset{cn}{⟶} ℂ$
287	283 285	idcncfg	$⊢ n \in ℕ \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
288	286 287	mulcncf	$⊢ n \in ℕ \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
289	288	adantl	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
290	282 289	cncfmpt1f	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ$
291		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \sin n x) \in MblFn$
292	177 290 291	sylancr	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x) \in MblFn$
293	141	adantr	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
294		simpr	$⊢ (n \in ℕ \land y \in dom (x \in C ⟼ \sin n x)) \to y \in dom (x \in C ⟼ \sin n x)$
295	268	ralrimiva	$⊢ n \in ℕ \to \forall x \in C \sin n x \in ℝ$
296		dmmptg	$⊢ \forall x \in C \sin n x \in ℝ \to dom (x \in C ⟼ \sin n x) = C$
297	295 296	syl	$⊢ n \in ℕ \to dom (x \in C ⟼ \sin n x) = C$
298	297	adantr	$⊢ (n \in ℕ \land y \in dom (x \in C ⟼ \sin n x)) \to dom (x \in C ⟼ \sin n x) = C$
299	294 298	eleqtrd	$⊢ (n \in ℕ \land y \in dom (x \in C ⟼ \sin n x)) \to y \in C$
300		eqidd	$⊢ (n \in ℕ \land y \in C) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
301	216	fveq2d	$⊢ x = y \to \sin n x = \sin n y$
302	301	adantl	$⊢ ((n \in ℕ \land y \in C) \land x = y) \to \sin n x = \sin n y$
303		simpr	$⊢ (n \in ℕ \land y \in C) \to y \in C$
304	264	adantr	$⊢ (n \in ℕ \land y \in C) \to n \in ℝ$
305	137 303	sseldi	$⊢ (n \in ℕ \land y \in C) \to y \in ℝ$
306	304 305	remulcld	$⊢ (n \in ℕ \land y \in C) \to n y \in ℝ$
307	306	resincld	$⊢ (n \in ℕ \land y \in C) \to \sin n y \in ℝ$
308	300 302 303 307	fvmptd	$⊢ (n \in ℕ \land y \in C) \to (x \in C ⟼ \sin n x) (y) = \sin n y$
309	308	fveq2d	$⊢ (n \in ℕ \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| = \|\sin n y\|$
310		abssinbd	$⊢ n y \in ℝ \to \|\sin n y\| \leq 1$
311	306 310	syl	$⊢ (n \in ℕ \land y \in C) \to \|\sin n y\| \leq 1$
312	309 311	eqbrtrd	$⊢ (n \in ℕ \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
313	299 312	syldan	$⊢ (n \in ℕ \land y \in dom (x \in C ⟼ \sin n x)) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
314	313	ralrimiva	$⊢ n \in ℕ \to \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
315		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \sin n x) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \sin n x) (y)\| \leq 1)$
316	315	ralbidv	$⊢ b = 1 \to (\forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1)$
317	316	rspcev	$⊢ (1 \in ℝ \land \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
318	204 314 317	sylancr	$⊢ n \in ℕ \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
319	318	adantl	$⊢ (φ \land n \in ℕ) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
320		bddmulibl	$⊢ ((x \in C ⟼ \sin n x) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
321	292 293 319 320	syl3anc	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
322	280 321	eqeltrd	$⊢ (φ \land n \in ℕ) \to (x \in C ⟼ F (x) \sin n x) \in 𝐿^{1}$
323	84 322	syldan	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \sin n x) \in 𝐿^{1}$
324	258 271 323	itgmulc2	$⊢ (φ \land n \in (1 \dots N)) \to \sin n X \int_{C} F (x) \sin n x d x = \int_{C} \sin n X F (x) \sin n x d x$
325	258	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X \in ℂ$
326	55 276	sylanl2	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n x \in ℂ$
327	325 242 326	mul12d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X F (x) \sin n x = F (x) \sin n X \sin n x$
328	325 326	mulcomd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X \sin n x = \sin n x \sin n X$
329	328	oveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \sin n X \sin n x = F (x) \sin n x \sin n X$
330	327 329	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X F (x) \sin n x = F (x) \sin n x \sin n X$
331	330	itgeq2dv	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} \sin n X F (x) \sin n x d x = \int_{C} F (x) \sin n x \sin n X d x$
332	324 331	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to \sin n X \int_{C} F (x) \sin n x d x = \int_{C} F (x) \sin n x \sin n X d x$
333	332	oveq1d	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\sin n X \int_{C} F (x) \sin n x d x}{π} = \frac{\int_{C} F (x) \sin n x \sin n X d x}{π}$
334	262 333	eqtr3d	$⊢ (φ \land n \in (1 \dots N)) \to \sin n X (\frac{\int_{C} F (x) \sin n x d x}{π}) = \frac{\int_{C} F (x) \sin n x \sin n X d x}{π}$
335	256 259 334	3eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to B (n) \sin n X = \frac{\int_{C} F (x) \sin n x \sin n X d x}{π}$
336	252 335	oveq12d	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X + B (n) \sin n X = (\frac{\int_{C} F (x) \cos n x \cos n X d x}{π}) + (\frac{\int_{C} F (x) \sin n x \sin n X d x}{π})$
337	56 169	sylanl2	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \in ℝ$
338	57 209	sylan	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n x \in ℝ$
339	62	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X \in ℝ$
340	338 339	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n x \cos n X \in ℝ$
341	337 340	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n x \cos n X \in ℝ$
342	242 243 241	mul13d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n x \cos n X = \cos n X \cos n x F (x)$
343	243 242	mulcomd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n x F (x) = F (x) \cos n x$
344	343	oveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n X \cos n x F (x) = \cos n X F (x) \cos n x$
345	342 344	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n x \cos n X = \cos n X F (x) \cos n x$
346	345	mpteq2dva	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \cos n x \cos n X) = (x \in C ⟼ \cos n X F (x) \cos n x)$
347	160 175 239	iblmulc2	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n X F (x) \cos n x) \in 𝐿^{1}$
348	346 347	eqeltrd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \cos n x \cos n X) \in 𝐿^{1}$
349	341 348	itgcl	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n x \cos n X d x \in ℂ$
350	84 268	sylan	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n x \in ℝ$
351	86	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X \in ℝ$
352	350 351	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n x \sin n X \in ℝ$
353	337 352	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \sin n x \sin n X \in ℝ$
354	242 326 325	mul13d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \sin n x \sin n X = \sin n X \sin n x F (x)$
355	326 242	mulcomd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n x F (x) = F (x) \sin n x$
356	355	oveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n X \sin n x F (x) = \sin n X F (x) \sin n x$
357	354 356	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \sin n x \sin n X = \sin n X F (x) \sin n x$
358	357	mpteq2dva	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \sin n x \sin n X) = (x \in C ⟼ \sin n X F (x) \sin n x)$
359	258 271 323	iblmulc2	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \sin n X F (x) \sin n x) \in 𝐿^{1}$
360	358 359	eqeltrd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \sin n x \sin n X) \in 𝐿^{1}$
361	353 360	itgcl	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \sin n x \sin n X d x \in ℂ$
362	349 361 164 165	divdird	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \cos n x \cos n X d x + \int_{C} F (x) \sin n x \sin n X d x}{π} = (\frac{\int_{C} F (x) \cos n x \cos n X d x}{π}) + (\frac{\int_{C} F (x) \sin n x \sin n X d x}{π})$
363	55	nncnd	$⊢ n \in (1 \dots N) \to n \in ℂ$
364	363	ad2antlr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n \in ℂ$
365	109	adantl	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to x \in ℂ$
366	6	recnd	$⊢ φ \to X \in ℂ$
367	366	ad2antrr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to X \in ℂ$
368	364 365 367	subdid	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n (x - X) = n x - n X$
369	368	fveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n (x - X) = \cos (n x - n X)$
370	364 365	mulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n x \in ℂ$
371	364 367	mulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n X \in ℂ$
372		cossub	$⊢ (n x \in ℂ \land n X \in ℂ) \to \cos (n x - n X) = \cos n x \cos n X + \sin n x \sin n X$
373	370 371 372	syl2anc	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos (n x - n X) = \cos n x \cos n X + \sin n x \sin n X$
374	369 373	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n (x - X) = \cos n x \cos n X + \sin n x \sin n X$
375	374	oveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n (x - X) = F (x) (\cos n x \cos n X + \sin n x \sin n X)$
376	340	recnd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n x \cos n X \in ℂ$
377	352	recnd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \sin n x \sin n X \in ℂ$
378	242 376 377	adddid	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) (\cos n x \cos n X + \sin n x \sin n X) = F (x) \cos n x \cos n X + F (x) \sin n x \sin n X$
379	375 378	eqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n (x - X) = F (x) \cos n x \cos n X + F (x) \sin n x \sin n X$
380	379	itgeq2dv	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n (x - X) d x = \int_{C} (F (x) \cos n x \cos n X + F (x) \sin n x \sin n X) d x$
381	341 348 353 360	itgadd	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} (F (x) \cos n x \cos n X + F (x) \sin n x \sin n X) d x = \int_{C} F (x) \cos n x \cos n X d x + \int_{C} F (x) \sin n x \sin n X d x$
382	380 381	eqtr2d	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n x \cos n X d x + \int_{C} F (x) \sin n x \sin n X d x = \int_{C} F (x) \cos n (x - X) d x$
383	382	oveq1d	$⊢ (φ \land n \in (1 \dots N)) \to \frac{\int_{C} F (x) \cos n x \cos n X d x + \int_{C} F (x) \sin n x \sin n X d x}{π} = \frac{\int_{C} F (x) \cos n (x - X) d x}{π}$
384	336 362 383	3eqtr2d	$⊢ (φ \land n \in (1 \dots N)) \to A (n) \cos n X + B (n) \sin n X = \frac{\int_{C} F (x) \cos n (x - X) d x}{π}$
385	384	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X) = \sum_{n = 1}^{N} (\frac{\int_{C} F (x) \cos n (x - X) d x}{π})$
386	59	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n \in ℝ$
387	118	adantl	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to x \in ℝ$
388	6	ad2antrr	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to X \in ℝ$
389	387 388	resubcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to x - X \in ℝ$
390	386 389	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to n (x - X) \in ℝ$
391	390	recoscld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n (x - X) \in ℝ$
392	337 391	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to F (x) \cos n (x - X) \in ℝ$
393	178	a1i	$⊢ (φ \land n \in (1 \dots N)) \to C \in V$
394		eqidd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X)) = (x \in C ⟼ \cos n (x - X))$
395		eqidd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
396	393 391 337 394 395	offval2	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X)) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ \cos n (x - X) F (x))$
397	391	recnd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n (x - X) \in ℂ$
398	397 242	mulcomd	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \to \cos n (x - X) F (x) = F (x) \cos n (x - X)$
399	398	mpteq2dva	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X) F (x)) = (x \in C ⟼ F (x) \cos n (x - X))$
400	396 399	eqtr2d	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \cos n (x - X)) = (x \in C ⟼ \cos n (x - X)) \times_{f} (x \in C ⟼ F (x))$
401	188	a1i	$⊢ (φ \land n \in (1 \dots N)) \to \cos : ℂ \underset{cn}{⟶} ℂ$
402	84 286	syl	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ n) : C \underset{cn}{⟶} ℂ$
403	84 287	syl	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
404	191	a1i	$⊢ (φ \land n \in (1 \dots N)) \to C \subseteq ℂ$
405	366	adantr	$⊢ (φ \land n \in (1 \dots N)) \to X \in ℂ$
406	195	a1i	$⊢ (φ \land n \in (1 \dots N)) \to ℂ \subseteq ℂ$
407	404 405 406	constcncfg	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ X) : C \underset{cn}{⟶} ℂ$
408	403 407	subcncf	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ x - X) : C \underset{cn}{⟶} ℂ$
409	402 408	mulcncf	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ n (x - X)) : C \underset{cn}{⟶} ℂ$
410	401 409	cncfmpt1f	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X)) : C \underset{cn}{⟶} ℂ$
411		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \cos n (x - X)) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \cos n (x - X)) \in MblFn$
412	177 410 411	sylancr	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X)) \in MblFn$
413	141	adantr	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
414		simpr	$⊢ ((φ \land n \in (1 \dots N)) \land y \in dom (x \in C ⟼ \cos n (x - X))) \to y \in dom (x \in C ⟼ \cos n (x - X))$
415	391	ralrimiva	$⊢ (φ \land n \in (1 \dots N)) \to \forall x \in C \cos n (x - X) \in ℝ$
416		dmmptg	$⊢ \forall x \in C \cos n (x - X) \in ℝ \to dom (x \in C ⟼ \cos n (x - X)) = C$
417	415 416	syl	$⊢ (φ \land n \in (1 \dots N)) \to dom (x \in C ⟼ \cos n (x - X)) = C$
418	417	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land y \in dom (x \in C ⟼ \cos n (x - X))) \to dom (x \in C ⟼ \cos n (x - X)) = C$
419	414 418	eleqtrd	$⊢ ((φ \land n \in (1 \dots N)) \land y \in dom (x \in C ⟼ \cos n (x - X))) \to y \in C$
420		eqidd	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to (x \in C ⟼ \cos n (x - X)) = (x \in C ⟼ \cos n (x - X))$
421		oveq1	$⊢ x = y \to x - X = y - X$
422	421	oveq2d	$⊢ x = y \to n (x - X) = n (y - X)$
423	422	fveq2d	$⊢ x = y \to \cos n (x - X) = \cos n (y - X)$
424	423	adantl	$⊢ (((φ \land n \in (1 \dots N)) \land y \in C) \land x = y) \to \cos n (x - X) = \cos n (y - X)$
425		simpr	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to y \in C$
426	59	adantr	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to n \in ℝ$
427	57 221	sylan	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to y \in ℝ$
428	6	ad2antrr	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to X \in ℝ$
429	427 428	resubcld	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to y - X \in ℝ$
430	426 429	remulcld	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to n (y - X) \in ℝ$
431	430	recoscld	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to \cos n (y - X) \in ℝ$
432	420 424 425 431	fvmptd	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to (x \in C ⟼ \cos n (x - X)) (y) = \cos n (y - X)$
433	432	fveq2d	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to \|(x \in C ⟼ \cos n (x - X)) (y)\| = \|\cos n (y - X)\|$
434		abscosbd	$⊢ n (y - X) \in ℝ \to \|\cos n (y - X)\| \leq 1$
435	430 434	syl	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to \|\cos n (y - X)\| \leq 1$
436	433 435	eqbrtrd	$⊢ ((φ \land n \in (1 \dots N)) \land y \in C) \to \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1$
437	419 436	syldan	$⊢ ((φ \land n \in (1 \dots N)) \land y \in dom (x \in C ⟼ \cos n (x - X))) \to \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1$
438	437	ralrimiva	$⊢ (φ \land n \in (1 \dots N)) \to \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1$
439		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \cos n (x - X)) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1)$
440	439	ralbidv	$⊢ b = 1 \to (\forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1)$
441	440	rspcev	$⊢ (1 \in ℝ \land \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq 1) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq b$
442	204 438 441	sylancr	$⊢ (φ \land n \in (1 \dots N)) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq b$
443		bddmulibl	$⊢ ((x \in C ⟼ \cos n (x - X)) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n (x - X)) \|(x \in C ⟼ \cos n (x - X)) (y)\| \leq b) \to (x \in C ⟼ \cos n (x - X)) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
444	412 413 442 443	syl3anc	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ \cos n (x - X)) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
445	400 444	eqeltrd	$⊢ (φ \land n \in (1 \dots N)) \to (x \in C ⟼ F (x) \cos n (x - X)) \in 𝐿^{1}$
446	392 445	itgcl	$⊢ (φ \land n \in (1 \dots N)) \to \int_{C} F (x) \cos n (x - X) d x \in ℂ$
447	30 143 446 103	fsumdivc	$⊢ φ \to \frac{\sum_{n = 1}^{N} \int_{C} F (x) \cos n (x - X) d x}{π} = \sum_{n = 1}^{N} (\frac{\int_{C} F (x) \cos n (x - X) d x}{π})$
448	177	a1i	$⊢ φ \to C \in dom vol$
449		anass	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \leftrightarrow (φ \land (n \in (1 \dots N) \land x \in C))$
450		ancom	$⊢ (n \in (1 \dots N) \land x \in C) \leftrightarrow (x \in C \land n \in (1 \dots N))$
451	450	anbi2i	$⊢ (φ \land (n \in (1 \dots N) \land x \in C)) \leftrightarrow (φ \land (x \in C \land n \in (1 \dots N)))$
452	449 451	bitri	$⊢ ((φ \land n \in (1 \dots N)) \land x \in C) \leftrightarrow (φ \land (x \in C \land n \in (1 \dots N)))$
453	452 392	sylbir	$⊢ (φ \land (x \in C \land n \in (1 \dots N))) \to F (x) \cos n (x - X) \in ℝ$
454	448 30 453 445	itgfsum	$⊢ φ \to ((x \in C ⟼ \sum_{n = 1}^{N} F (x) \cos n (x - X)) \in 𝐿^{1} \land \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x = \sum_{n = 1}^{N} \int_{C} F (x) \cos n (x - X) d x)$
455	454	simprd	$⊢ φ \to \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x = \sum_{n = 1}^{N} \int_{C} F (x) \cos n (x - X) d x$
456	455	eqcomd	$⊢ φ \to \sum_{n = 1}^{N} \int_{C} F (x) \cos n (x - X) d x = \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x$
457	456	oveq1d	$⊢ φ \to \frac{\sum_{n = 1}^{N} \int_{C} F (x) \cos n (x - X) d x}{π} = \frac{\int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π}$
458	385 447 457	3eqtr2d	$⊢ φ \to \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X) = \frac{\int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π}$
459	154 458	oveq12d	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n = 1}^{N} (A (n) \cos n X + B (n) \sin n X) = (\frac{\int_{C} (\frac{1}{2}) F (x) d x}{π}) + (\frac{\int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π})$
460	9	adantr	$⊢ (φ \land x \in C) \to N \in ℕ$
461		eqid	$⊢ D (N) = D (N)$
462		eqid	$⊢ (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s}{π}) = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s}{π})$
463	8 460 461 462	dirkertrigeq	$⊢ (φ \land x \in C) \to D (N) = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s}{π})$
464		oveq2	$⊢ s = x - X \to n s = n (x - X)$
465	464	fveq2d	$⊢ s = x - X \to \cos n s = \cos n (x - X)$
466	465	sumeq2sdv	$⊢ s = x - X \to \sum_{n = 1}^{N} \cos n s = \sum_{n = 1}^{N} \cos n (x - X)$
467	466	oveq2d	$⊢ s = x - X \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s = (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)$
468	467	oveq1d	$⊢ s = x - X \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s}{π} = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π}$
469	468	adantl	$⊢ ((φ \land x \in C) \land s = x - X) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n s}{π} = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π}$
470	6	adantr	$⊢ (φ \land x \in C) \to X \in ℝ$
471	119 470	resubcld	$⊢ (φ \land x \in C) \to x - X \in ℝ$
472		halfre	$⊢ \frac{1}{2} \in ℝ$
473	472	a1i	$⊢ (φ \land x \in C) \to \frac{1}{2} \in ℝ$
474		fzfid	$⊢ (φ \land x \in C) \to (1 \dots N) \in Fin$
475	391	an32s	$⊢ ((φ \land x \in C) \land n \in (1 \dots N)) \to \cos n (x - X) \in ℝ$
476	474 475	fsumrecl	$⊢ (φ \land x \in C) \to \sum_{n = 1}^{N} \cos n (x - X) \in ℝ$
477	473 476	readdcld	$⊢ (φ \land x \in C) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X) \in ℝ$
478	46	a1i	$⊢ (φ \land x \in C) \to π \in ℝ$
479	50	a1i	$⊢ (φ \land x \in C) \to π \neq 0$
480	477 478 479	redivcld	$⊢ (φ \land x \in C) \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π} \in ℝ$
481	463 469 471 480	fvmptd	$⊢ (φ \land x \in C) \to D (N) (x - X) = \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π}$
482	481 480	eqeltrd	$⊢ (φ \land x \in C) \to D (N) (x - X) \in ℝ$
483	120 482	remulcld	$⊢ (φ \land x \in C) \to F (x) D (N) (x - X) \in ℝ$
484	178	a1i	$⊢ φ \to C \in V$
485		eqidd	$⊢ φ \to (x \in C ⟼ D (N) (x - X)) = (x \in C ⟼ D (N) (x - X))$
486		eqidd	$⊢ φ \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
487	484 482 120 485 486	offval2	$⊢ φ \to (x \in C ⟼ D (N) (x - X)) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ D (N) (x - X) F (x))$
488	482	recnd	$⊢ (φ \land x \in C) \to D (N) (x - X) \in ℂ$
489	488 121	mulcomd	$⊢ (φ \land x \in C) \to D (N) (x - X) F (x) = F (x) D (N) (x - X)$
490	489	mpteq2dva	$⊢ φ \to (x \in C ⟼ D (N) (x - X) F (x)) = (x \in C ⟼ F (x) D (N) (x - X))$
491	487 490	eqtr2d	$⊢ φ \to (x \in C ⟼ F (x) D (N) (x - X)) = (x \in C ⟼ D (N) (x - X)) \times_{f} (x \in C ⟼ F (x))$
492		eqid	$⊢ (x \in [- π, π] ⟼ D (N) (x - X)) = (x \in [- π, π] ⟼ D (N) (x - X))$
493		eqid	$⊢ (x \in ℝ ⟼ D (N) (x - X)) = (x \in ℝ ⟼ D (N) (x - X))$
494	195	a1i	$⊢ φ \to ℂ \subseteq ℂ$
495		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
496	190 494 495	sylancr	$⊢ φ \to ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
497		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
498	6	adantr	$⊢ (φ \land x \in ℝ) \to X \in ℝ$
499	497 498	resubcld	$⊢ (φ \land x \in ℝ) \to x - X \in ℝ$
500		eqid	$⊢ (x \in ℝ ⟼ x - X) = (x \in ℝ ⟼ x - X)$
501	499 500	fmptd	$⊢ φ \to (x \in ℝ ⟼ x - X) : ℝ ⟶ ℝ$
502	190	a1i	$⊢ φ \to ℝ \subseteq ℂ$
503	502 494	idcncfg	$⊢ φ \to (x \in ℝ ⟼ x) : ℝ \underset{cn}{⟶} ℂ$
504	502 366 494	constcncfg	$⊢ φ \to (x \in ℝ ⟼ X) : ℝ \underset{cn}{⟶} ℂ$
505	503 504	subcncf	$⊢ φ \to (x \in ℝ ⟼ x - X) : ℝ \underset{cn}{⟶} ℂ$
506		cncffvrn	$⊢ (ℝ \subseteq ℂ \land (x \in ℝ ⟼ x - X) : ℝ \underset{cn}{⟶} ℂ) \to ((x \in ℝ ⟼ x - X) : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (x \in ℝ ⟼ x - X) : ℝ ⟶ ℝ)$
507	190 505 506	sylancr	$⊢ φ \to ((x \in ℝ ⟼ x - X) : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (x \in ℝ ⟼ x - X) : ℝ ⟶ ℝ)$
508	501 507	mpbird	$⊢ φ \to (x \in ℝ ⟼ x - X) : ℝ \underset{cn}{⟶} ℝ$
509	8	dirkercncf	$⊢ N \in ℕ \to D (N) : ℝ \underset{cn}{⟶} ℝ$
510	9 509	syl	$⊢ φ \to D (N) : ℝ \underset{cn}{⟶} ℝ$
511	508 510	cncfcompt	$⊢ φ \to (x \in ℝ ⟼ D (N) (x - X)) : ℝ \underset{cn}{⟶} ℝ$
512	496 511	sseldd	$⊢ φ \to (x \in ℝ ⟼ D (N) (x - X)) : ℝ \underset{cn}{⟶} ℂ$
513	46	renegcli	$⊢ - π \in ℝ$
514		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
515	513 46 514	mp2an	$⊢ [- π, π] \subseteq ℝ$
516	515	a1i	$⊢ φ \to [- π, π] \subseteq ℝ$
517	8	dirkerf	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$
518	9 517	syl	$⊢ φ \to D (N) : ℝ ⟶ ℝ$
519	518	adantr	$⊢ (φ \land x \in [- π, π]) \to D (N) : ℝ ⟶ ℝ$
520	516	sselda	$⊢ (φ \land x \in [- π, π]) \to x \in ℝ$
521	6	adantr	$⊢ (φ \land x \in [- π, π]) \to X \in ℝ$
522	520 521	resubcld	$⊢ (φ \land x \in [- π, π]) \to x - X \in ℝ$
523	519 522	ffvelrnd	$⊢ (φ \land x \in [- π, π]) \to D (N) (x - X) \in ℝ$
524	523	recnd	$⊢ (φ \land x \in [- π, π]) \to D (N) (x - X) \in ℂ$
525	493 512 516 494 524	cncfmptssg	$⊢ φ \to (x \in [- π, π] ⟼ D (N) (x - X)) : [- π, π] \underset{cn}{⟶} ℂ$
526	133	a1i	$⊢ φ \to C \subseteq [- π, π]$
527	492 525 526 494 488	cncfmptssg	$⊢ φ \to (x \in C ⟼ D (N) (x - X)) : C \underset{cn}{⟶} ℂ$
528		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ D (N) (x - X)) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ D (N) (x - X)) \in MblFn$
529	177 527 528	sylancr	$⊢ φ \to (x \in C ⟼ D (N) (x - X)) \in MblFn$
530	513	a1i	$⊢ φ \to - π \in ℝ$
531		0red	$⊢ φ \to 0 \in ℝ$
532		negpilt0	$⊢ - π < 0$
533	532	a1i	$⊢ φ \to - π < 0$
534	49	a1i	$⊢ φ \to 0 < π$
535	530 531 102 533 534	lttrd	$⊢ φ \to - π < π$
536	530 102 535	ltled	$⊢ φ \to - π \leq π$
537	493 512 516 502 523	cncfmptssg	$⊢ φ \to (x \in [- π, π] ⟼ D (N) (x - X)) : [- π, π] \underset{cn}{⟶} ℝ$
538	530 102 536 537	evthiccabs	$⊢ φ \to (\exists c \in [- π, π] \forall y \in [- π, π] \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| \land \exists z \in [- π, π] \forall w \in [- π, π] \|(x \in [- π, π] ⟼ D (N) (x - X)) (z)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (w)\|)$
539	538	simpld	$⊢ φ \to \exists c \in [- π, π] \forall y \in [- π, π] \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\|$
540		eqidd	$⊢ (φ \land y \in [- π, π]) \to (x \in [- π, π] ⟼ D (N) (x - X)) = (x \in [- π, π] ⟼ D (N) (x - X))$
541	421	fveq2d	$⊢ x = y \to D (N) (x - X) = D (N) (y - X)$
542	541	adantl	$⊢ ((φ \land y \in [- π, π]) \land x = y) \to D (N) (x - X) = D (N) (y - X)$
543		simpr	$⊢ (φ \land y \in [- π, π]) \to y \in [- π, π]$
544	518	adantr	$⊢ (φ \land y \in [- π, π]) \to D (N) : ℝ ⟶ ℝ$
545	515 543	sseldi	$⊢ (φ \land y \in [- π, π]) \to y \in ℝ$
546	6	adantr	$⊢ (φ \land y \in [- π, π]) \to X \in ℝ$
547	545 546	resubcld	$⊢ (φ \land y \in [- π, π]) \to y - X \in ℝ$
548	544 547	ffvelrnd	$⊢ (φ \land y \in [- π, π]) \to D (N) (y - X) \in ℝ$
549	540 542 543 548	fvmptd	$⊢ (φ \land y \in [- π, π]) \to (x \in [- π, π] ⟼ D (N) (x - X)) (y) = D (N) (y - X)$
550	549	fveq2d	$⊢ (φ \land y \in [- π, π]) \to \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| = \|D (N) (y - X)\|$
551	550	adantlr	$⊢ ((φ \land c \in [- π, π]) \land y \in [- π, π]) \to \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| = \|D (N) (y - X)\|$
552		eqidd	$⊢ (φ \land c \in [- π, π]) \to (x \in [- π, π] ⟼ D (N) (x - X)) = (x \in [- π, π] ⟼ D (N) (x - X))$
553		oveq1	$⊢ x = c \to x - X = c - X$
554	553	fveq2d	$⊢ x = c \to D (N) (x - X) = D (N) (c - X)$
555	554	adantl	$⊢ ((φ \land c \in [- π, π]) \land x = c) \to D (N) (x - X) = D (N) (c - X)$
556		simpr	$⊢ (φ \land c \in [- π, π]) \to c \in [- π, π]$
557	518	adantr	$⊢ (φ \land c \in [- π, π]) \to D (N) : ℝ ⟶ ℝ$
558	515 556	sseldi	$⊢ (φ \land c \in [- π, π]) \to c \in ℝ$
559	6	adantr	$⊢ (φ \land c \in [- π, π]) \to X \in ℝ$
560	558 559	resubcld	$⊢ (φ \land c \in [- π, π]) \to c - X \in ℝ$
561	557 560	ffvelrnd	$⊢ (φ \land c \in [- π, π]) \to D (N) (c - X) \in ℝ$
562	552 555 556 561	fvmptd	$⊢ (φ \land c \in [- π, π]) \to (x \in [- π, π] ⟼ D (N) (x - X)) (c) = D (N) (c - X)$
563	562	fveq2d	$⊢ (φ \land c \in [- π, π]) \to \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| = \|D (N) (c - X)\|$
564	563	adantr	$⊢ ((φ \land c \in [- π, π]) \land y \in [- π, π]) \to \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| = \|D (N) (c - X)\|$
565	551 564	breq12d	$⊢ ((φ \land c \in [- π, π]) \land y \in [- π, π]) \to (\|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| \leftrightarrow \|D (N) (y - X)\| \leq \|D (N) (c - X)\|)$
566	565	ralbidva	$⊢ (φ \land c \in [- π, π]) \to (\forall y \in [- π, π] \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| \leftrightarrow \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|)$
567	566	rexbidva	$⊢ φ \to (\exists c \in [- π, π] \forall y \in [- π, π] \|(x \in [- π, π] ⟼ D (N) (x - X)) (y)\| \leq \|(x \in [- π, π] ⟼ D (N) (x - X)) (c)\| \leftrightarrow \exists c \in [- π, π] \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|)$
568	539 567	mpbid	$⊢ φ \to \exists c \in [- π, π] \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|$
569	561	recnd	$⊢ (φ \land c \in [- π, π]) \to D (N) (c - X) \in ℂ$
570	569	abscld	$⊢ (φ \land c \in [- π, π]) \to \|D (N) (c - X)\| \in ℝ$
571	570	3adant3	$⊢ (φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \to \|D (N) (c - X)\| \in ℝ$
572		nfv	$⊢ Ⅎ y φ$
573		nfv	$⊢ Ⅎ y c \in [- π, π]$
574		nfra1	$⊢ Ⅎ y \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|$
575	572 573 574	nf3an	$⊢ Ⅎ y (φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|)$
576		simpr	$⊢ (φ \land y \in dom (x \in C ⟼ D (N) (x - X))) \to y \in dom (x \in C ⟼ D (N) (x - X))$
577	482	ralrimiva	$⊢ φ \to \forall x \in C D (N) (x - X) \in ℝ$
578		dmmptg	$⊢ \forall x \in C D (N) (x - X) \in ℝ \to dom (x \in C ⟼ D (N) (x - X)) = C$
579	577 578	syl	$⊢ φ \to dom (x \in C ⟼ D (N) (x - X)) = C$
580	579	adantr	$⊢ (φ \land y \in dom (x \in C ⟼ D (N) (x - X))) \to dom (x \in C ⟼ D (N) (x - X)) = C$
581	576 580	eleqtrd	$⊢ (φ \land y \in dom (x \in C ⟼ D (N) (x - X))) \to y \in C$
582	581	3ad2antl1	$⊢ ((φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in dom (x \in C ⟼ D (N) (x - X))) \to y \in C$
583		eqidd	$⊢ (φ \land y \in C) \to (x \in C ⟼ D (N) (x - X)) = (x \in C ⟼ D (N) (x - X))$
584	541	adantl	$⊢ ((φ \land y \in C) \land x = y) \to D (N) (x - X) = D (N) (y - X)$
585		simpr	$⊢ (φ \land y \in C) \to y \in C$
586	518	adantr	$⊢ (φ \land y \in C) \to D (N) : ℝ ⟶ ℝ$
587	137 585	sseldi	$⊢ (φ \land y \in C) \to y \in ℝ$
588	6	adantr	$⊢ (φ \land y \in C) \to X \in ℝ$
589	587 588	resubcld	$⊢ (φ \land y \in C) \to y - X \in ℝ$
590	586 589	ffvelrnd	$⊢ (φ \land y \in C) \to D (N) (y - X) \in ℝ$
591	583 584 585 590	fvmptd	$⊢ (φ \land y \in C) \to (x \in C ⟼ D (N) (x - X)) (y) = D (N) (y - X)$
592	591	fveq2d	$⊢ (φ \land y \in C) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| = \|D (N) (y - X)\|$
593	592	adantlr	$⊢ ((φ \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| = \|D (N) (y - X)\|$
594		simplr	$⊢ ((φ \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|$
595	133	sseli	$⊢ y \in C \to y \in [- π, π]$
596	595	adantl	$⊢ ((φ \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to y \in [- π, π]$
597		rspa	$⊢ (\forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\| \land y \in [- π, π]) \to \|D (N) (y - X)\| \leq \|D (N) (c - X)\|$
598	594 596 597	syl2anc	$⊢ ((φ \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to \|D (N) (y - X)\| \leq \|D (N) (c - X)\|$
599	593 598	eqbrtrd	$⊢ ((φ \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|$
600	599	3adantl2	$⊢ ((φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in C) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|$
601	582 600	syldan	$⊢ ((φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \land y \in dom (x \in C ⟼ D (N) (x - X))) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|$
602	601	ex	$⊢ (φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \to (y \in dom (x \in C ⟼ D (N) (x - X)) \to \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|)$
603	575 602	ralrimi	$⊢ (φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \to \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|$
604		breq2	$⊢ b = \|D (N) (c - X)\| \to (\|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|)$
605	604	ralbidv	$⊢ b = \|D (N) (c - X)\| \to (\forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|)$
606	605	rspcev	$⊢ (\|D (N) (c - X)\| \in ℝ \land \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq \|D (N) (c - X)\|) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b$
607	571 603 606	syl2anc	$⊢ (φ \land c \in [- π, π] \land \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\|) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b$
608	607	rexlimdv3a	$⊢ φ \to (\exists c \in [- π, π] \forall y \in [- π, π] \|D (N) (y - X)\| \leq \|D (N) (c - X)\| \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b)$
609	568 608	mpd	$⊢ φ \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b$
610		bddmulibl	$⊢ ((x \in C ⟼ D (N) (x - X)) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ D (N) (x - X)) \|(x \in C ⟼ D (N) (x - X)) (y)\| \leq b) \to (x \in C ⟼ D (N) (x - X)) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
611	529 141 609 610	syl3anc	$⊢ φ \to (x \in C ⟼ D (N) (x - X)) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
612	491 611	eqeltrd	$⊢ φ \to (x \in C ⟼ F (x) D (N) (x - X)) \in 𝐿^{1}$
613	143 483 612	itgmulc2	$⊢ φ \to π \int_{C} F (x) D (N) (x - X) d x = \int_{C} π F (x) D (N) (x - X) d x$
614	143	adantr	$⊢ (φ \land x \in C) \to π \in ℂ$
615	121 488 614	mul13d	$⊢ (φ \land x \in C) \to F (x) D (N) (x - X) π = π D (N) (x - X) F (x)$
616	489	oveq2d	$⊢ (φ \land x \in C) \to π D (N) (x - X) F (x) = π F (x) D (N) (x - X)$
617	615 616	eqtrd	$⊢ (φ \land x \in C) \to F (x) D (N) (x - X) π = π F (x) D (N) (x - X)$
618	617	itgeq2dv	$⊢ φ \to \int_{C} F (x) D (N) (x - X) π d x = \int_{C} π F (x) D (N) (x - X) d x$
619	613 618	eqtr4d	$⊢ φ \to π \int_{C} F (x) D (N) (x - X) d x = \int_{C} F (x) D (N) (x - X) π d x$
620	149	adantr	$⊢ (φ \land x \in C) \to \frac{1}{2} \in ℂ$
621	620 121	mulcomd	$⊢ (φ \land x \in C) \to (\frac{1}{2}) F (x) = F (x) (\frac{1}{2})$
622	397	an32s	$⊢ ((φ \land x \in C) \land n \in (1 \dots N)) \to \cos n (x - X) \in ℂ$
623	474 121 622	fsummulc2	$⊢ (φ \land x \in C) \to F (x) \sum_{n = 1}^{N} \cos n (x - X) = \sum_{n = 1}^{N} F (x) \cos n (x - X)$
624	623	eqcomd	$⊢ (φ \land x \in C) \to \sum_{n = 1}^{N} F (x) \cos n (x - X) = F (x) \sum_{n = 1}^{N} \cos n (x - X)$
625	621 624	oveq12d	$⊢ (φ \land x \in C) \to (\frac{1}{2}) F (x) + \sum_{n = 1}^{N} F (x) \cos n (x - X) = F (x) (\frac{1}{2}) + F (x) \sum_{n = 1}^{N} \cos n (x - X)$
626	474 622	fsumcl	$⊢ (φ \land x \in C) \to \sum_{n = 1}^{N} \cos n (x - X) \in ℂ$
627	121 620 626	adddid	$⊢ (φ \land x \in C) \to F (x) ((\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)) = F (x) (\frac{1}{2}) + F (x) \sum_{n = 1}^{N} \cos n (x - X)$
628	481	oveq1d	$⊢ (φ \land x \in C) \to D (N) (x - X) π = (\frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π}) π$
629	620 626	addcld	$⊢ (φ \land x \in C) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X) \in ℂ$
630	629 614 479	divcan1d	$⊢ (φ \land x \in C) \to (\frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)}{π}) π = (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)$
631	628 630	eqtr2d	$⊢ (φ \land x \in C) \to (\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X) = D (N) (x - X) π$
632	631	oveq2d	$⊢ (φ \land x \in C) \to F (x) ((\frac{1}{2}) + \sum_{n = 1}^{N} \cos n (x - X)) = F (x) D (N) (x - X) π$
633	625 627 632	3eqtr2rd	$⊢ (φ \land x \in C) \to F (x) D (N) (x - X) π = (\frac{1}{2}) F (x) + \sum_{n = 1}^{N} F (x) \cos n (x - X)$
634	633	itgeq2dv	$⊢ φ \to \int_{C} F (x) D (N) (x - X) π d x = \int_{C} ((\frac{1}{2}) F (x) + \sum_{n = 1}^{N} F (x) \cos n (x - X)) d x$
635		remulcl	$⊢ (\frac{1}{2} \in ℝ \land F (x) \in ℝ) \to (\frac{1}{2}) F (x) \in ℝ$
636	472 120 635	sylancr	$⊢ (φ \land x \in C) \to (\frac{1}{2}) F (x) \in ℝ$
637	149 120 141	iblmulc2	$⊢ φ \to (x \in C ⟼ (\frac{1}{2}) F (x)) \in 𝐿^{1}$
638	392	an32s	$⊢ ((φ \land x \in C) \land n \in (1 \dots N)) \to F (x) \cos n (x - X) \in ℝ$
639	474 638	fsumrecl	$⊢ (φ \land x \in C) \to \sum_{n = 1}^{N} F (x) \cos n (x - X) \in ℝ$
640	454	simpld	$⊢ φ \to (x \in C ⟼ \sum_{n = 1}^{N} F (x) \cos n (x - X)) \in 𝐿^{1}$
641	636 637 639 640	itgadd	$⊢ φ \to \int_{C} ((\frac{1}{2}) F (x) + \sum_{n = 1}^{N} F (x) \cos n (x - X)) d x = \int_{C} (\frac{1}{2}) F (x) d x + \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x$
642	619 634 641	3eqtrrd	$⊢ φ \to \int_{C} (\frac{1}{2}) F (x) d x + \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x = π \int_{C} F (x) D (N) (x - X) d x$
643	642	oveq1d	$⊢ φ \to \frac{\int_{C} (\frac{1}{2}) F (x) d x + \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π} = \frac{π \int_{C} F (x) D (N) (x - X) d x}{π}$
644	636 637	itgcl	$⊢ φ \to \int_{C} (\frac{1}{2}) F (x) d x \in ℂ$
645	639 640	itgcl	$⊢ φ \to \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x \in ℂ$
646	644 645 143 103	divdird	$⊢ φ \to \frac{\int_{C} (\frac{1}{2}) F (x) d x + \int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π} = (\frac{\int_{C} (\frac{1}{2}) F (x) d x}{π}) + (\frac{\int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π})$
647	483 612	itgcl	$⊢ φ \to \int_{C} F (x) D (N) (x - X) d x \in ℂ$
648	647 143 103	divcan3d	$⊢ φ \to \frac{π \int_{C} F (x) D (N) (x - X) d x}{π} = \int_{C} F (x) D (N) (x - X) d x$
649	643 646 648	3eqtr3d	$⊢ φ \to (\frac{\int_{C} (\frac{1}{2}) F (x) d x}{π}) + (\frac{\int_{C} \sum_{n = 1}^{N} F (x) \cos n (x - X) d x}{π}) = \int_{C} F (x) D (N) (x - X) d x$
650	91 459 649	3eqtrd	$⊢ φ \to S (N) = \int_{C} F (x) D (N) (x - X) d x$

Metamath Proof Explorer

Theorem fourierdlem83

Proof