fourierdlem84

Description: If F is piecewise coninuous and D is continuous, then G is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem84.1	$⊢ φ \to A \in ℝ$
	fourierdlem84.2	$⊢ φ \to B \in ℝ$
	fourierdlem84.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem84.xre	$⊢ φ \to X \in ℝ$
	fourierdlem84.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + X \land p (m) = B + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem84.m	$⊢ φ \to M \in ℕ$
	fourierdlem84.v	$⊢ φ \to V \in P (M)$
	fourierdlem84.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem84.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem84.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
	fourierdlem84.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem84.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem84.d	$⊢ φ \to D : ℝ \underset{cn}{⟶} ℝ$
	fourierdlem84.g	$⊢ G = (s \in [A, B] ⟼ F (X + s) D (s))$
Assertion	fourierdlem84	$⊢ φ \to G \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem84.1	$⊢ φ \to A \in ℝ$
2		fourierdlem84.2	$⊢ φ \to B \in ℝ$
3		fourierdlem84.f	$⊢ φ \to F : ℝ ⟶ ℝ$
4		fourierdlem84.xre	$⊢ φ \to X \in ℝ$
5		fourierdlem84.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A + X \land p (m) = B + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
6		fourierdlem84.m	$⊢ φ \to M \in ℕ$
7		fourierdlem84.v	$⊢ φ \to V \in P (M)$
8		fourierdlem84.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
9		fourierdlem84.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
10		fourierdlem84.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
11		fourierdlem84.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
12		fourierdlem84.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
13		fourierdlem84.d	$⊢ φ \to D : ℝ \underset{cn}{⟶} ℝ$
14		fourierdlem84.g	$⊢ G = (s \in [A, B] ⟼ F (X + s) D (s))$
15	1 2 4 5 12 6 7 11	fourierdlem14	$⊢ φ \to Q \in O (M)$
16	3	adantr	$⊢ (φ \land s \in [A, B]) \to F : ℝ ⟶ ℝ$
17	4	adantr	$⊢ (φ \land s \in [A, B]) \to X \in ℝ$
18	1	adantr	$⊢ (φ \land s \in [A, B]) \to A \in ℝ$
19	2	adantr	$⊢ (φ \land s \in [A, B]) \to B \in ℝ$
20		simpr	$⊢ (φ \land s \in [A, B]) \to s \in [A, B]$
21		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land s \in [A, B]) \to s \in ℝ$
22	18 19 20 21	syl3anc	$⊢ (φ \land s \in [A, B]) \to s \in ℝ$
23	17 22	readdcld	$⊢ (φ \land s \in [A, B]) \to X + s \in ℝ$
24	16 23	ffvelcdmd	$⊢ (φ \land s \in [A, B]) \to F (X + s) \in ℝ$
25		cncff	$⊢ D : ℝ \underset{cn}{⟶} ℝ \to D : ℝ ⟶ ℝ$
26	13 25	syl	$⊢ φ \to D : ℝ ⟶ ℝ$
27	26	adantr	$⊢ (φ \land s \in [A, B]) \to D : ℝ ⟶ ℝ$
28	27 22	ffvelcdmd	$⊢ (φ \land s \in [A, B]) \to D (s) \in ℝ$
29	24 28	remulcld	$⊢ (φ \land s \in [A, B]) \to F (X + s) D (s) \in ℝ$
30	29	recnd	$⊢ (φ \land s \in [A, B]) \to F (X + s) D (s) \in ℂ$
31	30 14	fmptd	$⊢ φ \to G : [A, B] ⟶ ℂ$
32	14	a1i	$⊢ (φ \land i \in (0 ..^M)) \to G = (s \in [A, B] ⟼ F (X + s) D (s))$
33	32	reseq1d	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} = {(s \in [A, B] ⟼ F (X + s) D (s)) ↾}_{(Q (i), Q (i + 1))}$
34		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
35	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
36	35	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
37	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
38	37	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
39	12 6 15	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
40	39	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
41		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
42	36 38 40 41	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
43	34 42	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
44	43	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(s \in [A, B] ⟼ F (X + s) D (s)) ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s))$
45	33 44	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to {G ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s))$
46	1 4	readdcld	$⊢ φ \to A + X \in ℝ$
47	2 4	readdcld	$⊢ φ \to B + X \in ℝ$
48	46 47	iccssred	$⊢ φ \to [A + X, B + X] \subseteq ℝ$
49	48	adantr	$⊢ (φ \land i \in (0 ..^M)) \to [A + X, B + X] \subseteq ℝ$
50	5 6 7	fourierdlem15	$⊢ φ \to V : (0 \dots M) ⟶ [A + X, B + X]$
51	50	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ [A + X, B + X]$
52		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
53	52	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
54	51 53	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in [A + X, B + X]$
55	49 54	sseldd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
56	55	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ^{*}$
57	56	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) \in ℝ^{*}$
58		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
59	58	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
60	51 59	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in [A + X, B + X]$
61	49 60	sseldd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
62	61	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ^{*}$
63	62	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i + 1) \in ℝ^{*}$
64	4	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
65		elioore	$⊢ s \in (Q (i), Q (i + 1)) \to s \in ℝ$
66	65	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
67	64 66	readdcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s \in ℝ$
68	4	recnd	$⊢ φ \to X \in ℂ$
69	68	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℂ$
70	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
71	70	adantr	$⊢ (φ \land i \in (0 ..^M)) \to [A, B] \subseteq ℝ$
72	40 53	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [A, B]$
73	71 72	sseldd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
74	73	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℂ$
75	69 74	addcomd	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i) = Q (i) + X$
76	4	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
77	55 76	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X \in ℝ$
78	11	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
79	53 77 78	syl2anc	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) = V (i) - X$
80	79	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) + X = V (i) - X + X$
81	55	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℂ$
82	81 69	npcand	$⊢ (φ \land i \in (0 ..^M)) \to V (i) - X + X = V (i)$
83	75 80 82	3eqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to V (i) = X + Q (i)$
84	83	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) = X + Q (i)$
85	73	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ$
86	73	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
87	86	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i) \in ℝ^{*}$
88	40 71	fssd	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
89	88 59	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
90	89	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
91	90	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ^{*}$
92		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in (Q (i), Q (i + 1))$
93		ioogtlb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land s \in (Q (i), Q (i + 1))) \to Q (i) < s$
94	87 91 92 93	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i) < s$
95	85 66 64 94	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + Q (i) < X + s$
96	84 95	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to V (i) < X + s$
97	89	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ$
98		iooltub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land s \in (Q (i), Q (i + 1))) \to s < Q (i + 1)$
99	87 91 92 98	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s < Q (i + 1)$
100	66 97 64 99	ltadd2dd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s < X + Q (i + 1)$
101		fveq2	$⊢ i = j \to V (i) = V (j)$
102	101	oveq1d	$⊢ i = j \to V (i) - X = V (j) - X$
103	102	cbvmptv	$⊢ (i \in (0 \dots M) ⟼ V (i) - X) = (j \in (0 \dots M) ⟼ V (j) - X)$
104	11 103	eqtri	$⊢ Q = (j \in (0 \dots M) ⟼ V (j) - X)$
105	104	a1i	$⊢ (φ \land i \in (0 ..^M)) \to Q = (j \in (0 \dots M) ⟼ V (j) - X)$
106		fveq2	$⊢ j = i + 1 \to V (j) = V (i + 1)$
107	106	oveq1d	$⊢ j = i + 1 \to V (j) - X = V (i + 1) - X$
108	107	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land j = i + 1) \to V (j) - X = V (i + 1) - X$
109	61 76	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) - X \in ℝ$
110	105 108 59 109	fvmptd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) = V (i + 1) - X$
111	110	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) = X + V (i + 1) - X$
112	61	recnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℂ$
113	69 112	pncan3d	$⊢ (φ \land i \in (0 ..^M)) \to X + V (i + 1) - X = V (i + 1)$
114	111 113	eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to X + Q (i + 1) = V (i + 1)$
115	114	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + Q (i + 1) = V (i + 1)$
116	100 115	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s < V (i + 1)$
117	57 63 67 96 116	eliood	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to X + s \in (V (i), V (i + 1))$
118		fvres	$⊢ X + s \in (V (i), V (i + 1)) \to ({F ↾}_{(V (i), V (i + 1))}) (X + s) = F (X + s)$
119	117 118	syl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to ({F ↾}_{(V (i), V (i + 1))}) (X + s) = F (X + s)$
120	119	eqcomd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to F (X + s) = ({F ↾}_{(V (i), V (i + 1))}) (X + s)$
121	120	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) = (s \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(V (i), V (i + 1))}) (X + s))$
122		ioosscn	$⊢ (V (i), V (i + 1)) \subseteq ℂ$
123	122	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (V (i), V (i + 1)) \subseteq ℂ$
124		ioosscn	$⊢ (Q (i), Q (i + 1)) \subseteq ℂ$
125	124	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
126	123 8 125 69 117	fourierdlem23	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ ({F ↾}_{(V (i), V (i + 1))}) (X + s)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
127	121 126	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
128		eqid	$⊢ (s \in ℝ ⟼ D (s)) = (s \in ℝ ⟼ D (s))$
129		ax-resscn	$⊢ ℝ \subseteq ℂ$
130		ssid	$⊢ ℂ \subseteq ℂ$
131		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
132	129 130 131	mp2an	$⊢ ℝ \underset{cn}{⟶} ℝ \subseteq ℝ \underset{cn}{⟶} ℂ$
133	26	feqmptd	$⊢ φ \to D = (s \in ℝ ⟼ D (s))$
134	133	eqcomd	$⊢ φ \to (s \in ℝ ⟼ D (s)) = D$
135	134 13	eqeltrd	$⊢ φ \to (s \in ℝ ⟼ D (s)) : ℝ \underset{cn}{⟶} ℝ$
136	132 135	sselid	$⊢ φ \to (s \in ℝ ⟼ D (s)) : ℝ \underset{cn}{⟶} ℂ$
137	136	adantr	$⊢ (φ \land i \in (0 ..^M)) \to (s \in ℝ ⟼ D (s)) : ℝ \underset{cn}{⟶} ℂ$
138	43 71	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
139	130	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℂ \subseteq ℂ$
140	26	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D : ℝ ⟶ ℝ$
141	65	adantl	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to s \in ℝ$
142	140 141	ffvelcdmd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D (s) \in ℝ$
143	142	recnd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to D (s) \in ℂ$
144	143	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to D (s) \in ℂ$
145	128 137 138 139 144	cncfmptssg	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ D (s)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
146	127 145	mulcncf	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
147	45 146	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
148		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s))$
149		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ D (s)) = (s \in (Q (i), Q (i + 1)) ⟼ D (s))$
150		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) = (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s))$
151	3	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F : ℝ ⟶ ℝ$
152	4	adantr	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to X \in ℝ$
153	152 141	readdcld	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to X + s \in ℝ$
154	151 153	ffvelcdmd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℝ$
155	154	recnd	$⊢ (φ \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℂ$
156	155	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to F (X + s) \in ℂ$
157	3	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℝ$
158		ioossre	$⊢ (V (i), V (i + 1)) \subseteq ℝ$
159	158	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (V (i), V (i + 1)) \subseteq ℝ$
160	85 94	gtned	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \neq Q (i)$
161	83	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i) = ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i))$
162	9 161	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i)))$
163	157 76 138 148 117 159 160 162 74	fourierdlem53	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) {lim}_{ℂ} Q (i))$
164		limcresi	$⊢ (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i) \subseteq ({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
165	132 13	sselid	$⊢ φ \to D : ℝ \underset{cn}{⟶} ℂ$
166	165	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D : ℝ \underset{cn}{⟶} ℂ$
167	166 73	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in (D {lim}_{ℂ} Q (i))$
168	133	oveq1d	$⊢ φ \to D {lim}_{ℂ} Q (i) = (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i)$
169	168	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D {lim}_{ℂ} Q (i) = (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i)$
170	167 169	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in ((s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i))$
171	164 170	sselid	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in (({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
172	138	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ D (s))$
173	172	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ D (s)) {lim}_{ℂ} Q (i)$
174	171 173	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (s)) {lim}_{ℂ} Q (i))$
175	148 149 150 156 144 163 174	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to R D (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) {lim}_{ℂ} Q (i))$
176	14	reseq1i	$⊢ {G ↾}_{(Q (i), Q (i + 1))} = {(s \in [A, B] ⟼ F (X + s) D (s)) ↾}_{(Q (i), Q (i + 1))}$
177	176 44	eqtr2id	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) = {G ↾}_{(Q (i), Q (i + 1))}$
178	177	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) {lim}_{ℂ} Q (i) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
179	175 178	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R D (Q (i)) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
180	66 99	ltned	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \neq Q (i + 1)$
181	114	eqcomd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) = X + Q (i + 1)$
182	181	oveq2d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1) = ({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i + 1))$
183	10 182	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} (X + Q (i + 1)))$
184	89	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
185	157 76 138 148 117 159 180 183 184	fourierdlem53	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s)) {lim}_{ℂ} Q (i + 1))$
186		limcresi	$⊢ (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i + 1) \subseteq ({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
187	166 89	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in (D {lim}_{ℂ} Q (i + 1))$
188	133	oveq1d	$⊢ φ \to D {lim}_{ℂ} Q (i + 1) = (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i + 1)$
189	188	adantr	$⊢ (φ \land i \in (0 ..^M)) \to D {lim}_{ℂ} Q (i + 1) = (s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i + 1)$
190	187 189	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in ((s \in ℝ ⟼ D (s)) {lim}_{ℂ} Q (i + 1))$
191	186 190	sselid	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in (({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
192	172	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({(s \in ℝ ⟼ D (s)) ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (s \in (Q (i), Q (i + 1)) ⟼ D (s)) {lim}_{ℂ} Q (i + 1)$
193	191 192	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to D (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ D (s)) {lim}_{ℂ} Q (i + 1))$
194	148 149 150 156 144 185 193	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to L D (Q (i + 1)) \in ((s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) {lim}_{ℂ} Q (i + 1))$
195	177	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ F (X + s) D (s)) {lim}_{ℂ} Q (i + 1) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
196	194 195	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L D (Q (i + 1)) \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
197	12 6 15 31 147 179 196	fourierdlem69	$⊢ φ \to G \in 𝐿^{1}$

Metamath Proof Explorer

Theorem fourierdlem84

Proof