fourierdlem84

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

	Ref	Expression
Hypotheses	fourierdlem84.1	\|- ( ph -> A e. RR )
	fourierdlem84.2	\|- ( ph -> B e. RR )
	fourierdlem84.f	\|- ( ph -> F : RR --> RR )
	fourierdlem84.xre	\|- ( ph -> X e. RR )
	fourierdlem84.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( A + X ) /\ ( p ` m ) = ( B + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem84.m	\|- ( ph -> M e. NN )
	fourierdlem84.v	\|- ( ph -> V e. ( P ` M ) )
	fourierdlem84.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem84.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
	fourierdlem84.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
	fourierdlem84.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
	fourierdlem84.o	\|- O = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem84.d	\|- ( ph -> D e. ( RR -cn-> RR ) )
	fourierdlem84.g	\|- G = ( s e. ( A [,] B ) \|-> ( ( F ` ( X + s ) ) x. ( D ` s ) ) )
Assertion	fourierdlem84	\|- ( ph -> G e. L^1 )

Proof

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

Metamath Proof Explorer

Theorem fourierdlem84

Proof