fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem95.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem95.xre	$⊢ φ \to X \in ℝ$
	fourierdlem95.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem95.m	$⊢ φ \to M \in ℕ$
	fourierdlem95.v	$⊢ φ \to V \in P (M)$
	fourierdlem95.x	$⊢ φ \to X \in ran V$
	fourierdlem95.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem95.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem95.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
	fourierdlem95.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem95.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem95.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem95.s	$⊢ S = (s \in [- π, π] ⟼ \sin (n + (\frac{1}{2})) s)$
	fourierdlem95.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
	fourierdlem95.i	$⊢ I = ℝ D F$
	fourierdlem95.ifn	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ$
	fourierdlem95.b	$⊢ φ \to B \in (({I ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem95.c	$⊢ φ \to C \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem95.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem95.w	$⊢ φ \to W \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem95.admvol	$⊢ φ \to A \in dom vol$
	fourierdlem95.ass	$⊢ φ \to A \subseteq [- π, π] ∖ \{0\}$
	fourierlemenplusacver2eqitgdirker.e	$⊢ E = (n \in ℕ ⟼ \frac{\int_{A} G (s) d s}{π})$
	fourierdlem95.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})})))$
	fourierdlem95.o	$⊢ φ \to O \in ℝ$
	fourierdlem95.ifeqo	$⊢ (φ \land s \in A) \to if (0 < s, Y, W) = O$
	fourierdlem95.itgdirker	$⊢ (φ \land n \in ℕ) \to \int_{A} D (n) (s) d s = \frac{1}{2}$
