fourierdlem88

Description: Given a piecewise continuous function F , a continuous function K and a continuous function S , the function G is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem88.1	$⊢ 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))\})$
2		fourierdlem88.f	$⊢ φ \to F : ℝ ⟶ ℝ$
3		fourierdlem88.x	$⊢ φ \to X \in ran V$
4		fourierdlem88.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
5		fourierdlem88.w	$⊢ φ \to W \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
6		fourierdlem88.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
7		fourierdlem88.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
8		fourierdlem88.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
9		fourierdlem88.n	$⊢ φ \to N \in ℝ$
10		fourierdlem88.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
11		fourierdlem88.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
12		fourierdlem88.m	$⊢ φ \to M \in ℕ$
13		fourierdlem88.v	$⊢ φ \to V \in P (M)$
14		fourierdlem88.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
15		fourierdlem88.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
16		fourierdlem88.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
17		fourierdlem88.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
18		fourierdlem88.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
19		fourierdlem88.i	$⊢ I = ℝ D F$
20		fourierdlem88.ifn	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℝ$
21		fourierdlem88.c	$⊢ φ \to C \in (({I ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
22		fourierdlem88.d	$⊢ φ \to D \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
23		pire	$⊢ π \in ℝ$
24	23	a1i	$⊢ φ \to π \in ℝ$
25	24	renegcld	$⊢ φ \to - π \in ℝ$
26	1	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
27	12 26	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
28	13 27	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
29	28	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
30		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
31		frn	$⊢ V : (0 \dots M) ⟶ ℝ \to ran V \subseteq ℝ$
32	29 30 31	3syl	$⊢ φ \to ran V \subseteq ℝ$
33	32 3	sseldd	$⊢ φ \to X \in ℝ$
34	25 24 33 1 18 12 13 17	fourierdlem14	$⊢ φ \to Q \in O (M)$
35		ioossre	$⊢ (X, +∞) \subseteq ℝ$
36	35	a1i	$⊢ φ \to (X, +∞) \subseteq ℝ$
37	2 36	fssresd	$⊢ φ \to ({F ↾}_{(X, +∞)}) : (X, +∞) ⟶ ℝ$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39	36 38	sstrdi	$⊢ φ \to (X, +∞) \subseteq ℂ$
40		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
41		pnfxr	$⊢ +∞ \in ℝ^{*}$
42	41	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
43	33	ltpnfd	$⊢ φ \to X < +∞$
44	40 42 33 43	lptioo1cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞))$
45	37 39 44 4	limcrecl	$⊢ φ \to Y \in ℝ$
46		ioossre	$⊢ (−∞, X) \subseteq ℝ$
47	46	a1i	$⊢ φ \to (−∞, X) \subseteq ℝ$
48	2 47	fssresd	$⊢ φ \to ({F ↾}_{(−∞, X)}) : (−∞, X) ⟶ ℝ$
49	47 38	sstrdi	$⊢ φ \to (−∞, X) \subseteq ℂ$
50		mnfxr	$⊢ −∞ \in ℝ^{*}$
51	50	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
52	33	mnfltd	$⊢ φ \to −∞ < X$
53	40 51 33 52	lptioo2cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((−∞, X))$
54	48 49 53 5	limcrecl	$⊢ φ \to W \in ℝ$
55	2 33 45 54 6 7 8	fourierdlem55	$⊢ φ \to U : [- π, π] ⟶ ℝ$
56	55	ffvelrnda	$⊢ (φ \land s \in [- π, π]) \to U (s) \in ℝ$
57	10	fourierdlem5	$⊢ N \in ℝ \to S : [- π, π] ⟶ ℝ$
58	9 57	syl	$⊢ φ \to S : [- π, π] ⟶ ℝ$
59	58	ffvelrnda	$⊢ (φ \land s \in [- π, π]) \to S (s) \in ℝ$
60	56 59	remulcld	$⊢ (φ \land s \in [- π, π]) \to U (s) S (s) \in ℝ$
61	60	recnd	$⊢ (φ \land s \in [- π, π]) \to U (s) S (s) \in ℂ$
62	61 11	fmptd	$⊢ φ \to G : [- π, π] ⟶ ℂ$
63		ssid	$⊢ ℂ \subseteq ℂ$
64		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to (Q (i), Q (i + 1)) \underset{cn}{⟶} ℝ \subseteq (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
65	38 63 64	mp2an	$⊢ (Q (i), Q (i + 1)) \underset{cn}{⟶} ℝ \subseteq (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
66	2	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℝ$
67	18 12 34	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
68	67	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
69		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
70	69	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
71	68 70	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [- π, π]$
72		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
73	72	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
74	68 73	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in [- π, π]$
75	33	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
76	1 12 13 3	fourierdlem12	$⊢ (φ \land i \in (0 ..^M)) \to \neg X \in (V (i), V (i + 1))$
77	75	recnd	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
78	77	addid2d	$⊢ (φ \land i \in (0 ..^M)) \to 0 + X = X$
79	23	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ$
80	79	renegcld	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ$
81	80 75	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to - π + X \in ℝ$
82	79 75	readdcld	$⊢ (φ \land i \in (0 ..^M)) \to π + X \in ℝ$
83	81 82	iccssred	$⊢ (φ \land i \in (0 ..^M)) \to [- π + X, π + X] \subseteq ℝ$
84	1 12 13	fourierdlem15	$⊢ φ \to V : (0 \dots M) ⟶ [- π + X, π + X]$
85	84	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ [- π + X, π + X]$
86	85 70	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in [- π + X, π + X]$
87	83 86	sseldd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
88	87 75	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X \in ℝ$
89	17	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
90	70 88 89	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = V (i) - X$
91	90	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + X = V (i) - X + X$
92	87	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℂ$
93	92 77	npcand	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X + X = V (i)$
94	91 93	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + X = V (i)$
95		fveq2	$⊢ i = j \to V (i) = V (j)$
96	95	oveq1d	$⊢ i = j \to V (i) - X = V (j) - X$
97	96	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ V (i) - X) = (j \in (0 \dots M) ⟼ V (j) - X)$
98	17 97	eqtri	$⊢ Q = (j \in (0 \dots M) ⟼ V (j) - X)$
99	98	a1i	$⊢ (φ \land i \in (0 ..^M)) \to Q = (j \in (0 \dots M) ⟼ V (j) - X)$
100		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to j = i + 1$
101	100	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) = V (i + 1)$
102	101	oveq1d	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) - X = V (i + 1) - X$
103	85 73	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in [- π + X, π + X]$
104	83 103	sseldd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
105	104 75	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X \in ℝ$
106	99 102 73 105	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = V (i + 1) - X$
107	106	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + X = V (i + 1) - X + X$
108	104	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℂ$
109	108 77	npcand	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X + X = V (i + 1)$
110	107 109	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) + X = V (i + 1)$
111	94 110	oveq12d	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) + X, Q (i + 1) + X) = (V (i), V (i + 1))$
112	78 111	eleq12d	$⊢ (φ \land i \in (0 ..^M)) \to (0 + X \in (Q (i) + X, Q (i + 1) + X) \leftrightarrow X \in (V (i), V (i + 1)))$
113	76 112	mtbird	$⊢ (φ \land i \in (0 ..^M)) \to \neg 0 + X \in (Q (i) + X, Q (i + 1) + X)$
114		0red	$⊢ (φ \land i \in (0 ..^M)) \to 0 \in ℝ$
115	90 88	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
116	106 105	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
117	114 115 116 75	eliooshift	$⊢ (φ \land i \in (0 ..^M)) \to (0 \in (Q (i), Q (i + 1)) \leftrightarrow 0 + X \in (Q (i) + X, Q (i + 1) + X))$
118	113 117	mtbird	$⊢ (φ \land i \in (0 ..^M)) \to \neg 0 \in (Q (i), Q (i + 1))$
119	111	reseq2d	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i) + X, Q (i + 1) + X)} = {F ↾}_{(V (i), V (i + 1))}$
120	111	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i) + X, Q (i + 1) + X) \underset{cn}{⟶} ℂ = (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
121	14 119 120	3eltr4d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i) + X, Q (i + 1) + X)}) : (Q (i) + X, Q (i + 1) + X) \underset{cn}{⟶} ℂ$
122	45	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Y \in ℝ$
123	54	adantr	$⊢ (φ \land i \in (0 ..^M)) \to W \in ℝ$
124	9	adantr	$⊢ (φ \land i \in (0 ..^M)) \to N \in ℝ$
125	66 71 74 75 118 121 122 123 6 7 8 124 10 11	fourierdlem78	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℝ$
126	65 125	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
127		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ U (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s))$
128		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ S (s)) = (s \in (Q (i), Q (i + 1)) ⟼ S (s))$
129		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s))$
130	23	renegcli	$⊢ - π \in ℝ$
131	130	rexri	$⊢ - π \in ℝ^{*}$
132	131	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to - π \in ℝ^{*}$
133	23	rexri	$⊢ π \in ℝ^{*}$
134	133	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to π \in ℝ^{*}$
135	68	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [- π, π]$
136		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
137	132 134 135 136	fourierdlem8	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
138		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
139	138	sseli	$⊢ s \in (Q (i), Q (i + 1)) \to s \in [Q (i), Q (i + 1)]$
140	139	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in [Q (i), Q (i + 1)]$
141	137 140	sseldd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in [- π, π]$
142	2 33 45 54 6	fourierdlem9	$⊢ φ \to H : [- π, π] ⟶ ℝ$
143	142	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H : [- π, π] ⟶ ℝ$
144	143 141	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) \in ℝ$
145	7	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$
146	145	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K : [- π, π] ⟶ ℝ$
147	146 141	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K (s) \in ℝ$
148	144 147	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) K (s) \in ℝ$
149	8	fvmpt2	$⊢ (s \in [- π, π] \land H (s) K (s) \in ℝ) \to U (s) = H (s) K (s)$
150	141 148 149	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) = H (s) K (s)$
151	150 148	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) \in ℝ$
152	151	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) \in ℂ$
153	9 10	fourierdlem18	$⊢ φ \to S : [- π, π] \underset{cn}{⟶} ℝ$
154		cncff	$⊢ S : [- π, π] \underset{cn}{⟶} ℝ \to S : [- π, π] ⟶ ℝ$
155	153 154	syl	$⊢ φ \to S : [- π, π] ⟶ ℝ$
156	155	adantr	$⊢ (φ \land i \in (0 ..^M)) \to S : [- π, π] ⟶ ℝ$
157	156	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S : [- π, π] ⟶ ℝ$
158	157 141	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S (s) \in ℝ$
159	158	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S (s) \in ℂ$
160		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ H (s)) = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
161		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ K (s)) = (s \in (Q (i), Q (i + 1)) ⟼ K (s))$
162		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) = (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s))$
163	144	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) \in ℂ$
164	147	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K (s) \in ℂ$
165	38	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
166	20 165	fssd	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
167		eqid	$⊢ if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) = if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)})$
168	33 1 2 3 4 54 6 12 13 15 17 18 19 166 22 167	fourierdlem75	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
169	142	adantr	$⊢ (φ \land i \in (0 ..^M)) \to H : [- π, π] ⟶ ℝ$
170	131	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
171	133	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
172		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
173	170 171 68 172	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
174	138 173	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
175	169 174	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
176	175	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i)$
177	168 176	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i))$
178		limcresi	$⊢ K {lim}_{ℂ} Q (i) \subseteq ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
179	7	fourierdlem62	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ$
180	179	a1i	$⊢ (φ \land i \in (0 ..^M)) \to K : [- π, π] \underset{cn}{⟶} ℝ$
181	180 71	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in (K {lim}_{ℂ} Q (i))$
182	178 181	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in (({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
183	145	a1i	$⊢ (φ \land i \in (0 ..^M)) \to K : [- π, π] ⟶ ℝ$
184	183 174	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {K ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ K (s))$
185	184	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i)$
186	182 185	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i))$
187	160 161 162 163 164 177 186	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i))$
188	150	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) K (s) = U (s)$
189	188	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s))$
190	189	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i)$
191	187 190	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i))$
192		limcresi	$⊢ S {lim}_{ℂ} Q (i) \subseteq ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
193	153	adantr	$⊢ (φ \land i \in (0 ..^M)) \to S : [- π, π] \underset{cn}{⟶} ℝ$
194	193 71	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in (S {lim}_{ℂ} Q (i))$
195	192 194	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in (({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
196	156 174	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {S ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ S (s))$
197	196	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i)$
198	195 197	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i))$
199	127 128 129 152 159 191 198	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) S (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i))$
200	60 11	fmptd	$⊢ φ \to G : [- π, π] ⟶ ℝ$
201	200	adantr	$⊢ (φ \land i \in (0 ..^M)) \to G : [- π, π] ⟶ ℝ$
202	201 174	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ G (s))$
203	151 158	remulcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) S (s) \in ℝ$
204	11	fvmpt2	$⊢ (s \in [- π, π] \land U (s) S (s) \in ℝ) \to G (s) = U (s) S (s)$
205	141 203 204	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to G (s) = U (s) S (s)$
206	205	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ G (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s))$
207	202 206	eqtr2d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) = {G ↾}_{(Q (i), Q (i + 1))}$
208	207	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
209	199 208	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, D, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) S (Q (i)) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
210		eqid	$⊢ if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) = if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)})$
211	33 1 2 3 45 5 6 12 13 16 17 18 19 20 21 210	fourierdlem74	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
212	175	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i + 1)$
213	211 212	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i + 1))$
214		limcresi	$⊢ K {lim}_{ℂ} Q (i + 1) \subseteq ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
215	180 74	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i + 1)) \in (K {lim}_{ℂ} Q (i + 1))$
216	214 215	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i + 1)) \in (({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
217	184	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i + 1)$
218	216 217	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i + 1))$
219	160 161 162 163 164 213 218	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) K (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i + 1))$
220	189	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i + 1) = (s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i + 1)$
221	219 220	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) K (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i + 1))$
222		limcresi	$⊢ S {lim}_{ℂ} Q (i + 1) \subseteq ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
223	193 74	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i + 1)) \in (S {lim}_{ℂ} Q (i + 1))$
224	222 223	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i + 1)) \in (({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
225	196	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i + 1)$
226	224 225	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i + 1))$
227	127 128 129 152 159 221 226	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) K (Q (i + 1)) S (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i + 1))$
228	207	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i + 1) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
229	227 228	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i + 1) = X, C, \frac{L - if (V (i + 1) < X, W, Y)}{Q (i + 1)}) K (Q (i + 1)) S (Q (i + 1)) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
230	18 12 34 62 126 209 229	fourierdlem69	$⊢ φ \to G \in 𝐿^{1}$

Metamath Proof Explorer

Theorem fourierdlem88

Proof