fourierdlem112

Description: Here abbreviations (local definitions) are introduced to prove the fourier theorem. ( Zm ) is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem112.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem112.d	$⊢ D = (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	fourierdlem112.p	$⊢ P = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
	fourierdlem112.m	$⊢ φ \to M \in ℕ$
	fourierdlem112.q	$⊢ φ \to Q \in P (M)$
	fourierdlem112.n	$⊢ N = \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1$
	fourierdlem112.v	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
	fourierdlem112.x	$⊢ φ \to X \in ℝ$
	fourierdlem112.xran	$⊢ φ \to X \in ran V$
	fourierdlem112.t	$⊢ T = 2 π$
	fourierdlem112.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem112.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem112.c	$⊢ (φ \land i \in (0 ..^M)) \to C \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem112.u	$⊢ (φ \land i \in (0 ..^M)) \to U \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem112.fdvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem112.e	$⊢ φ \to E \in (({F_{ℝ}^{'} ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem112.i	$⊢ φ \to I \in (({F_{ℝ}^{'} ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem112.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem112.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem112.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fourierdlem112.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
	fourierdlem112.z	$⊢ Z = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
	fourierdlem112.23	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
	fourierdlem112.fbd	$⊢ φ \to \exists w \in ℝ \forall t \in ℝ \|F (t)\| \leq w$
	fourierdlem112.fdvbd	$⊢ φ \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
	fourierdlem112.25	$⊢ φ \to X \in ℝ$
Assertion	fourierdlem112	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2})$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem112.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem112.d	$⊢ D = (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
3		fourierdlem112.p	$⊢ P = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
4		fourierdlem112.m	$⊢ φ \to M \in ℕ$
5		fourierdlem112.q	$⊢ φ \to Q \in P (M)$
6		fourierdlem112.n	$⊢ N = \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1$
7		fourierdlem112.v	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
8		fourierdlem112.x	$⊢ φ \to X \in ℝ$
9		fourierdlem112.xran	$⊢ φ \to X \in ran V$
10		fourierdlem112.t	$⊢ T = 2 π$
11		fourierdlem112.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
12		fourierdlem112.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
13		fourierdlem112.c	$⊢ (φ \land i \in (0 ..^M)) \to C \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
14		fourierdlem112.u	$⊢ (φ \land i \in (0 ..^M)) \to U \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
15		fourierdlem112.fdvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
16		fourierdlem112.e	$⊢ φ \to E \in (({F_{ℝ}^{'} ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
17		fourierdlem112.i	$⊢ φ \to I \in (({F_{ℝ}^{'} ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
18		fourierdlem112.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
19		fourierdlem112.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
20		fourierdlem112.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
21		fourierdlem112.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
22		fourierdlem112.z	$⊢ Z = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
23		fourierdlem112.23	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
24		fourierdlem112.fbd	$⊢ φ \to \exists w \in ℝ \forall t \in ℝ \|F (t)\| \leq w$
25		fourierdlem112.fdvbd	$⊢ φ \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
26		fourierdlem112.25	$⊢ φ \to X \in ℝ$
27		fveq2	$⊢ n = j \to A (n) = A (j)$
28		oveq1	$⊢ n = j \to n X = j X$
29	28	fveq2d	$⊢ n = j \to \cos n X = \cos j X$
30	27 29	oveq12d	$⊢ n = j \to A (n) \cos n X = A (j) \cos j X$
31		fveq2	$⊢ n = j \to B (n) = B (j)$
32	28	fveq2d	$⊢ n = j \to \sin n X = \sin j X$
33	31 32	oveq12d	$⊢ n = j \to B (n) \sin n X = B (j) \sin j X$
34	30 33	oveq12d	$⊢ n = j \to A (n) \cos n X + B (n) \sin n X = A (j) \cos j X + B (j) \sin j X$
35	34	cbvmptv	$⊢ (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X) = (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)$
36	23 35	eqtri	$⊢ S = (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)$
37		seqeq3	$⊢ S = (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X) \to seq 1 (+ S) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X))$
38	36 37	mp1i	$⊢ φ \to seq 1 (+ S) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X))$
39		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
40		1zzd	$⊢ φ \to 1 \in ℤ$
41		nfv	$⊢ Ⅎ n φ$
42		nfcv	$⊢ \underline{Ⅎ} n ℕ$
43		nfcv	$⊢ \underline{Ⅎ} n (- π, 0)$
44		nfcv	$⊢ \underline{Ⅎ} n F (X + s)$
45		nfcv	$⊢ \underline{Ⅎ} n \times$
46		nfcv	$⊢ \underline{Ⅎ} n D (m) (s)$
47	44 45 46	nfov	$⊢ \underline{Ⅎ} n F (X + s) D (m) (s)$
48	43 47	nfitg	$⊢ \underline{Ⅎ} n \int_{(- π, 0)} F (X + s) D (m) (s) d s$
49	42 48	nfmpt	$⊢ \underline{Ⅎ} n (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s)$
50		nfcv	$⊢ \underline{Ⅎ} n (0, π)$
51	50 47	nfitg	$⊢ \underline{Ⅎ} n \int_{(0, π)} F (X + s) D (m) (s) d s$
52	42 51	nfmpt	$⊢ \underline{Ⅎ} n (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s)$
53		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
54	20 53	nfcxfr	$⊢ \underline{Ⅎ} n A$
55		nfcv	$⊢ \underline{Ⅎ} n 0$
56	54 55	nffv	$⊢ \underline{Ⅎ} n A (0)$
57		nfcv	$⊢ \underline{Ⅎ} n \div$
58		nfcv	$⊢ \underline{Ⅎ} n 2$
59	56 57 58	nfov	$⊢ \underline{Ⅎ} n (\frac{A (0)}{2})$
60		nfcv	$⊢ \underline{Ⅎ} n +$
61		nfcv	$⊢ \underline{Ⅎ} n (1 \dots m)$
62	61	nfsum1	$⊢ \underline{Ⅎ} n \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
63	59 60 62	nfov	$⊢ \underline{Ⅎ} n ((\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
64	42 63	nfmpt	$⊢ \underline{Ⅎ} n (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
65	22 64	nfcxfr	$⊢ \underline{Ⅎ} n Z$
66		eqid	$⊢ (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
67		picn	$⊢ π \in ℂ$
68	67	2timesi	$⊢ 2 π = π + π$
69	67 67	subnegi	$⊢ π - (- π) = π + π$
70	68 10 69	3eqtr4i	$⊢ T = π - (- π)$
71		pire	$⊢ π \in ℝ$
72	71	a1i	$⊢ φ \to π \in ℝ$
73	72	renegcld	$⊢ φ \to - π \in ℝ$
74	73 26	readdcld	$⊢ φ \to - π + X \in ℝ$
75	72 26	readdcld	$⊢ φ \to π + X \in ℝ$
76		negpilt0	$⊢ - π < 0$
77		pipos	$⊢ 0 < π$
78	71	renegcli	$⊢ - π \in ℝ$
79		0re	$⊢ 0 \in ℝ$
80	78 79 71	lttri	$⊢ (- π < 0 \land 0 < π) \to - π < π$
81	76 77 80	mp2an	$⊢ - π < π$
82	81	a1i	$⊢ φ \to - π < π$
83	73 72 26 82	ltadd1dd	$⊢ φ \to - π + X < π + X$
84		oveq1	$⊢ y = x \to y + k T = x + k T$
85	84	eleq1d	$⊢ y = x \to (y + k T \in ran Q \leftrightarrow x + k T \in ran Q)$
86	85	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
87	86	cbvrabv	$⊢ \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{x \in [- π + X, π + X] \| \exists k \in ℤ x + k T \in ran Q\}$
88	87	uneq2i	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{x \in [- π + X, π + X] \| \exists k \in ℤ x + k T \in ran Q\}$
89	70 3 4 5 74 75 83 66 88 6 7	fourierdlem54	$⊢ φ \to ((N \in ℕ \land V \in (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) (N)) \land V {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
90	89	simpld	$⊢ φ \to (N \in ℕ \land V \in (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) (N))$
91	90	simpld	$⊢ φ \to N \in ℕ$
92	90	simprd	$⊢ φ \to V \in (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) (N)$
93	1	adantr	$⊢ (φ \land i \in (0 ..^N)) \to F : ℝ ⟶ ℝ$
94		fveq2	$⊢ i = j \to p (i) = p (j)$
95		oveq1	$⊢ i = j \to i + 1 = j + 1$
96	95	fveq2d	$⊢ i = j \to p (i + 1) = p (j + 1)$
97	94 96	breq12d	$⊢ i = j \to (p (i) < p (i + 1) \leftrightarrow p (j) < p (j + 1))$
98	97	cbvralvw	$⊢ \forall i \in (0 ..^n) p (i) < p (i + 1) \leftrightarrow \forall j \in (0 ..^n) p (j) < p (j + 1)$
99	98	anbi2i	$⊢ ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1)) \leftrightarrow ((p (0) = - π \land p (n) = π) \land \forall j \in (0 ..^n) p (j) < p (j + 1))$
100	99	a1i	$⊢ p \in (ℝ^{(0 \dots n)}) \to (((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1)) \leftrightarrow ((p (0) = - π \land p (n) = π) \land \forall j \in (0 ..^n) p (j) < p (j + 1)))$
101	100	rabbiia	$⊢ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\} = \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall j \in (0 ..^n) p (j) < p (j + 1))\}$
102	101	mpteq2i	$⊢ (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall j \in (0 ..^n) p (j) < p (j + 1))\})$
103	3 102	eqtri	$⊢ P = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall j \in (0 ..^n) p (j) < p (j + 1))\})$
104	4	adantr	$⊢ (φ \land i \in (0 ..^N)) \to M \in ℕ$
105	5	adantr	$⊢ (φ \land i \in (0 ..^N)) \to Q \in P (M)$
106	11	adantlr	$⊢ ((φ \land i \in (0 ..^N)) \land x \in ℝ) \to F (x + T) = F (x)$
107		eleq1w	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
108	107	anbi2d	$⊢ i = j \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j \in (0 ..^M)))$
109		fveq2	$⊢ i = j \to Q (i) = Q (j)$
110	95	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
111	109 110	oveq12d	$⊢ i = j \to (Q (i), Q (i + 1)) = (Q (j), Q (j + 1))$
112	111	reseq2d	$⊢ i = j \to {F ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (j), Q (j + 1))}$
113	111	oveq1d	$⊢ i = j \to (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ = (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ$
114	112 113	eleq12d	$⊢ i = j \to (({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \leftrightarrow ({F ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ)$
115	108 114	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ) \leftrightarrow ((φ \land j \in (0 ..^M)) \to ({F ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ))$
116	115 12	chvarvv	$⊢ (φ \land j \in (0 ..^M)) \to ({F ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ$
117	116	adantlr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (0 ..^M)) \to ({F ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ$
118	74	adantr	$⊢ (φ \land i \in (0 ..^N)) \to - π + X \in ℝ$
119	74	rexrd	$⊢ φ \to - π + X \in ℝ^{*}$
120		pnfxr	$⊢ +∞ \in ℝ^{*}$
121	120	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
122	75	ltpnfd	$⊢ φ \to π + X < +∞$
123	119 121 75 83 122	eliood	$⊢ φ \to π + X \in (- π + X, +∞)$
124	123	adantr	$⊢ (φ \land i \in (0 ..^N)) \to π + X \in (- π + X, +∞)$
125		id	$⊢ i \in (0 ..^N) \to i \in (0 ..^N)$
126	6	oveq2i	$⊢ (0 ..^N) = (0 ..^\|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
127	125 126	eleqtrdi	$⊢ i \in (0 ..^N) \to i \in (0 ..^\|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
128	127	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i \in (0 ..^\|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
129	6	oveq2i	$⊢ (0 \dots N) = (0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1)$
130		isoeq4	$⊢ (0 \dots N) = (0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1) \to (f {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
131	129 130	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\})$
132	131	iotabii	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots N), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
133	7 132	eqtri	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
134	93 103 70 104 105 106 117 118 124 128 133	fourierdlem98	$⊢ (φ \land i \in (0 ..^N)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
135	24	adantr	$⊢ (φ \land i \in (0 ..^N)) \to \exists w \in ℝ \forall t \in ℝ \|F (t)\| \leq w$
136		nfra1	$⊢ Ⅎ t \forall t \in ℝ \|F (t)\| \leq w$
137		elioore	$⊢ t \in (V (i), V (i + 1)) \to t \in ℝ$
138		rspa	$⊢ (\forall t \in ℝ \|F (t)\| \leq w \land t \in ℝ) \to \|F (t)\| \leq w$
139	137 138	sylan2	$⊢ (\forall t \in ℝ \|F (t)\| \leq w \land t \in (V (i), V (i + 1))) \to \|F (t)\| \leq w$
140	139	ex	$⊢ \forall t \in ℝ \|F (t)\| \leq w \to (t \in (V (i), V (i + 1)) \to \|F (t)\| \leq w)$
141	136 140	ralrimi	$⊢ \forall t \in ℝ \|F (t)\| \leq w \to \forall t \in (V (i), V (i + 1)) \|F (t)\| \leq w$
142	141	reximi	$⊢ \exists w \in ℝ \forall t \in ℝ \|F (t)\| \leq w \to \exists w \in ℝ \forall t \in (V (i), V (i + 1)) \|F (t)\| \leq w$
143	135 142	syl	$⊢ (φ \land i \in (0 ..^N)) \to \exists w \in ℝ \forall t \in (V (i), V (i + 1)) \|F (t)\| \leq w$
144		ssid	$⊢ ℝ \subseteq ℝ$
145		dvfre	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
146	1 144 145	sylancl	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
147	146	adantr	$⊢ (φ \land i \in (0 ..^N)) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
148		eqid	$⊢ ℝ D F = ℝ D F$
149	71	a1i	$⊢ (φ \land i \in (0 ..^N)) \to π \in ℝ$
150	78	a1i	$⊢ (φ \land i \in (0 ..^N)) \to - π \in ℝ$
151	111	reseq2d	$⊢ i = j \to {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))} = {F_{ℝ}^{'} ↾}_{(Q (j), Q (j + 1))}$
152	151 113	eleq12d	$⊢ i = j \to (({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \leftrightarrow ({F_{ℝ}^{'} ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ)$
153	108 152	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ) \leftrightarrow ((φ \land j \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ))$
154	153 15	chvarvv	$⊢ (φ \land j \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ$
155	154	adantlr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (j), Q (j + 1))}) : (Q (j), Q (j + 1)) \underset{cn}{⟶} ℂ$
156	73 8	readdcld	$⊢ φ \to - π + X \in ℝ$
157	156	adantr	$⊢ (φ \land i \in (0 ..^N)) \to - π + X \in ℝ$
158	156	rexrd	$⊢ φ \to - π + X \in ℝ^{*}$
159	72 8	readdcld	$⊢ φ \to π + X \in ℝ$
160	73 72 8 82	ltadd1dd	$⊢ φ \to - π + X < π + X$
161	159	ltpnfd	$⊢ φ \to π + X < +∞$
162	158 121 159 160 161	eliood	$⊢ φ \to π + X \in (- π + X, +∞)$
163	162	adantr	$⊢ (φ \land i \in (0 ..^N)) \to π + X \in (- π + X, +∞)$
164		oveq1	$⊢ k = h \to k T = h T$
165	164	oveq2d	$⊢ k = h \to y + k T = y + h T$
166	165	eleq1d	$⊢ k = h \to (y + k T \in ran Q \leftrightarrow y + h T \in ran Q)$
167	166	cbvrexvw	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q$
168	167	rgenw	$⊢ \forall y \in [- π + X, π + X] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q)$
169		rabbi	$⊢ \forall y \in [- π + X, π + X] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists h \in ℤ y + h T \in ran Q) \leftrightarrow \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}$
170	168 169	mpbi	$⊢ \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}$
171	170	uneq2i	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}$
172		isoeq5	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\} \to (f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}))$
173	171 172	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\})$
174	173	iotabii	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}))$
175	133 174	eqtri	$⊢ V = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists h \in ℤ y + h T \in ran Q\}))$
176		eleq1w	$⊢ v = u \to (v \in dom F_{ℝ}^{'} \leftrightarrow u \in dom F_{ℝ}^{'})$
177		fveq2	$⊢ v = u \to F_{ℝ}^{'} (v) = F_{ℝ}^{'} (u)$
178	176 177	ifbieq1d	$⊢ v = u \to if (v \in dom F_{ℝ}^{'}, F_{ℝ}^{'} (v), 0) = if (u \in dom F_{ℝ}^{'}, F_{ℝ}^{'} (u), 0)$
179	178	cbvmptv	$⊢ (v \in ℝ ⟼ if (v \in dom F_{ℝ}^{'}, F_{ℝ}^{'} (v), 0)) = (u \in ℝ ⟼ if (u \in dom F_{ℝ}^{'}, F_{ℝ}^{'} (u), 0))$
180	93 148 103 149 150 70 104 105 106 155 157 163 128 175 179	fourierdlem97	$⊢ (φ \land i \in (0 ..^N)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
181		cncff	$⊢ ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
182		fdm	$⊢ ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ \to dom ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) = (V (i), V (i + 1))$
183	180 181 182	3syl	$⊢ (φ \land i \in (0 ..^N)) \to dom ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) = (V (i), V (i + 1))$
184		ssdmres	$⊢ (V (i), V (i + 1)) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) = (V (i), V (i + 1))$
185	183 184	sylibr	$⊢ (φ \land i \in (0 ..^N)) \to (V (i), V (i + 1)) \subseteq dom F_{ℝ}^{'}$
186	147 185	fssresd	$⊢ (φ \land i \in (0 ..^N)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ$
187		ax-resscn	$⊢ ℝ \subseteq ℂ$
188	187	a1i	$⊢ (φ \land i \in (0 ..^N)) \to ℝ \subseteq ℂ$
189		cncfcdm	$⊢ (ℝ \subseteq ℂ \land ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ) \to (({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ \leftrightarrow ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ)$
190	188 180 189	syl2anc	$⊢ (φ \land i \in (0 ..^N)) \to (({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ \leftrightarrow ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ)$
191	186 190	mpbird	$⊢ (φ \land i \in (0 ..^N)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ$
192	25	adantr	$⊢ (φ \land i \in (0 ..^N)) \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
193		nfv	$⊢ Ⅎ t (φ \land i \in (0 ..^N))$
194		nfra1	$⊢ Ⅎ t \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
195	193 194	nfan	$⊢ Ⅎ t ((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z)$
196		fvres	$⊢ t \in (V (i), V (i + 1)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t) = F_{ℝ}^{'} (t)$
197	196	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land t \in (V (i), V (i + 1))) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t) = F_{ℝ}^{'} (t)$
198	197	fveq2d	$⊢ ((φ \land i \in (0 ..^N)) \land t \in (V (i), V (i + 1))) \to \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| = \|F_{ℝ}^{'} (t)\|$
199	198	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (V (i), V (i + 1))) \to \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| = \|F_{ℝ}^{'} (t)\|$
200		simplr	$⊢ (((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (V (i), V (i + 1))) \to \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
201	185	sselda	$⊢ ((φ \land i \in (0 ..^N)) \land t \in (V (i), V (i + 1))) \to t \in dom F_{ℝ}^{'}$
202	201	adantlr	$⊢ (((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (V (i), V (i + 1))) \to t \in dom F_{ℝ}^{'}$
203		rspa	$⊢ (\forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \land t \in dom F_{ℝ}^{'}) \to \|F_{ℝ}^{'} (t)\| \leq z$
204	200 202 203	syl2anc	$⊢ (((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (V (i), V (i + 1))) \to \|F_{ℝ}^{'} (t)\| \leq z$
205	199 204	eqbrtrd	$⊢ (((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (V (i), V (i + 1))) \to \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z$
206	205	ex	$⊢ ((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \to (t \in (V (i), V (i + 1)) \to \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z)$
207	195 206	ralrimi	$⊢ ((φ \land i \in (0 ..^N)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \to \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z$
208	207	ex	$⊢ (φ \land i \in (0 ..^N)) \to (\forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \to \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z)$
209	208	reximdv	$⊢ (φ \land i \in (0 ..^N)) \to (\exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \to \exists z \in ℝ \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z)$
210	192 209	mpd	$⊢ (φ \land i \in (0 ..^N)) \to \exists z \in ℝ \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z$
211		nfra1	$⊢ Ⅎ t \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z$
212	196	eqcomd	$⊢ t \in (V (i), V (i + 1)) \to F_{ℝ}^{'} (t) = ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)$
213	212	fveq2d	$⊢ t \in (V (i), V (i + 1)) \to \|F_{ℝ}^{'} (t)\| = \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\|$
214	213	adantl	$⊢ (\forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \land t \in (V (i), V (i + 1))) \to \|F_{ℝ}^{'} (t)\| = \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\|$
215		rspa	$⊢ (\forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \land t \in (V (i), V (i + 1))) \to \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z$
216	214 215	eqbrtrd	$⊢ (\forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \land t \in (V (i), V (i + 1))) \to \|F_{ℝ}^{'} (t)\| \leq z$
217	216	ex	$⊢ \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \to (t \in (V (i), V (i + 1)) \to \|F_{ℝ}^{'} (t)\| \leq z)$
218	211 217	ralrimi	$⊢ \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \to \forall t \in (V (i), V (i + 1)) \|F_{ℝ}^{'} (t)\| \leq z$
219	218	a1i	$⊢ (φ \land i \in (0 ..^N)) \to (\forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \to \forall t \in (V (i), V (i + 1)) \|F_{ℝ}^{'} (t)\| \leq z)$
220	219	reximdv	$⊢ (φ \land i \in (0 ..^N)) \to (\exists z \in ℝ \forall t \in (V (i), V (i + 1)) \|({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) (t)\| \leq z \to \exists z \in ℝ \forall t \in (V (i), V (i + 1)) \|F_{ℝ}^{'} (t)\| \leq z)$
221	210 220	mpd	$⊢ (φ \land i \in (0 ..^N)) \to \exists z \in ℝ \forall t \in (V (i), V (i + 1)) \|F_{ℝ}^{'} (t)\| \leq z$
222		nfv	$⊢ Ⅎ i (φ \land j \in (0 ..^M))$
223		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ j / i ⦌ C$
224	223	nfel1	$⊢ Ⅎ i ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j))$
225	222 224	nfim	$⊢ Ⅎ i ((φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j)))$
226		csbeq1a	$⊢ i = j \to C = ⦋ j / i ⦌ C$
227	112 109	oveq12d	$⊢ i = j \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j)$
228	226 227	eleq12d	$⊢ i = j \to (C \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)) \leftrightarrow ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j)))$
229	108 228	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to C \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))) \leftrightarrow ((φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j))))$
230	225 229 13	chvarfv	$⊢ (φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j))$
231	230	adantlr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (0 ..^M)) \to ⦋ j / i ⦌ C \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j))$
232	93 103 70 104 105 106 117 231 118 124 128 133	fourierdlem96	$⊢ (φ \land i \in (0 ..^N)) \to if ((d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (V (i))) = Q ((y \in ℝ ⟼ sup (\{f \in (0 ..^M) \| Q (f) \leq (d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (y))\} ℝ <)) (V (i))), (j \in (0 ..^M) ⟼ ⦋ j / i ⦌ C) ((y \in ℝ ⟼ sup (\{f \in (0 ..^M) \| Q (f) \leq (d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (y))\} ℝ <)) (V (i))), F ((d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (V (i))))) \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
233		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ j / i ⦌ U$
234	233	nfel1	$⊢ Ⅎ i ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1))$
235	222 234	nfim	$⊢ Ⅎ i ((φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1)))$
236		csbeq1a	$⊢ i = j \to U = ⦋ j / i ⦌ U$
237	112 110	oveq12d	$⊢ i = j \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1)$
238	236 237	eleq12d	$⊢ i = j \to (U \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)) \leftrightarrow ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1)))$
239	108 238	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to U \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \leftrightarrow ((φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1))))$
240	235 239 14	chvarfv	$⊢ (φ \land j \in (0 ..^M)) \to ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1))$
241	240	adantlr	$⊢ ((φ \land i \in (0 ..^N)) \land j \in (0 ..^M)) \to ⦋ j / i ⦌ U \in (({F ↾}_{(Q (j), Q (j + 1))}) {lim}_{ℂ} Q (j + 1))$
242	93 103 70 104 105 106 117 241 157 163 128 133	fourierdlem99	$⊢ (φ \land i \in (0 ..^N)) \to if ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (V (i + 1)) = Q ((y \in ℝ ⟼ sup (\{h \in (0 ..^M) \| Q (h) \leq (g \in (- π, π] ⟼ if (g = π, - π, g)) ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (y))\} ℝ <)) (V (i)) + 1), (j \in (0 ..^M) ⟼ ⦋ j / i ⦌ U) ((y \in ℝ ⟼ sup (\{h \in (0 ..^M) \| Q (h) \leq (g \in (- π, π] ⟼ if (g = π, - π, g)) ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (y))\} ℝ <)) (V (i))), F ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (V (i + 1)))) \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
243		eqeq1	$⊢ g = s \to (g = 0 \leftrightarrow s = 0)$
244		oveq2	$⊢ g = s \to X + g = X + s$
245	244	fveq2d	$⊢ g = s \to F (X + g) = F (X + s)$
246		breq2	$⊢ g = s \to (0 < g \leftrightarrow 0 < s)$
247	246	ifbid	$⊢ g = s \to if (0 < g, R, L) = if (0 < s, R, L)$
248	245 247	oveq12d	$⊢ g = s \to F (X + g) - if (0 < g, R, L) = F (X + s) - if (0 < s, R, L)$
249		id	$⊢ g = s \to g = s$
250	248 249	oveq12d	$⊢ g = s \to \frac{F (X + g) - if (0 < g, R, L)}{g} = \frac{F (X + s) - if (0 < s, R, L)}{s}$
251	243 250	ifbieq2d	$⊢ g = s \to if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g}) = if (s = 0, 0, \frac{F (X + s) - if (0 < s, R, L)}{s})$
252	251	cbvmptv	$⊢ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, R, L)}{s}))$
253		eqeq1	$⊢ o = s \to (o = 0 \leftrightarrow s = 0)$
254		id	$⊢ o = s \to o = s$
255		oveq1	$⊢ o = s \to \frac{o}{2} = \frac{s}{2}$
256	255	fveq2d	$⊢ o = s \to \sin (\frac{o}{2}) = \sin (\frac{s}{2})$
257	256	oveq2d	$⊢ o = s \to 2 \sin (\frac{o}{2}) = 2 \sin (\frac{s}{2})$
258	254 257	oveq12d	$⊢ o = s \to \frac{o}{2 \sin (\frac{o}{2})} = \frac{s}{2 \sin (\frac{s}{2})}$
259	253 258	ifbieq2d	$⊢ o = s \to if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})}) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
260	259	cbvmptv	$⊢ (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
261		fveq2	$⊢ r = s \to (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) = (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (s)$
262		fveq2	$⊢ r = s \to (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r) = (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (s)$
263	261 262	oveq12d	$⊢ r = s \to (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r) = (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (s) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (s)$
264	263	cbvmptv	$⊢ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) = (s \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (s) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (s))$
265		oveq2	$⊢ d = s \to (k + (\frac{1}{2})) d = (k + (\frac{1}{2})) s$
266	265	fveq2d	$⊢ d = s \to \sin (k + (\frac{1}{2})) d = \sin (k + (\frac{1}{2})) s$
267	266	cbvmptv	$⊢ (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) = (s \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) s)$
268		fveq2	$⊢ z = s \to (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) = (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s)$
269		fveq2	$⊢ z = s \to (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z) = (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (s)$
270	268 269	oveq12d	$⊢ z = s \to (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z) = (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (s)$
271	270	cbvmptv	$⊢ (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) = (s \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (s))$
272		fveq2	$⊢ m = n \to D (m) = D (n)$
273	272	fveq1d	$⊢ m = n \to D (m) (s) = D (n) (s)$
274	273	oveq2d	$⊢ m = n \to F (X + s) D (m) (s) = F (X + s) D (n) (s)$
275	274	adantr	$⊢ (m = n \land s \in (- π, 0)) \to F (X + s) D (m) (s) = F (X + s) D (n) (s)$
276	275	itgeq2dv	$⊢ m = n \to \int_{(- π, 0)} F (X + s) D (m) (s) d s = \int_{(- π, 0)} F (X + s) D (n) (s) d s$
277	276	cbvmptv	$⊢ (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) = (n \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (n) (s) d s)$
278		oveq1	$⊢ c = k \to c + (\frac{1}{2}) = k + (\frac{1}{2})$
279	278	oveq1d	$⊢ c = k \to (c + (\frac{1}{2})) d = (k + (\frac{1}{2})) d$
280	279	fveq2d	$⊢ c = k \to \sin (c + (\frac{1}{2})) d = \sin (k + (\frac{1}{2})) d$
281	280	mpteq2dv	$⊢ c = k \to (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) = (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d)$
282	281	fveq1d	$⊢ c = k \to (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z) = (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)$
283	282	oveq2d	$⊢ c = k \to (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z) = (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)$
284	283	mpteq2dv	$⊢ c = k \to (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) = (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z))$
285	284	fveq1d	$⊢ c = k \to (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) = (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s)$
286	285	adantr	$⊢ (c = k \land s \in (- π, 0)) \to (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) = (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s)$
287	286	itgeq2dv	$⊢ c = k \to \int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s = \int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s$
288	287	oveq1d	$⊢ c = k \to \frac{\int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s}{π} = \frac{\int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s}{π}$
289	288	cbvmptv	$⊢ (c \in ℕ ⟼ \frac{\int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s}{π}) = (k \in ℕ ⟼ \frac{\int_{(- π, 0)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s}{π})$
290		oveq1	$⊢ y = s \to y \mod 2 π = s \mod 2 π$
291	290	eqeq1d	$⊢ y = s \to (y \mod 2 π = 0 \leftrightarrow s \mod 2 π = 0)$
292		oveq2	$⊢ y = s \to (m + (\frac{1}{2})) y = (m + (\frac{1}{2})) s$
293	292	fveq2d	$⊢ y = s \to \sin (m + (\frac{1}{2})) y = \sin (m + (\frac{1}{2})) s$
294		oveq1	$⊢ y = s \to \frac{y}{2} = \frac{s}{2}$
295	294	fveq2d	$⊢ y = s \to \sin (\frac{y}{2}) = \sin (\frac{s}{2})$
296	295	oveq2d	$⊢ y = s \to 2 π \sin (\frac{y}{2}) = 2 π \sin (\frac{s}{2})$
297	293 296	oveq12d	$⊢ y = s \to \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})} = \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
298	291 297	ifbieq2d	$⊢ y = s \to if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}) = if (s \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
299	298	cbvmptv	$⊢ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
300		simpl	$⊢ (m = k \land s \in ℝ) \to m = k$
301	300	oveq2d	$⊢ (m = k \land s \in ℝ) \to 2 m = 2 k$
302	301	oveq1d	$⊢ (m = k \land s \in ℝ) \to 2 m + 1 = 2 k + 1$
303	302	oveq1d	$⊢ (m = k \land s \in ℝ) \to \frac{2 m + 1}{2 π} = \frac{2 k + 1}{2 π}$
304	300	oveq1d	$⊢ (m = k \land s \in ℝ) \to m + (\frac{1}{2}) = k + (\frac{1}{2})$
305	304	oveq1d	$⊢ (m = k \land s \in ℝ) \to (m + (\frac{1}{2})) s = (k + (\frac{1}{2})) s$
306	305	fveq2d	$⊢ (m = k \land s \in ℝ) \to \sin (m + (\frac{1}{2})) s = \sin (k + (\frac{1}{2})) s$
307	306	oveq1d	$⊢ (m = k \land s \in ℝ) \to \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})} = \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
308	303 307	ifeq12d	$⊢ (m = k \land s \in ℝ) \to if (s \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}) = if (s \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
309	308	mpteq2dva	$⊢ m = k \to (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
310	299 309	eqtrid	$⊢ m = k \to (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
311	310	cbvmptv	$⊢ (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))) = (k \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
312	2 311	eqtri	$⊢ D = (k \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
313		eqid	$⊢ {(r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) ↾}_{[- π, l]} = {(r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) ↾}_{[- π, l]}$
314		eqid	$⊢ \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)) = \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))$
315		eqid	$⊢ \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1 = \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1$
316		isoeq1	$⊢ u = w \to (u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))) \leftrightarrow w {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))))$
317	316	cbviotavw	$⊢ (ι u \| u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)))) = (ι w \| w {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))))$
318		fveq2	$⊢ j = i \to V (j) = V (i)$
319	318	oveq1d	$⊢ j = i \to V (j) - X = V (i) - X$
320	319	cbvmptv	$⊢ (j \in (0 \dots N) ⟼ V (j) - X) = (i \in (0 \dots N) ⟼ V (i) - X)$
321		eqid	$⊢ (ι m \in (0 ..^N) \| ((ι u \| u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)))) (b), (ι u \| u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)))) (b + 1)) \subseteq ((j \in (0 \dots N) ⟼ V (j) - X) (m), (j \in (0 \dots N) ⟼ V (j) - X) (m + 1))) = (ι m \in (0 ..^N) \| ((ι u \| u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)))) (b), (ι u \| u {Isom}_{<, <} ((0 \dots \|\{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l))\| - 1), \{- π, l\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (- π, l)))) (b + 1)) \subseteq ((j \in (0 \dots N) ⟼ V (j) - X) (m), (j \in (0 \dots N) ⟼ V (j) - X) (m + 1)))$
322		fveq2	$⊢ a = s \to (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) = (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s)$
323		oveq2	$⊢ a = s \to (b + (\frac{1}{2})) a = (b + (\frac{1}{2})) s$
324	323	fveq2d	$⊢ a = s \to \sin (b + (\frac{1}{2})) a = \sin (b + (\frac{1}{2})) s$
325	322 324	oveq12d	$⊢ a = s \to (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a = (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s$
326	325	cbvitgv	$⊢ \int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a = \int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s$
327	326	fveq2i	$⊢ \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| = \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\|$
328	327	breq1i	$⊢ \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{i}{2} \leftrightarrow \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{i}{2}$
329	328	anbi2i	$⊢ ((((φ \land i \in ℝ^{+}) \land l \in (- π, 0)) \land b \in ℕ) \land \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{i}{2}) \leftrightarrow ((((φ \land i \in ℝ^{+}) \land l \in (- π, 0)) \land b \in ℕ) \land \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{i}{2})$
330	325	cbvitgv	$⊢ \int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a = \int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s$
331	330	fveq2i	$⊢ \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| = \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\|$
332	331	breq1i	$⊢ \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{i}{2} \leftrightarrow \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{i}{2}$
333	329 332	anbi12i	$⊢ (((((φ \land i \in ℝ^{+}) \land l \in (- π, 0)) \land b \in ℕ) \land \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{i}{2}) \land \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{i}{2}) \leftrightarrow (((((φ \land i \in ℝ^{+}) \land l \in (- π, 0)) \land b \in ℕ) \land \|\int_{(l, 0)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{i}{2}) \land \|\int_{(- π, l)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{i}{2})$
334	1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 277 289 19 18 16 17 312 313 314 315 317 320 321 333	fourierdlem103	$⊢ φ \to (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) ⇝ (\frac{L}{2})$
335		nnex	$⊢ ℕ \in V$
336	335	mptex	$⊢ (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)) \in V$
337	22 336	eqeltri	$⊢ Z \in V$
338	337	a1i	$⊢ φ \to Z \in V$
339	274	adantr	$⊢ (m = n \land s \in (0, π)) \to F (X + s) D (m) (s) = F (X + s) D (n) (s)$
340	339	itgeq2dv	$⊢ m = n \to \int_{(0, π)} F (X + s) D (m) (s) d s = \int_{(0, π)} F (X + s) D (n) (s) d s$
341	340	cbvmptv	$⊢ (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) = (n \in ℕ ⟼ \int_{(0, π)} F (X + s) D (n) (s) d s)$
342	285	adantr	$⊢ (c = k \land s \in (0, π)) \to (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) = (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s)$
343	342	itgeq2dv	$⊢ c = k \to \int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s = \int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s$
344	343	oveq1d	$⊢ c = k \to \frac{\int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s}{π} = \frac{\int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s}{π}$
345	344	cbvmptv	$⊢ (c \in ℕ ⟼ \frac{\int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (c + (\frac{1}{2})) d) (z)) (s) d s}{π}) = (k \in ℕ ⟼ \frac{\int_{(0, π)} (z \in [- π, π] ⟼ (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (z) (d \in [- π, π] ⟼ \sin (k + (\frac{1}{2})) d) (z)) (s) d s}{π})$
346		eqid	$⊢ {(r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) ↾}_{[e, π]} = {(r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) ↾}_{[e, π]}$
347		eqid	$⊢ \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)) = \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))$
348		eqid	$⊢ \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1 = \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1$
349		isoeq1	$⊢ u = v \to (u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))) \leftrightarrow v {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))))$
350	349	cbviotavw	$⊢ (ι u \| u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)))) = (ι v \| v {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))))$
351		eqid	$⊢ (ι a \in (0 ..^N) \| ((ι u \| u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)))) (b), (ι u \| u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)))) (b + 1)) \subseteq ((j \in (0 \dots N) ⟼ V (j) - X) (a), (j \in (0 \dots N) ⟼ V (j) - X) (a + 1))) = (ι a \in (0 ..^N) \| ((ι u \| u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)))) (b), (ι u \| u {Isom}_{<, <} ((0 \dots \|\{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π))\| - 1), \{e, π\} \cup (ran (j \in (0 \dots N) ⟼ V (j) - X) \cap (e, π)))) (b + 1)) \subseteq ((j \in (0 \dots N) ⟼ V (j) - X) (a), (j \in (0 \dots N) ⟼ V (j) - X) (a + 1)))$
352	325	cbvitgv	$⊢ \int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a = \int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s$
353	352	fveq2i	$⊢ \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| = \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\|$
354	353	breq1i	$⊢ \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{q}{2} \leftrightarrow \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{q}{2}$
355	354	anbi2i	$⊢ ((((φ \land q \in ℝ^{+}) \land e \in (0, π)) \land b \in ℕ) \land \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{q}{2}) \leftrightarrow ((((φ \land q \in ℝ^{+}) \land e \in (0, π)) \land b \in ℕ) \land \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{q}{2})$
356	325	cbvitgv	$⊢ \int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a = \int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s$
357	356	fveq2i	$⊢ \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| = \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\|$
358	357	breq1i	$⊢ \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{q}{2} \leftrightarrow \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{q}{2}$
359	355 358	anbi12i	$⊢ (((((φ \land q \in ℝ^{+}) \land e \in (0, π)) \land b \in ℕ) \land \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{q}{2}) \land \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (a) \sin (b + (\frac{1}{2})) a d a\| < \frac{q}{2}) \leftrightarrow (((((φ \land q \in ℝ^{+}) \land e \in (0, π)) \land b \in ℕ) \land \|\int_{(0, e)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{q}{2}) \land \|\int_{(e, π)} (r \in [- π, π] ⟼ (g \in [- π, π] ⟼ if (g = 0, 0, \frac{F (X + g) - if (0 < g, R, L)}{g})) (r) (o \in [- π, π] ⟼ if (o = 0, 1, \frac{o}{2 \sin (\frac{o}{2})})) (r)) (s) \sin (b + (\frac{1}{2})) s d s\| < \frac{q}{2})$
360	1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 341 345 19 18 16 17 312 346 347 348 350 320 351 359	fourierdlem104	$⊢ φ \to (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) ⇝ (\frac{R}{2})$
361		eqidd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) = (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s)$
362	276	adantl	$⊢ ((φ \land n \in ℕ) \land m = n) \to \int_{(- π, 0)} F (X + s) D (m) (s) d s = \int_{(- π, 0)} F (X + s) D (n) (s) d s$
363		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
364		elioore	$⊢ s \in (- π, 0) \to s \in ℝ$
365	1	adantr	$⊢ (φ \land s \in ℝ) \to F : ℝ ⟶ ℝ$
366	26	adantr	$⊢ (φ \land s \in ℝ) \to X \in ℝ$
367		simpr	$⊢ (φ \land s \in ℝ) \to s \in ℝ$
368	366 367	readdcld	$⊢ (φ \land s \in ℝ) \to X + s \in ℝ$
369	365 368	ffvelcdmd	$⊢ (φ \land s \in ℝ) \to F (X + s) \in ℝ$
370	369	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s) \in ℝ$
371	2	dirkerre	$⊢ (n \in ℕ \land s \in ℝ) \to D (n) (s) \in ℝ$
372	371	adantll	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to D (n) (s) \in ℝ$
373	370 372	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in ℝ) \to F (X + s) D (n) (s) \in ℝ$
374	364 373	sylan2	$⊢ ((φ \land n \in ℕ) \land s \in (- π, 0)) \to F (X + s) D (n) (s) \in ℝ$
375		ioossicc	$⊢ (- π, 0) \subseteq [- π, 0]$
376	78	leidi	$⊢ - π \leq - π$
377	79 71 77	ltleii	$⊢ 0 \leq π$
378		iccss	$⊢ ((- π \in ℝ \land π \in ℝ) \land (- π \leq - π \land 0 \leq π)) \to [- π, 0] \subseteq [- π, π]$
379	78 71 376 377 378	mp4an	$⊢ [- π, 0] \subseteq [- π, π]$
380	375 379	sstri	$⊢ (- π, 0) \subseteq [- π, π]$
381	380	a1i	$⊢ (φ \land n \in ℕ) \to (- π, 0) \subseteq [- π, π]$
382		ioombl	$⊢ (- π, 0) \in dom vol$
383	382	a1i	$⊢ (φ \land n \in ℕ) \to (- π, 0) \in dom vol$
384	1	adantr	$⊢ (φ \land s \in [- π, π]) \to F : ℝ ⟶ ℝ$
385	26	adantr	$⊢ (φ \land s \in [- π, π]) \to X \in ℝ$
386	73 72	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
387	386	sselda	$⊢ (φ \land s \in [- π, π]) \to s \in ℝ$
388	385 387	readdcld	$⊢ (φ \land s \in [- π, π]) \to X + s \in ℝ$
389	384 388	ffvelcdmd	$⊢ (φ \land s \in [- π, π]) \to F (X + s) \in ℝ$
390	389	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in [- π, π]) \to F (X + s) \in ℝ$
391		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
392	78 71 391	mp2an	$⊢ [- π, π] \subseteq ℝ$
393	392	sseli	$⊢ s \in [- π, π] \to s \in ℝ$
394	393 371	sylan2	$⊢ (n \in ℕ \land s \in [- π, π]) \to D (n) (s) \in ℝ$
395	394	adantll	$⊢ ((φ \land n \in ℕ) \land s \in [- π, π]) \to D (n) (s) \in ℝ$
396	390 395	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in [- π, π]) \to F (X + s) D (n) (s) \in ℝ$
397	78	a1i	$⊢ (φ \land n \in ℕ) \to - π \in ℝ$
398	71	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
399	1	adantr	$⊢ (φ \land n \in ℕ) \to F : ℝ ⟶ ℝ$
400	26	adantr	$⊢ (φ \land n \in ℕ) \to X \in ℝ$
401	91	adantr	$⊢ (φ \land n \in ℕ) \to N \in ℕ$
402	92	adantr	$⊢ (φ \land n \in ℕ) \to V \in (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π + X \land p (n) = π + X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) (N)$
403	134	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^N)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
404	232	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^N)) \to if ((d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (V (i))) = Q ((y \in ℝ ⟼ sup (\{f \in (0 ..^M) \| Q (f) \leq (d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (y))\} ℝ <)) (V (i))), (j \in (0 ..^M) ⟼ ⦋ j / i ⦌ C) ((y \in ℝ ⟼ sup (\{f \in (0 ..^M) \| Q (f) \leq (d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (y))\} ℝ <)) (V (i))), F ((d \in (- π, π] ⟼ if (d = π, - π, d)) ((c \in ℝ ⟼ c + ⌊\frac{π - c}{T}⌋ T) (V (i))))) \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
405	242	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^N)) \to if ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (V (i + 1)) = Q ((y \in ℝ ⟼ sup (\{h \in (0 ..^M) \| Q (h) \leq (g \in (- π, π] ⟼ if (g = π, - π, g)) ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (y))\} ℝ <)) (V (i)) + 1), (j \in (0 ..^M) ⟼ ⦋ j / i ⦌ U) ((y \in ℝ ⟼ sup (\{h \in (0 ..^M) \| Q (h) \leq (g \in (- π, π] ⟼ if (g = π, - π, g)) ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (y))\} ℝ <)) (V (i))), F ((e \in ℝ ⟼ e + ⌊\frac{π - e}{T}⌋ T) (V (i + 1)))) \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
406	2	dirkercncf	$⊢ n \in ℕ \to D (n) : ℝ \underset{cn}{⟶} ℝ$
407	406	adantl	$⊢ (φ \land n \in ℕ) \to D (n) : ℝ \underset{cn}{⟶} ℝ$
408		eqid	$⊢ (s \in [- π, π] ⟼ F (X + s) D (n) (s)) = (s \in [- π, π] ⟼ F (X + s) D (n) (s))$
409	397 398 399 400 66 401 402 403 404 405 320 3 407 408	fourierdlem84	$⊢ (φ \land n \in ℕ) \to (s \in [- π, π] ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
410	381 383 396 409	iblss	$⊢ (φ \land n \in ℕ) \to (s \in (- π, 0) ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
411	374 410	itgcl	$⊢ (φ \land n \in ℕ) \to \int_{(- π, 0)} F (X + s) D (n) (s) d s \in ℂ$
412	361 362 363 411	fvmptd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s$
413	412 411	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) (n) \in ℂ$
414		eqidd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) = (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s)$
415	340	adantl	$⊢ ((φ \land n \in ℕ) \land m = n) \to \int_{(0, π)} F (X + s) D (m) (s) d s = \int_{(0, π)} F (X + s) D (n) (s) d s$
416	1	adantr	$⊢ (φ \land s \in (0, π)) \to F : ℝ ⟶ ℝ$
417	26	adantr	$⊢ (φ \land s \in (0, π)) \to X \in ℝ$
418		elioore	$⊢ s \in (0, π) \to s \in ℝ$
419	418	adantl	$⊢ (φ \land s \in (0, π)) \to s \in ℝ$
420	417 419	readdcld	$⊢ (φ \land s \in (0, π)) \to X + s \in ℝ$
421	416 420	ffvelcdmd	$⊢ (φ \land s \in (0, π)) \to F (X + s) \in ℝ$
422	421	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to F (X + s) \in ℝ$
423	418 371	sylan2	$⊢ (n \in ℕ \land s \in (0, π)) \to D (n) (s) \in ℝ$
424	423	adantll	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to D (n) (s) \in ℝ$
425	422 424	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in (0, π)) \to F (X + s) D (n) (s) \in ℝ$
426		ioossicc	$⊢ (0, π) \subseteq [0, π]$
427	78 79 76	ltleii	$⊢ - π \leq 0$
428	71	leidi	$⊢ π \leq π$
429		iccss	$⊢ ((- π \in ℝ \land π \in ℝ) \land (- π \leq 0 \land π \leq π)) \to [0, π] \subseteq [- π, π]$
430	78 71 427 428 429	mp4an	$⊢ [0, π] \subseteq [- π, π]$
431	426 430	sstri	$⊢ (0, π) \subseteq [- π, π]$
432	431	a1i	$⊢ (φ \land n \in ℕ) \to (0, π) \subseteq [- π, π]$
433		ioombl	$⊢ (0, π) \in dom vol$
434	433	a1i	$⊢ (φ \land n \in ℕ) \to (0, π) \in dom vol$
435	432 434 396 409	iblss	$⊢ (φ \land n \in ℕ) \to (s \in (0, π) ⟼ F (X + s) D (n) (s)) \in 𝐿^{1}$
436	425 435	itgcl	$⊢ (φ \land n \in ℕ) \to \int_{(0, π)} F (X + s) D (n) (s) d s \in ℂ$
437	414 415 363 436	fvmptd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) (n) = \int_{(0, π)} F (X + s) D (n) (s) d s$
438	437 436	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) (n) \in ℂ$
439		eleq1w	$⊢ m = n \to (m \in ℕ \leftrightarrow n \in ℕ)$
440	439	anbi2d	$⊢ m = n \to ((φ \land m \in ℕ) \leftrightarrow (φ \land n \in ℕ))$
441		fveq2	$⊢ m = n \to Z (m) = Z (n)$
442	276 340	oveq12d	$⊢ m = n \to \int_{(- π, 0)} F (X + s) D (m) (s) d s + \int_{(0, π)} F (X + s) D (m) (s) d s = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$
443	441 442	eqeq12d	$⊢ m = n \to (Z (m) = \int_{(- π, 0)} F (X + s) D (m) (s) d s + \int_{(0, π)} F (X + s) D (m) (s) d s \leftrightarrow Z (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s)$
444	440 443	imbi12d	$⊢ m = n \to (((φ \land m \in ℕ) \to Z (m) = \int_{(- π, 0)} F (X + s) D (m) (s) d s + \int_{(0, π)} F (X + s) D (m) (s) d s) \leftrightarrow ((φ \land n \in ℕ) \to Z (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s))$
445		oveq1	$⊢ n = m \to n x = m x$
446	445	fveq2d	$⊢ n = m \to \cos n x = \cos m x$
447	446	oveq2d	$⊢ n = m \to F (x) \cos n x = F (x) \cos m x$
448	447	adantr	$⊢ (n = m \land x \in (- π, π)) \to F (x) \cos n x = F (x) \cos m x$
449	448	itgeq2dv	$⊢ n = m \to \int_{(- π, π)} F (x) \cos n x d x = \int_{(- π, π)} F (x) \cos m x d x$
450	449	oveq1d	$⊢ n = m \to \frac{\int_{(- π, π)} F (x) \cos n x d x}{π} = \frac{\int_{(- π, π)} F (x) \cos m x d x}{π}$
451	450	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π}) = (m \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos m x d x}{π})$
452	20 451	eqtri	$⊢ A = (m \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos m x d x}{π})$
453	445	fveq2d	$⊢ n = m \to \sin n x = \sin m x$
454	453	oveq2d	$⊢ n = m \to F (x) \sin n x = F (x) \sin m x$
455	454	adantr	$⊢ (n = m \land x \in (- π, π)) \to F (x) \sin n x = F (x) \sin m x$
456	455	itgeq2dv	$⊢ n = m \to \int_{(- π, π)} F (x) \sin n x d x = \int_{(- π, π)} F (x) \sin m x d x$
457	456	oveq1d	$⊢ n = m \to \frac{\int_{(- π, π)} F (x) \sin n x d x}{π} = \frac{\int_{(- π, π)} F (x) \sin m x d x}{π}$
458	457	cbvmptv	$⊢ (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π}) = (m \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin m x d x}{π})$
459	21 458	eqtri	$⊢ B = (m \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin m x d x}{π})$
460		fveq2	$⊢ n = k \to A (n) = A (k)$
461		oveq1	$⊢ n = k \to n X = k X$
462	461	fveq2d	$⊢ n = k \to \cos n X = \cos k X$
463	460 462	oveq12d	$⊢ n = k \to A (n) \cos n X = A (k) \cos k X$
464		fveq2	$⊢ n = k \to B (n) = B (k)$
465	461	fveq2d	$⊢ n = k \to \sin n X = \sin k X$
466	464 465	oveq12d	$⊢ n = k \to B (n) \sin n X = B (k) \sin k X$
467	463 466	oveq12d	$⊢ n = k \to A (n) \cos n X + B (n) \sin n X = A (k) \cos k X + B (k) \sin k X$
468	467	cbvsumv	$⊢ \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
469	468	oveq2i	$⊢ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = (\frac{A (0)}{2}) + \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
470	469	mpteq2i	$⊢ (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)) = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X))$
471		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
472	471	sumeq1d	$⊢ m = n \to \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)$
473	472	oveq2d	$⊢ m = n \to (\frac{A (0)}{2}) + \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) = (\frac{A (0)}{2}) + \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)$
474	473	cbvmptv	$⊢ (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)) = (n \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X))$
475		fveq2	$⊢ k = m \to A (k) = A (m)$
476		oveq1	$⊢ k = m \to k X = m X$
477	476	fveq2d	$⊢ k = m \to \cos k X = \cos m X$
478	475 477	oveq12d	$⊢ k = m \to A (k) \cos k X = A (m) \cos m X$
479		fveq2	$⊢ k = m \to B (k) = B (m)$
480	476	fveq2d	$⊢ k = m \to \sin k X = \sin m X$
481	479 480	oveq12d	$⊢ k = m \to B (k) \sin k X = B (m) \sin m X$
482	478 481	oveq12d	$⊢ k = m \to A (k) \cos k X + B (k) \sin k X = A (m) \cos m X + B (m) \sin m X$
483	482	cbvsumv	$⊢ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = \sum_{m = 1}^{n} (A (m) \cos m X + B (m) \sin m X)$
484	483	oveq2i	$⊢ (\frac{A (0)}{2}) + \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = (\frac{A (0)}{2}) + \sum_{m = 1}^{n} (A (m) \cos m X + B (m) \sin m X)$
485	484	mpteq2i	$⊢ (n \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) = (n \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{m = 1}^{n} (A (m) \cos m X + B (m) \sin m X))$
486	474 485	eqtri	$⊢ (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)) = (n \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{m = 1}^{n} (A (m) \cos m X + B (m) \sin m X))$
487	22 470 486	3eqtri	$⊢ Z = (n \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{m = 1}^{n} (A (m) \cos m X + B (m) \sin m X))$
488		oveq2	$⊢ y = x \to X + y = X + x$
489	488	fveq2d	$⊢ y = x \to F (X + y) = F (X + x)$
490		fveq2	$⊢ y = x \to D (m) (y) = D (m) (x)$
491	489 490	oveq12d	$⊢ y = x \to F (X + y) D (m) (y) = F (X + x) D (m) (x)$
492	491	cbvmptv	$⊢ (y \in ℝ ⟼ F (X + y) D (m) (y)) = (x \in ℝ ⟼ F (X + x) D (m) (x))$
493		eqid	$⊢ (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π - X \land p (n) = π - X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\}) = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π - X \land p (n) = π - X) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
494		fveq2	$⊢ j = i \to Q (j) = Q (i)$
495	494	oveq1d	$⊢ j = i \to Q (j) - X = Q (i) - X$
496	495	cbvmptv	$⊢ (j \in (0 \dots M) ⟼ Q (j) - X) = (i \in (0 \dots M) ⟼ Q (i) - X)$
497	452 459 487 2 3 4 5 8 1 11 492 12 13 14 10 493 496	fourierdlem111	$⊢ (φ \land m \in ℕ) \to Z (m) = \int_{(- π, 0)} F (X + s) D (m) (s) d s + \int_{(0, π)} F (X + s) D (m) (s) d s$
498	444 497	chvarvv	$⊢ (φ \land n \in ℕ) \to Z (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$
499	412 437	oveq12d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) (n) + (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) (n) = \int_{(- π, 0)} F (X + s) D (n) (s) d s + \int_{(0, π)} F (X + s) D (n) (s) d s$
500	498 499	eqtr4d	$⊢ (φ \land n \in ℕ) \to Z (n) = (m \in ℕ ⟼ \int_{(- π, 0)} F (X + s) D (m) (s) d s) (n) + (m \in ℕ ⟼ \int_{(0, π)} F (X + s) D (m) (s) d s) (n)$
501	41 49 52 65 39 40 334 338 360 413 438 500	climaddf	$⊢ φ \to Z ⇝ ((\frac{L}{2}) + (\frac{R}{2}))$
502		limccl	$⊢ ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \subseteq ℂ$
503	502 18	sselid	$⊢ φ \to L \in ℂ$
504		limccl	$⊢ ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \subseteq ℂ$
505	504 19	sselid	$⊢ φ \to R \in ℂ$
506		2cnd	$⊢ φ \to 2 \in ℂ$
507		2pos	$⊢ 0 < 2$
508	507	a1i	$⊢ φ \to 0 < 2$
509	508	gt0ne0d	$⊢ φ \to 2 \neq 0$
510	503 505 506 509	divdird	$⊢ φ \to \frac{L + R}{2} = (\frac{L}{2}) + (\frac{R}{2})$
511	501 510	breqtrrd	$⊢ φ \to Z ⇝ (\frac{L + R}{2})$
512		0nn0	$⊢ 0 \in ℕ_{0}$
513	1	adantr	$⊢ (φ \land 0 \in ℕ_{0}) \to F : ℝ ⟶ ℝ$
514		eqid	$⊢ (- π, π) = (- π, π)$
515		ioossre	$⊢ (- π, π) \subseteq ℝ$
516	515	a1i	$⊢ φ \to (- π, π) \subseteq ℝ$
517	1 516	feqresmpt	$⊢ φ \to {F ↾}_{(- π, π)} = (x \in (- π, π) ⟼ F (x))$
518		ioossicc	$⊢ (- π, π) \subseteq [- π, π]$
519	518	a1i	$⊢ φ \to (- π, π) \subseteq [- π, π]$
520		ioombl	$⊢ (- π, π) \in dom vol$
521	520	a1i	$⊢ φ \to (- π, π) \in dom vol$
522	1	adantr	$⊢ (φ \land x \in [- π, π]) \to F : ℝ ⟶ ℝ$
523	386	sselda	$⊢ (φ \land x \in [- π, π]) \to x \in ℝ$
524	522 523	ffvelcdmd	$⊢ (φ \land x \in [- π, π]) \to F (x) \in ℝ$
525	1 386	feqresmpt	$⊢ φ \to {F ↾}_{[- π, π]} = (x \in [- π, π] ⟼ F (x))$
526	187	a1i	$⊢ φ \to ℝ \subseteq ℂ$
527	1 526	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
528	527 386	fssresd	$⊢ φ \to ({F ↾}_{[- π, π]}) : [- π, π] ⟶ ℂ$
529		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
530	78	rexri	$⊢ - π \in ℝ^{*}$
531	530	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
532	71	rexri	$⊢ π \in ℝ^{*}$
533	532	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
534	3 4 5	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
535	534	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
536		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
537	531 533 535 536	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
538	529 537	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
539	538	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (i), Q (i + 1))}$
540	539 12	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
541	539	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = {({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}$
542	541	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
543	13 542	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to C \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
544	541	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
545	14 544	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to U \in (({({F ↾}_{[- π, π]}) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
546	3 4 5 528 540 543 545	fourierdlem69	$⊢ φ \to {F ↾}_{[- π, π]} \in 𝐿^{1}$
547	525 546	eqeltrrd	$⊢ φ \to (x \in [- π, π] ⟼ F (x)) \in 𝐿^{1}$
548	519 521 524 547	iblss	$⊢ φ \to (x \in (- π, π) ⟼ F (x)) \in 𝐿^{1}$
549	517 548	eqeltrd	$⊢ φ \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
550	549	adantr	$⊢ (φ \land 0 \in ℕ_{0}) \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
551		simpr	$⊢ (φ \land 0 \in ℕ_{0}) \to 0 \in ℕ_{0}$
552	513 514 550 20 551	fourierdlem16	$⊢ (φ \land 0 \in ℕ_{0}) \to ((A (0) \in ℝ \land (x \in (- π, π) ⟼ F (x)) \in 𝐿^{1}) \land \int_{(- π, π)} F (x) \cos 0 \cdot x d x \in ℝ)$
553	552	simplld	$⊢ (φ \land 0 \in ℕ_{0}) \to A (0) \in ℝ$
554	512 553	mpan2	$⊢ φ \to A (0) \in ℝ$
555	554	rehalfcld	$⊢ φ \to \frac{A (0)}{2} \in ℝ$
556	555	recnd	$⊢ φ \to \frac{A (0)}{2} \in ℂ$
557	335	mptex	$⊢ (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) \in V$
558	557	a1i	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) \in V$
559		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
560	555	adantr	$⊢ (φ \land m \in ℕ) \to \frac{A (0)}{2} \in ℝ$
561		fzfid	$⊢ (φ \land m \in ℕ) \to (1 \dots m) \in Fin$
562		simpll	$⊢ ((φ \land m \in ℕ) \land n \in (1 \dots m)) \to φ$
563		elfznn	$⊢ n \in (1 \dots m) \to n \in ℕ$
564	563	adantl	$⊢ ((φ \land m \in ℕ) \land n \in (1 \dots m)) \to n \in ℕ$
565		simpl	$⊢ (φ \land n \in ℕ) \to φ$
566	363	nnnn0d	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
567		eleq1w	$⊢ k = n \to (k \in ℕ_{0} \leftrightarrow n \in ℕ_{0})$
568	567	anbi2d	$⊢ k = n \to ((φ \land k \in ℕ_{0}) \leftrightarrow (φ \land n \in ℕ_{0}))$
569		fveq2	$⊢ k = n \to A (k) = A (n)$
570	569	eleq1d	$⊢ k = n \to (A (k) \in ℝ \leftrightarrow A (n) \in ℝ)$
571	568 570	imbi12d	$⊢ k = n \to (((φ \land k \in ℕ_{0}) \to A (k) \in ℝ) \leftrightarrow ((φ \land n \in ℕ_{0}) \to A (n) \in ℝ))$
572	1	adantr	$⊢ (φ \land k \in ℕ_{0}) \to F : ℝ ⟶ ℝ$
573	549	adantr	$⊢ (φ \land k \in ℕ_{0}) \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
574		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
575	572 514 573 20 574	fourierdlem16	$⊢ (φ \land k \in ℕ_{0}) \to ((A (k) \in ℝ \land (x \in (- π, π) ⟼ F (x)) \in 𝐿^{1}) \land \int_{(- π, π)} F (x) \cos k x d x \in ℝ)$
576	575	simplld	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in ℝ$
577	571 576	chvarvv	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℝ$
578	565 566 577	syl2anc	$⊢ (φ \land n \in ℕ) \to A (n) \in ℝ$
579	363	nnred	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
580	579 400	remulcld	$⊢ (φ \land n \in ℕ) \to n X \in ℝ$
581	580	recoscld	$⊢ (φ \land n \in ℕ) \to \cos n X \in ℝ$
582	578 581	remulcld	$⊢ (φ \land n \in ℕ) \to A (n) \cos n X \in ℝ$
583		eleq1w	$⊢ k = n \to (k \in ℕ \leftrightarrow n \in ℕ)$
584	583	anbi2d	$⊢ k = n \to ((φ \land k \in ℕ) \leftrightarrow (φ \land n \in ℕ))$
585		fveq2	$⊢ k = n \to B (k) = B (n)$
586	585	eleq1d	$⊢ k = n \to (B (k) \in ℝ \leftrightarrow B (n) \in ℝ)$
587	584 586	imbi12d	$⊢ k = n \to (((φ \land k \in ℕ) \to B (k) \in ℝ) \leftrightarrow ((φ \land n \in ℕ) \to B (n) \in ℝ))$
588	1	adantr	$⊢ (φ \land k \in ℕ) \to F : ℝ ⟶ ℝ$
589	549	adantr	$⊢ (φ \land k \in ℕ) \to {F ↾}_{(- π, π)} \in 𝐿^{1}$
590		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
591	588 514 589 21 590	fourierdlem21	$⊢ (φ \land k \in ℕ) \to ((B (k) \in ℝ \land (x \in (- π, π) ⟼ F (x) \sin k x) \in 𝐿^{1}) \land \int_{(- π, π)} F (x) \sin k x d x \in ℝ)$
592	591	simplld	$⊢ (φ \land k \in ℕ) \to B (k) \in ℝ$
593	587 592	chvarvv	$⊢ (φ \land n \in ℕ) \to B (n) \in ℝ$
594	580	resincld	$⊢ (φ \land n \in ℕ) \to \sin n X \in ℝ$
595	593 594	remulcld	$⊢ (φ \land n \in ℕ) \to B (n) \sin n X \in ℝ$
596	582 595	readdcld	$⊢ (φ \land n \in ℕ) \to A (n) \cos n X + B (n) \sin n X \in ℝ$
597	562 564 596	syl2anc	$⊢ ((φ \land m \in ℕ) \land n \in (1 \dots m)) \to A (n) \cos n X + B (n) \sin n X \in ℝ$
598	561 597	fsumrecl	$⊢ (φ \land m \in ℕ) \to \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in ℝ$
599	560 598	readdcld	$⊢ (φ \land m \in ℕ) \to (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in ℝ$
600	22	fvmpt2	$⊢ (m \in ℕ \land (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in ℝ) \to Z (m) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
601	559 599 600	syl2anc	$⊢ (φ \land m \in ℕ) \to Z (m) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
602	601 599	eqeltrd	$⊢ (φ \land m \in ℕ) \to Z (m) \in ℝ$
603	602	recnd	$⊢ (φ \land m \in ℕ) \to Z (m) \in ℂ$
604		eqidd	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) = (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X))$
605		oveq2	$⊢ n = m \to (1 \dots n) = (1 \dots m)$
606	605	sumeq1d	$⊢ n = m \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
607	606	adantl	$⊢ ((φ \land m \in ℕ) \land n = m) \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
608		sumex	$⊢ \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) \in V$
609	608	a1i	$⊢ (φ \land m \in ℕ) \to \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) \in V$
610	604 607 559 609	fvmptd	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) (m) = \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
611	560	recnd	$⊢ (φ \land m \in ℕ) \to \frac{A (0)}{2} \in ℂ$
612	598	recnd	$⊢ (φ \land m \in ℕ) \to \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in ℂ$
613	611 612	pncan2d	$⊢ (φ \land m \in ℕ) \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}^{m} (A (n) \cos n X + B (n) \sin n X)$
614	613 468	eqtr2di	$⊢ (φ \land m \in ℕ) \to \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) - (\frac{A (0)}{2})$
615		ovex	$⊢ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in V$
616	22	fvmpt2	$⊢ (m \in ℕ \land (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) \in V) \to Z (m) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
617	559 615 616	sylancl	$⊢ (φ \land m \in ℕ) \to Z (m) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
618	617	eqcomd	$⊢ (φ \land m \in ℕ) \to (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = Z (m)$
619	618	oveq1d	$⊢ (φ \land m \in ℕ) \to (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) - (\frac{A (0)}{2}) = Z (m) - (\frac{A (0)}{2})$
620	610 614 619	3eqtrd	$⊢ (φ \land m \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) (m) = Z (m) - (\frac{A (0)}{2})$
621	39 40 511 556 558 603 620	climsubc1	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$
622		seqex	$⊢ seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) \in V$
623	622	a1i	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) \in V$
624		eqidd	$⊢ (φ \land l \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) = (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X))$
625		oveq2	$⊢ n = l \to (1 \dots n) = (1 \dots l)$
626	625	sumeq1d	$⊢ n = l \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X)$
627	626	adantl	$⊢ ((φ \land l \in ℕ) \land n = l) \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X)$
628		simpr	$⊢ (φ \land l \in ℕ) \to l \in ℕ$
629		fzfid	$⊢ (φ \land l \in ℕ) \to (1 \dots l) \in Fin$
630		elfznn	$⊢ k \in (1 \dots l) \to k \in ℕ$
631	630	nnnn0d	$⊢ k \in (1 \dots l) \to k \in ℕ_{0}$
632	631 576	sylan2	$⊢ (φ \land k \in (1 \dots l)) \to A (k) \in ℝ$
633	630	nnred	$⊢ k \in (1 \dots l) \to k \in ℝ$
634	633	adantl	$⊢ (φ \land k \in (1 \dots l)) \to k \in ℝ$
635	8	adantr	$⊢ (φ \land k \in (1 \dots l)) \to X \in ℝ$
636	634 635	remulcld	$⊢ (φ \land k \in (1 \dots l)) \to k X \in ℝ$
637	636	recoscld	$⊢ (φ \land k \in (1 \dots l)) \to \cos k X \in ℝ$
638	632 637	remulcld	$⊢ (φ \land k \in (1 \dots l)) \to A (k) \cos k X \in ℝ$
639	630 592	sylan2	$⊢ (φ \land k \in (1 \dots l)) \to B (k) \in ℝ$
640	636	resincld	$⊢ (φ \land k \in (1 \dots l)) \to \sin k X \in ℝ$
641	639 640	remulcld	$⊢ (φ \land k \in (1 \dots l)) \to B (k) \sin k X \in ℝ$
642	638 641	readdcld	$⊢ (φ \land k \in (1 \dots l)) \to A (k) \cos k X + B (k) \sin k X \in ℝ$
643	642	adantlr	$⊢ ((φ \land l \in ℕ) \land k \in (1 \dots l)) \to A (k) \cos k X + B (k) \sin k X \in ℝ$
644	629 643	fsumrecl	$⊢ (φ \land l \in ℕ) \to \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X) \in ℝ$
645	624 627 628 644	fvmptd	$⊢ (φ \land l \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) (l) = \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X)$
646		eleq1w	$⊢ n = l \to (n \in ℕ \leftrightarrow l \in ℕ)$
647	646	anbi2d	$⊢ n = l \to ((φ \land n \in ℕ) \leftrightarrow (φ \land l \in ℕ))$
648		fveq2	$⊢ n = l \to seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (n) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (l)$
649	626 648	eqeq12d	$⊢ n = l \to (\sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (n) \leftrightarrow \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (l))$
650	647 649	imbi12d	$⊢ n = l \to (((φ \land n \in ℕ) \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (n)) \leftrightarrow ((φ \land l \in ℕ) \to \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (l)))$
651		eqidd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X) = (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)$
652		fveq2	$⊢ j = k \to A (j) = A (k)$
653		oveq1	$⊢ j = k \to j X = k X$
654	653	fveq2d	$⊢ j = k \to \cos j X = \cos k X$
655	652 654	oveq12d	$⊢ j = k \to A (j) \cos j X = A (k) \cos k X$
656		fveq2	$⊢ j = k \to B (j) = B (k)$
657	653	fveq2d	$⊢ j = k \to \sin j X = \sin k X$
658	656 657	oveq12d	$⊢ j = k \to B (j) \sin j X = B (k) \sin k X$
659	655 658	oveq12d	$⊢ j = k \to A (j) \cos j X + B (j) \sin j X = A (k) \cos k X + B (k) \sin k X$
660	659	adantl	$⊢ (((φ \land n \in ℕ) \land k \in (1 \dots n)) \land j = k) \to A (j) \cos j X + B (j) \sin j X = A (k) \cos k X + B (k) \sin k X$
661		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
662	661	adantl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
663		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
664		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
665		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
666	665	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℝ$
667	8	adantr	$⊢ (φ \land k \in ℕ_{0}) \to X \in ℝ$
668	666 667	remulcld	$⊢ (φ \land k \in ℕ_{0}) \to k X \in ℝ$
669	668	recoscld	$⊢ (φ \land k \in ℕ_{0}) \to \cos k X \in ℝ$
670	576 669	remulcld	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \cos k X \in ℝ$
671	664 670	sylan2	$⊢ (φ \land k \in ℕ) \to A (k) \cos k X \in ℝ$
672	664 668	sylan2	$⊢ (φ \land k \in ℕ) \to k X \in ℝ$
673	672	resincld	$⊢ (φ \land k \in ℕ) \to \sin k X \in ℝ$
674	592 673	remulcld	$⊢ (φ \land k \in ℕ) \to B (k) \sin k X \in ℝ$
675	671 674	readdcld	$⊢ (φ \land k \in ℕ) \to A (k) \cos k X + B (k) \sin k X \in ℝ$
676	663 662 675	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A (k) \cos k X + B (k) \sin k X \in ℝ$
677	651 660 662 676	fvmptd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X) (k) = A (k) \cos k X + B (k) \sin k X$
678	363 39	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
679	676	recnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A (k) \cos k X + B (k) \sin k X \in ℂ$
680	677 678 679	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (n)$
681	650 680	chvarvv	$⊢ (φ \land l \in ℕ) \to \sum_{k = 1}^{l} (A (k) \cos k X + B (k) \sin k X) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (l)$
682	645 681	eqtrd	$⊢ (φ \land l \in ℕ) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) (l) = seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) (l)$
683	39 558 623 40 682	climeq	$⊢ φ \to ((n \in ℕ ⟼ \sum_{k = 1}^{n} (A (k) \cos k X + B (k) \sin k X)) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \leftrightarrow seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})))$
684	621 683	mpbid	$⊢ φ \to seq 1 (+ (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$
685	38 684	eqbrtrd	$⊢ φ \to seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2}))$
686		eqidd	$⊢ (φ \land n \in ℕ) \to (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X) = (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X)$
687		fveq2	$⊢ j = n \to A (j) = A (n)$
688		oveq1	$⊢ j = n \to j X = n X$
689	688	fveq2d	$⊢ j = n \to \cos j X = \cos n X$
690	687 689	oveq12d	$⊢ j = n \to A (j) \cos j X = A (n) \cos n X$
691		fveq2	$⊢ j = n \to B (j) = B (n)$
692	688	fveq2d	$⊢ j = n \to \sin j X = \sin n X$
693	691 692	oveq12d	$⊢ j = n \to B (j) \sin j X = B (n) \sin n X$
694	690 693	oveq12d	$⊢ j = n \to A (j) \cos j X + B (j) \sin j X = A (n) \cos n X + B (n) \sin n X$
695	694	adantl	$⊢ ((φ \land n \in ℕ) \land j = n) \to A (j) \cos j X + B (j) \sin j X = A (n) \cos n X + B (n) \sin n X$
696	686 695 363 596	fvmptd	$⊢ (φ \land n \in ℕ) \to (j \in ℕ ⟼ A (j) \cos j X + B (j) \sin j X) (n) = A (n) \cos n X + B (n) \sin n X$
697	596	recnd	$⊢ (φ \land n \in ℕ) \to A (n) \cos n X + B (n) \sin n X \in ℂ$
698	39 40 696 697 684	isumclim	$⊢ φ \to \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = (\frac{L + R}{2}) - (\frac{A (0)}{2})$
699	698	oveq2d	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = (\frac{A (0)}{2}) + (\frac{L + R}{2}) - (\frac{A (0)}{2})$
700	503 505	addcld	$⊢ φ \to L + R \in ℂ$
701	700	halfcld	$⊢ φ \to \frac{L + R}{2} \in ℂ$
702	556 701	pncan3d	$⊢ φ \to (\frac{A (0)}{2}) + (\frac{L + R}{2}) - (\frac{A (0)}{2}) = \frac{L + R}{2}$
703	699 702	eqtrd	$⊢ φ \to (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2}$
704	685 703	jca	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2})$

Metamath Proof Explorer

Theorem fourierdlem112

Proof