Assertion	fourierdlem95	$⊢ (φ \land n \in ℕ) \to E (n) + (\frac{O}{2}) = \int_{A} F (X + s) D (n) (s) d s$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem95.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem95.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem95.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
4		fourierdlem95.m	$⊢ φ \to M \in ℕ$
5		fourierdlem95.v	$⊢ φ \to V \in P (M)$
6		fourierdlem95.x	$⊢ φ \to X \in ran V$
7		fourierdlem95.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem95.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
9		fourierdlem95.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
10		fourierdlem95.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
11		fourierdlem95.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
12		fourierdlem95.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
13		fourierdlem95.s	$⊢ S = (s \in [- π, π] ⟼ \sin (n + (\frac{1}{2})) s)$
14		fourierdlem95.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
15		fourierdlem95.i	$⊢ I = ℝ D F$
16		fourierdlem95.ifn	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ$
17		fourierdlem95.b	$⊢ φ \to B \in (({I ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
18		fourierdlem95.c	$⊢ φ \to C \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
19		fourierdlem95.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
20		fourierdlem95.w	$⊢ φ \to W \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
21		fourierdlem95.admvol	$⊢ φ \to A \in dom vol$
22		fourierdlem95.ass	$⊢ φ \to A \subseteq [- π, π] ∖ \{0\}$
23		fourierlemenplusacver2eqitgdirker.e	$⊢ E = (n \in ℕ ⟼ \frac{\int_{A} G (s) d s}{π})$
24		fourierdlem95.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})})))$
25		fourierdlem95.o	$⊢ φ \to O \in ℝ$
26		fourierdlem95.ifeqo	$⊢ (φ \land s \in A) \to if (0 < s, Y, W) = O$
27		fourierdlem95.itgdirker	$⊢ (φ \land n \in ℕ) \to \int_{A} D (n) (s) d s = \frac{1}{2}$
28		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
29	22	difss2d	$⊢ φ \to A \subseteq [- π, π]$
30	29	adantr	$⊢ (φ \land n \in ℕ) \to A \subseteq [- π, π]$
31	30	sselda	$⊢ ((φ \land n \in ℕ) \land s \in A) \to s \in [- π, π]$
32	1	adantr	$⊢ (φ \land n \in ℕ) \to F : ℝ ⟶ ℝ$
33	2	adantr	$⊢ (φ \land n \in ℕ) \to X \in ℝ$
34		ioossre	$⊢ (X, +∞) \subseteq ℝ$
35	34	a1i	$⊢ φ \to (X, +∞) \subseteq ℝ$
36	1 35	fssresd	$⊢ φ \to ({F ↾}_{(X, +∞)}) : (X, +∞) ⟶ ℝ$
37		ioosscn	$⊢ (X, +∞) \subseteq ℂ$
38	37	a1i	$⊢ φ \to (X, +∞) \subseteq ℂ$
39		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
40		pnfxr	$⊢ +∞ \in ℝ^{*}$
41	40	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
42	2	ltpnfd	$⊢ φ \to X < +∞$
43	39 41 2 42	lptioo1cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞))$
44	36 38 43 19	limcrecl	$⊢ φ \to Y \in ℝ$
45	44	adantr	$⊢ (φ \land n \in ℕ) \to Y \in ℝ$
46		ioossre	$⊢ (−∞, X) \subseteq ℝ$
47	46	a1i	$⊢ φ \to (−∞, X) \subseteq ℝ$
48	1 47	fssresd	$⊢ φ \to ({F ↾}_{(−∞, X)}) : (−∞, X) ⟶ ℝ$
49		ioosscn	$⊢ (−∞, X) \subseteq ℂ$
50	49	a1i	$⊢ φ \to (−∞, X) \subseteq ℂ$
51		mnfxr	$⊢ −∞ \in ℝ^{*}$
52	51	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
53	2	mnfltd	$⊢ φ \to −∞ < X$
54	39 52 2 53	lptioo2cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((−∞, X))$
55	48 50 54 20	limcrecl	$⊢ φ \to W \in ℝ$
56	55	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ$
57	28	nnred	$⊢ (φ \land n \in ℕ) \to n \in ℝ$
58	32 33 45 56 10 11 12 57 13 14	fourierdlem67	$⊢ (φ \land n \in ℕ) \to G : [- π, π] ⟶ ℝ$
59	58	ffvelcdmda	$⊢ ((φ \land n \in ℕ) \land s \in [- π, π]) \to G (s) \in ℝ$
60	31 59	syldan	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) \in ℝ$
61	21	adantr	$⊢ (φ \land n \in ℕ) \to A \in dom vol$
62	58	feqmptd	$⊢ (φ \land n \in ℕ) \to G = (s \in [- π, π] ⟼ G (s))$
63	6	adantr	$⊢ (φ \land n \in ℕ) \to X \in ran V$
64	19	adantr	$⊢ (φ \land n \in ℕ) \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
65	20	adantr	$⊢ (φ \land n \in ℕ) \to W \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
66	4	adantr	$⊢ (φ \land n \in ℕ) \to M \in ℕ$
67	5	adantr	$⊢ (φ \land n \in ℕ) \to V \in P (M)$
68	7	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
69	8	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
70	9	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
71		fveq2	$⊢ j = i \to V (j) = V (i)$
72	71	oveq1d	$⊢ j = i \to V (j) - X = V (i) - X$
73	72	cbvmptv	$⊢ (j \in (0 \dots M) ⟼ V (j) - X) = (i \in (0 \dots M) ⟼ V (i) - X)$
74		eqid	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
75	16	adantlr	$⊢ ((φ \land n \in ℕ) \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ$
76	17	adantr	$⊢ (φ \land n \in ℕ) \to B \in (({I ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
77	18	adantr	$⊢ (φ \land n \in ℕ) \to C \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
78	3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77	fourierdlem88	$⊢ (φ \land n \in ℕ) \to G \in 𝐿^{1}$
79	62 78	eqeltrrd	$⊢ (φ \land n \in ℕ) \to (s \in [- π, π] ⟼ G (s)) \in 𝐿^{1}$
80	30 61 59 79	iblss	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ G (s)) \in 𝐿^{1}$
81	60 80	itgrecl	$⊢ (φ \land n \in ℕ) \to \int_{A} G (s) d s \in ℝ$
82		pire	$⊢ π \in ℝ$
83	82	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
84		pipos	$⊢ 0 < π$
85	82 84	gt0ne0ii	$⊢ π \neq 0$
86	85	a1i	$⊢ (φ \land n \in ℕ) \to π \neq 0$
87	81 83 86	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{\int_{A} G (s) d s}{π} \in ℝ$
88	23	fvmpt2	$⊢ (n \in ℕ \land \frac{\int_{A} G (s) d s}{π} \in ℝ) \to E (n) = \frac{\int_{A} G (s) d s}{π}$
89	28 87 88	syl2anc	$⊢ (φ \land n \in ℕ) \to E (n) = \frac{\int_{A} G (s) d s}{π}$
90	25	recnd	$⊢ φ \to O \in ℂ$
91		2cnd	$⊢ φ \to 2 \in ℂ$
92		2ne0	$⊢ 2 \neq 0$
93	92	a1i	$⊢ φ \to 2 \neq 0$
94	90 91 93	divrecd	$⊢ φ \to \frac{O}{2} = O (\frac{1}{2})$
95	94	adantr	$⊢ (φ \land n \in ℕ) \to \frac{O}{2} = O (\frac{1}{2})$
96	27	eqcomd	$⊢ (φ \land n \in ℕ) \to \frac{1}{2} = \int_{A} D (n) (s) d s$
97	96	oveq2d	$⊢ (φ \land n \in ℕ) \to O (\frac{1}{2}) = O \int_{A} D (n) (s) d s$
98	95 97	eqtrd	$⊢ (φ \land n \in ℕ) \to \frac{O}{2} = O \int_{A} D (n) (s) d s$
99	89 98	oveq12d	$⊢ (φ \land n \in ℕ) \to E (n) + (\frac{O}{2}) = (\frac{\int_{A} G (s) d s}{π}) + O \int_{A} D (n) (s) d s$
100	22	sselda	$⊢ (φ \land s \in A) \to s \in ([- π, π] ∖ \{0\})$
101	100	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to s \in ([- π, π] ∖ \{0\})$
102		eqid	$⊢ [- π, π] ∖ \{0\} = [- π, π] ∖ \{0\}$
103	1 2 44 55 24 10 11 12 13 14 102	fourierdlem66	$⊢ ((φ \land n \in ℕ) \land s \in ([- π, π] ∖ \{0\})) \to G (s) = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
104	101 103	syldan	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) = π (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
105	104	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{A} G (s) d s = \int_{A} π (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s$
106	105	oveq1d	$⊢ (φ \land n \in ℕ) \to \frac{\int_{A} G (s) d s}{π} = \frac{\int_{A} π (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s}{π}$
107	83	recnd	$⊢ (φ \land n \in ℕ) \to π \in ℂ$
108	1	adantr	$⊢ (φ \land s \in A) \to F : ℝ ⟶ ℝ$
109	2	adantr	$⊢ (φ \land s \in A) \to X \in ℝ$
110		difss	$⊢ [- π, π] ∖ \{0\} \subseteq [- π, π]$
111	82	renegcli	$⊢ - π \in ℝ$
112		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
113	111 82 112	mp2an	$⊢ [- π, π] \subseteq ℝ$
114	110 113	sstri	$⊢ [- π, π] ∖ \{0\} \subseteq ℝ$
115	114 100	sselid	$⊢ (φ \land s \in A) \to s \in ℝ$
116	109 115	readdcld	$⊢ (φ \land s \in A) \to X + s \in ℝ$
117	108 116	ffvelcdmd	$⊢ (φ \land s \in A) \to F (X + s) \in ℝ$
118	44 55	ifcld	$⊢ φ \to if (0 < s, Y, W) \in ℝ$
119	118	adantr	$⊢ (φ \land s \in A) \to if (0 < s, Y, W) \in ℝ$
120	117 119	resubcld	$⊢ (φ \land s \in A) \to F (X + s) - if (0 < s, Y, W) \in ℝ$
121	120	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to F (X + s) - if (0 < s, Y, W) \in ℝ$
122	28	adantr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to n \in ℕ$
123	115	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to s \in ℝ$
124	24	dirkerre	$⊢ (n \in ℕ \land s \in ℝ) \to D (n) (s) \in ℝ$
125	122 123 124	syl2anc	$⊢ ((φ \land n \in ℕ) \land s \in A) \to D (n) (s) \in ℝ$
126	121 125	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) \in ℝ$
127	104	eqcomd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to π (F (X + s) - if (0 < s, Y, W)) D (n) (s) = G (s)$
128	127	oveq1d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \frac{π (F (X + s) - if (0 < s, Y, W)) D (n) (s)}{π} = \frac{G (s)}{π}$
129		picn	$⊢ π \in ℂ$
130	129	a1i	$⊢ ((φ \land n \in ℕ) \land s \in A) \to π \in ℂ$
131	126	recnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) \in ℂ$
132	85	a1i	$⊢ ((φ \land n \in ℕ) \land s \in A) \to π \neq 0$
133	130 131 130 132	div23d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \frac{π (F (X + s) - if (0 < s, Y, W)) D (n) (s)}{π} = (\frac{π}{π}) (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
134	60	recnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to G (s) \in ℂ$
135	134 130 132	divrec2d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \frac{G (s)}{π} = (\frac{1}{π}) G (s)$
136	128 133 135	3eqtr3rd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (\frac{1}{π}) G (s) = (\frac{π}{π}) (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
137	129 85	dividi	$⊢ \frac{π}{π} = 1$
138	137	a1i	$⊢ ((φ \land n \in ℕ) \land s \in A) \to \frac{π}{π} = 1$
139	138	oveq1d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (\frac{π}{π}) (F (X + s) - if (0 < s, Y, W)) D (n) (s) = 1 (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
140	131	mullidd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to 1 (F (X + s) - if (0 < s, Y, W)) D (n) (s) = (F (X + s) - if (0 < s, Y, W)) D (n) (s)$
141	136 139 140	3eqtrrd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) = (\frac{1}{π}) G (s)$
142	141	mpteq2dva	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ (F (X + s) - if (0 < s, Y, W)) D (n) (s)) = (s \in A ⟼ (\frac{1}{π}) G (s))$
143	107 86	reccld	$⊢ (φ \land n \in ℕ) \to \frac{1}{π} \in ℂ$
144	143 60 80	iblmulc2	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ (\frac{1}{π}) G (s)) \in 𝐿^{1}$
145	142 144	eqeltrd	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ (F (X + s) - if (0 < s, Y, W)) D (n) (s)) \in 𝐿^{1}$
146	107 126 145	itgmulc2	$⊢ (φ \land n \in ℕ) \to π \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s = \int_{A} π (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s$
147	146	eqcomd	$⊢ (φ \land n \in ℕ) \to \int_{A} π (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s = π \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s$
148	147	oveq1d	$⊢ (φ \land n \in ℕ) \to \frac{\int_{A} π (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s}{π} = \frac{π \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s}{π}$
149	126 145	itgcl	$⊢ (φ \land n \in ℕ) \to \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s \in ℂ$
150	149 107 86	divcan3d	$⊢ (φ \land n \in ℕ) \to \frac{π \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s}{π} = \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s$
151	106 148 150	3eqtrd	$⊢ (φ \land n \in ℕ) \to \frac{\int_{A} G (s) d s}{π} = \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s$
152	90	adantr	$⊢ (φ \land n \in ℕ) \to O \in ℂ$
153	113	sseli	$⊢ s \in [- π, π] \to s \in ℝ$
154	153 124	sylan2	$⊢ (n \in ℕ \land s \in [- π, π]) \to D (n) (s) \in ℝ$
155	154	adantll	$⊢ ((φ \land n \in ℕ) \land s \in [- π, π]) \to D (n) (s) \in ℝ$
156	111	a1i	$⊢ (φ \land n \in ℕ) \to - π \in ℝ$
157		ax-resscn	$⊢ ℝ \subseteq ℂ$
158	157	a1i	$⊢ n \in ℕ \to ℝ \subseteq ℂ$
159		ssid	$⊢ ℂ \subseteq ℂ$
160		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
161	158 159 160	sylancl	$⊢ n \in ℕ \to [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
162		eqid	$⊢ (s \in ℝ ⟼ D (n) (s)) = (s \in ℝ ⟼ D (n) (s))$
163	24	dirkerf	$⊢ n \in ℕ \to D (n) : ℝ ⟶ ℝ$
164	163	feqmptd	$⊢ n \in ℕ \to D (n) = (s \in ℝ ⟼ D (n) (s))$
165	24	dirkercncf	$⊢ n \in ℕ \to D (n) : ℝ \underset{cn}{⟶} ℝ$
166	164 165	eqeltrrd	$⊢ n \in ℕ \to (s \in ℝ ⟼ D (n) (s)) : ℝ \underset{cn}{⟶} ℝ$
167	113	a1i	$⊢ n \in ℕ \to [- π, π] \subseteq ℝ$
168		ssid	$⊢ ℝ \subseteq ℝ$
169	168	a1i	$⊢ n \in ℕ \to ℝ \subseteq ℝ$
170	162 166 167 169 154	cncfmptssg	$⊢ n \in ℕ \to (s \in [- π, π] ⟼ D (n) (s)) : [- π, π] \underset{cn}{⟶} ℝ$
171	161 170	sseldd	$⊢ n \in ℕ \to (s \in [- π, π] ⟼ D (n) (s)) : [- π, π] \underset{cn}{⟶} ℂ$
172	171	adantl	$⊢ (φ \land n \in ℕ) \to (s \in [- π, π] ⟼ D (n) (s)) : [- π, π] \underset{cn}{⟶} ℂ$
173		cniccibl	$⊢ (- π \in ℝ \land π \in ℝ \land (s \in [- π, π] ⟼ D (n) (s)) : [- π, π] \underset{cn}{⟶} ℂ) \to (s \in [- π, π] ⟼ D (n) (s)) \in 𝐿^{1}$
174	156 83 172 173	syl3anc	$⊢ (φ \land n \in ℕ) \to (s \in [- π, π] ⟼ D (n) (s)) \in 𝐿^{1}$
175	30 61 155 174	iblss	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ D (n) (s)) \in 𝐿^{1}$
176	152 125 175	itgmulc2	$⊢ (φ \land n \in ℕ) \to O \int_{A} D (n) (s) d s = \int_{A} O D (n) (s) d s$
177	151 176	oveq12d	$⊢ (φ \land n \in ℕ) \to (\frac{\int_{A} G (s) d s}{π}) + O \int_{A} D (n) (s) d s = \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s + \int_{A} O D (n) (s) d s$
178	25	ad2antrr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to O \in ℝ$
179	178 125	remulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to O D (n) (s) \in ℝ$
180	152 125 175	iblmulc2	$⊢ (φ \land n \in ℕ) \to (s \in A ⟼ O D (n) (s)) \in 𝐿^{1}$
181	126 145 179 180	itgadd	$⊢ (φ \land n \in ℕ) \to \int_{A} ((F (X + s) - if (0 < s, Y, W)) D (n) (s) + O D (n) (s)) d s = \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s + \int_{A} O D (n) (s) d s$
182	26	eqcomd	$⊢ (φ \land s \in A) \to O = if (0 < s, Y, W)$
183	182	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to O = if (0 < s, Y, W)$
184	183	oveq1d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to O D (n) (s) = if (0 < s, Y, W) D (n) (s)$
185	184	oveq2d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) + O D (n) (s) = (F (X + s) - if (0 < s, Y, W)) D (n) (s) + if (0 < s, Y, W) D (n) (s)$
186	117	recnd	$⊢ (φ \land s \in A) \to F (X + s) \in ℂ$
187	186	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to F (X + s) \in ℂ$
188	119	recnd	$⊢ (φ \land s \in A) \to if (0 < s, Y, W) \in ℂ$
189	188	adantlr	$⊢ ((φ \land n \in ℕ) \land s \in A) \to if (0 < s, Y, W) \in ℂ$
190	125	recnd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to D (n) (s) \in ℂ$
191	187 189 190	subdird	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) = F (X + s) D (n) (s) - if (0 < s, Y, W) D (n) (s)$
192	191	oveq1d	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) + if (0 < s, Y, W) D (n) (s) = F (X + s) D (n) (s) - if (0 < s, Y, W) D (n) (s) + if (0 < s, Y, W) D (n) (s)$
193	187 190	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to F (X + s) D (n) (s) \in ℂ$
194	189 190	mulcld	$⊢ ((φ \land n \in ℕ) \land s \in A) \to if (0 < s, Y, W) D (n) (s) \in ℂ$
195	193 194	npcand	$⊢ ((φ \land n \in ℕ) \land s \in A) \to F (X + s) D (n) (s) - if (0 < s, Y, W) D (n) (s) + if (0 < s, Y, W) D (n) (s) = F (X + s) D (n) (s)$
196	185 192 195	3eqtrd	$⊢ ((φ \land n \in ℕ) \land s \in A) \to (F (X + s) - if (0 < s, Y, W)) D (n) (s) + O D (n) (s) = F (X + s) D (n) (s)$
197	196	itgeq2dv	$⊢ (φ \land n \in ℕ) \to \int_{A} ((F (X + s) - if (0 < s, Y, W)) D (n) (s) + O D (n) (s)) d s = \int_{A} F (X + s) D (n) (s) d s$
198	181 197	eqtr3d	$⊢ (φ \land n \in ℕ) \to \int_{A} (F (X + s) - if (0 < s, Y, W)) D (n) (s) d s + \int_{A} O D (n) (s) d s = \int_{A} F (X + s) D (n) (s) d s$
199	99 177 198	3eqtrd	$⊢ (φ \land n \in ℕ) \to E (n) + (\frac{O}{2}) = \int_{A} F (X + s) D (n) (s) d s$

Metamath Proof Explorer

Theorem fourierdlem95

Proof