fourierdlem72

Description: The derivative of O is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem72.f	\|- ( ph -> F : RR --> RR )
	fourierdlem72.xre	\|- ( ph -> X e. RR )
	fourierdlem72.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem72.m	\|- ( ph -> M e. NN )
	fourierdlem72.v	\|- ( ph -> V e. ( P ` M ) )
	fourierdlem72.dvcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
	fourierdlem72.a	\|- ( ph -> A e. RR )
	fourierdlem72.b	\|- ( ph -> B e. RR )
	fourierdlem72.altb	\|- ( ph -> A < B )
	fourierdlem72.ab	\|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
	fourierdlem72.n0	\|- ( ph -> -. 0 e. ( A [,] B ) )
	fourierdlem72.c	\|- ( ph -> C e. RR )
	fourierdlem72.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
	fourierdlem72.u	\|- ( ph -> U e. ( 0 ..^ M ) )
	fourierdlem72.abss	\|- ( ph -> ( A (,) B ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
	fourierdlem72.h	\|- H = ( s e. ( A (,) B ) \|-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
	fourierdlem72.k	\|- K = ( s e. ( A (,) B ) \|-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
	fourierdlem72.o	\|- O = ( s e. ( A (,) B ) \|-> ( ( H ` s ) x. ( K ` s ) ) )
Assertion	fourierdlem72	\|- ( ph -> ( RR _D O ) e. ( ( A (,) B ) -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem72.f	\|- ( ph -> F : RR --> RR )
2		fourierdlem72.xre	\|- ( ph -> X e. RR )
3		fourierdlem72.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4		fourierdlem72.m	\|- ( ph -> M e. NN )
5		fourierdlem72.v	\|- ( ph -> V e. ( P ` M ) )
6		fourierdlem72.dvcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
7		fourierdlem72.a	\|- ( ph -> A e. RR )
8		fourierdlem72.b	\|- ( ph -> B e. RR )
9		fourierdlem72.altb	\|- ( ph -> A < B )
10		fourierdlem72.ab	\|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
11		fourierdlem72.n0	\|- ( ph -> -. 0 e. ( A [,] B ) )
12		fourierdlem72.c	\|- ( ph -> C e. RR )
13		fourierdlem72.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
14		fourierdlem72.u	\|- ( ph -> U e. ( 0 ..^ M ) )
15		fourierdlem72.abss	\|- ( ph -> ( A (,) B ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
16		fourierdlem72.h	\|- H = ( s e. ( A (,) B ) \|-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
17		fourierdlem72.k	\|- K = ( s e. ( A (,) B ) \|-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
18		fourierdlem72.o	\|- O = ( s e. ( A (,) B ) \|-> ( ( H ` s ) x. ( K ` s ) ) )
19		ovex	\|- ( A (,) B ) e. _V
20	19	a1i	\|- ( ph -> ( A (,) B ) e. _V )
21	1	adantr	\|- ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
22	2	adantr	\|- ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
23		elioore	\|- ( s e. ( A (,) B ) -> s e. RR )
24	23	adantl	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
25	22 24	readdcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
26	21 25	ffvelcdmd	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
27	12	adantr	\|- ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
28	26 27	resubcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
29		ioossicc	\|- ( A (,) B ) C_ ( A [,] B )
30	29	sseli	\|- ( s e. ( A (,) B ) -> s e. ( A [,] B ) )
31	30	ad2antlr	\|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ -. s =/= 0 ) -> s e. ( A [,] B ) )
32		id	\|- ( s =/= 0 -> s =/= 0 )
33	32	necon1bi	\|- ( -. s =/= 0 -> s = 0 )
34	33	eleq1d	\|- ( -. s =/= 0 -> ( s e. ( A [,] B ) <-> 0 e. ( A [,] B ) ) )
35	34	adantl	\|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ -. s =/= 0 ) -> ( s e. ( A [,] B ) <-> 0 e. ( A [,] B ) ) )
36	31 35	mpbid	\|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ -. s =/= 0 ) -> 0 e. ( A [,] B ) )
37	11	ad2antrr	\|- ( ( ( ph /\ s e. ( A (,) B ) ) /\ -. s =/= 0 ) -> -. 0 e. ( A [,] B ) )
38	36 37	condan	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
39	28 24 38	redivcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - C ) / s ) e. RR )
40	39 16	fmptd	\|- ( ph -> H : ( A (,) B ) --> RR )
41	40	ffvelcdmda	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( H ` s ) e. RR )
42		2re	\|- 2 e. RR
43	42	a1i	\|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. RR )
44	24	rehalfcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR )
45	44	resincld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR )
46	43 45	remulcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
47		2cnd	\|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC )
48	24	recnd	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
49	48	halfcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. CC )
50	49	sincld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
51		2ne0	\|- 2 =/= 0
52	51	a1i	\|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 )
53	10	sselda	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) )
54		fourierdlem44	\|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
55	53 38 54	syl2anc	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
56	47 50 52 55	mulne0d	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
57	24 46 56	redivcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
58	57 17	fmptd	\|- ( ph -> K : ( A (,) B ) --> RR )
59	58	ffvelcdmda	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) e. RR )
60	40	feqmptd	\|- ( ph -> H = ( s e. ( A (,) B ) \|-> ( H ` s ) ) )
61	58	feqmptd	\|- ( ph -> K = ( s e. ( A (,) B ) \|-> ( K ` s ) ) )
62	20 41 59 60 61	offval2	\|- ( ph -> ( H oF x. K ) = ( s e. ( A (,) B ) \|-> ( ( H ` s ) x. ( K ` s ) ) ) )
63	18 62	eqtr4id	\|- ( ph -> O = ( H oF x. K ) )
64	63	oveq2d	\|- ( ph -> ( RR _D O ) = ( RR _D ( H oF x. K ) ) )
65		reelprrecn	\|- RR e. { RR , CC }
66	65	a1i	\|- ( ph -> RR e. { RR , CC } )
67	26	recnd	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
68	12	recnd	\|- ( ph -> C e. CC )
69	68	adantr	\|- ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
70	67 69	subcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
71		ioossre	\|- ( A (,) B ) C_ RR
72	71	a1i	\|- ( ph -> ( A (,) B ) C_ RR )
73	72	sselda	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
74	73	recnd	\|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
75	70 74 38	divcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - C ) / s ) e. CC )
76	75 16	fmptd	\|- ( ph -> H : ( A (,) B ) --> CC )
77	74	halfcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. CC )
78	77	sincld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
79	47 78	mulcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
80	74 79 56	divcld	\|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
81	80 17	fmptd	\|- ( ph -> K : ( A (,) B ) --> CC )
82		ax-resscn	\|- RR C_ CC
83	82	a1i	\|- ( ph -> RR C_ CC )
84		ssid	\|- CC C_ CC
85	84	a1i	\|- ( ph -> CC C_ CC )
86		cncfss	\|- ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> RR ) C_ ( ( A (,) B ) -cn-> CC ) )
87	83 85 86	syl2anc	\|- ( ph -> ( ( A (,) B ) -cn-> RR ) C_ ( ( A (,) B ) -cn-> CC ) )
88	38	nelrdva	\|- ( ph -> -. 0 e. ( A (,) B ) )
89	1 83	fssd	\|- ( ph -> F : RR --> CC )
90		ssid	\|- RR C_ RR
91	90	a1i	\|- ( ph -> RR C_ RR )
92		ioossre	\|- ( ( X + A ) (,) ( X + B ) ) C_ RR
93	92	a1i	\|- ( ph -> ( ( X + A ) (,) ( X + B ) ) C_ RR )
94		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
95		tgioo4	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
96	94 95	dvres	\|- ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( X + A ) (,) ( X + B ) ) C_ RR ) ) -> ( RR _D ( F \|` ( ( X + A ) (,) ( X + B ) ) ) ) = ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( X + A ) (,) ( X + B ) ) ) ) )
97	83 89 91 93 96	syl22anc	\|- ( ph -> ( RR _D ( F \|` ( ( X + A ) (,) ( X + B ) ) ) ) = ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( X + A ) (,) ( X + B ) ) ) ) )
98		ioontr	\|- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( X + A ) (,) ( X + B ) ) ) = ( ( X + A ) (,) ( X + B ) )
99	98	reseq2i	\|- ( ( RR _D F ) \|` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( X + A ) (,) ( X + B ) ) ) ) = ( ( RR _D F ) \|` ( ( X + A ) (,) ( X + B ) ) )
100	97 99	eqtrdi	\|- ( ph -> ( RR _D ( F \|` ( ( X + A ) (,) ( X + B ) ) ) ) = ( ( RR _D F ) \|` ( ( X + A ) (,) ( X + B ) ) ) )
101	3	fourierdlem2	\|- ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
102	4 101	syl	\|- ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
103	5 102	mpbid	\|- ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
104	103	simpld	\|- ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
105		elmapi	\|- ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
106	104 105	syl	\|- ( ph -> V : ( 0 ... M ) --> RR )
107		elfzofz	\|- ( U e. ( 0 ..^ M ) -> U e. ( 0 ... M ) )
108	14 107	syl	\|- ( ph -> U e. ( 0 ... M ) )
109	106 108	ffvelcdmd	\|- ( ph -> ( V ` U ) e. RR )
110	109	rexrd	\|- ( ph -> ( V ` U ) e. RR* )
111		fzofzp1	\|- ( U e. ( 0 ..^ M ) -> ( U + 1 ) e. ( 0 ... M ) )
112	14 111	syl	\|- ( ph -> ( U + 1 ) e. ( 0 ... M ) )
113	106 112	ffvelcdmd	\|- ( ph -> ( V ` ( U + 1 ) ) e. RR )
114	113	rexrd	\|- ( ph -> ( V ` ( U + 1 ) ) e. RR* )
115		pire	\|- _pi e. RR
116	115	a1i	\|- ( ph -> _pi e. RR )
117	116	renegcld	\|- ( ph -> -u _pi e. RR )
118	117 116 2 3 4 5 108 13	fourierdlem13	\|- ( ph -> ( ( Q ` U ) = ( ( V ` U ) - X ) /\ ( V ` U ) = ( X + ( Q ` U ) ) ) )
119	118	simprd	\|- ( ph -> ( V ` U ) = ( X + ( Q ` U ) ) )
120	118	simpld	\|- ( ph -> ( Q ` U ) = ( ( V ` U ) - X ) )
121	109 2	resubcld	\|- ( ph -> ( ( V ` U ) - X ) e. RR )
122	120 121	eqeltrd	\|- ( ph -> ( Q ` U ) e. RR )
123	117 116 2 3 4 5 112 13	fourierdlem13	\|- ( ph -> ( ( Q ` ( U + 1 ) ) = ( ( V ` ( U + 1 ) ) - X ) /\ ( V ` ( U + 1 ) ) = ( X + ( Q ` ( U + 1 ) ) ) ) )
124	123	simpld	\|- ( ph -> ( Q ` ( U + 1 ) ) = ( ( V ` ( U + 1 ) ) - X ) )
125	113 2	resubcld	\|- ( ph -> ( ( V ` ( U + 1 ) ) - X ) e. RR )
126	124 125	eqeltrd	\|- ( ph -> ( Q ` ( U + 1 ) ) e. RR )
127	122 126 7 8 9 15	fourierdlem10	\|- ( ph -> ( ( Q ` U ) <_ A /\ B <_ ( Q ` ( U + 1 ) ) ) )
128	127	simpld	\|- ( ph -> ( Q ` U ) <_ A )
129	122 7 2 128	leadd2dd	\|- ( ph -> ( X + ( Q ` U ) ) <_ ( X + A ) )
130	119 129	eqbrtrd	\|- ( ph -> ( V ` U ) <_ ( X + A ) )
131	127	simprd	\|- ( ph -> B <_ ( Q ` ( U + 1 ) ) )
132	8 126 2 131	leadd2dd	\|- ( ph -> ( X + B ) <_ ( X + ( Q ` ( U + 1 ) ) ) )
133	123	simprd	\|- ( ph -> ( V ` ( U + 1 ) ) = ( X + ( Q ` ( U + 1 ) ) ) )
134	132 133	breqtrrd	\|- ( ph -> ( X + B ) <_ ( V ` ( U + 1 ) ) )
135		ioossioo	\|- ( ( ( ( V ` U ) e. RR* /\ ( V ` ( U + 1 ) ) e. RR* ) /\ ( ( V ` U ) <_ ( X + A ) /\ ( X + B ) <_ ( V ` ( U + 1 ) ) ) ) -> ( ( X + A ) (,) ( X + B ) ) C_ ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) )
136	110 114 130 134 135	syl22anc	\|- ( ph -> ( ( X + A ) (,) ( X + B ) ) C_ ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) )
137	136	resabs1d	\|- ( ph -> ( ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) \|` ( ( X + A ) (,) ( X + B ) ) ) = ( ( RR _D F ) \|` ( ( X + A ) (,) ( X + B ) ) ) )
138	137	eqcomd	\|- ( ph -> ( ( RR _D F ) \|` ( ( X + A ) (,) ( X + B ) ) ) = ( ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) \|` ( ( X + A ) (,) ( X + B ) ) ) )
139	14	ancli	\|- ( ph -> ( ph /\ U e. ( 0 ..^ M ) ) )
140		eleq1	\|- ( i = U -> ( i e. ( 0 ..^ M ) <-> U e. ( 0 ..^ M ) ) )
141	140	anbi2d	\|- ( i = U -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ U e. ( 0 ..^ M ) ) ) )
142		fveq2	\|- ( i = U -> ( V ` i ) = ( V ` U ) )
143		oveq1	\|- ( i = U -> ( i + 1 ) = ( U + 1 ) )
144	143	fveq2d	\|- ( i = U -> ( V ` ( i + 1 ) ) = ( V ` ( U + 1 ) ) )
145	142 144	oveq12d	\|- ( i = U -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) = ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) )
146	145	reseq2d	\|- ( i = U -> ( ( RR _D F ) \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) )
147	145	oveq1d	\|- ( i = U -> ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) = ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) )
148	146 147	eleq12d	\|- ( i = U -> ( ( ( RR _D F ) \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) <-> ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) e. ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) ) )
149	141 148	imbi12d	\|- ( i = U -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) ) <-> ( ( ph /\ U e. ( 0 ..^ M ) ) -> ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) e. ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) ) ) )
150	149 6	vtoclg	\|- ( U e. ( 0 ..^ M ) -> ( ( ph /\ U e. ( 0 ..^ M ) ) -> ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) e. ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) ) )
151	14 139 150	sylc	\|- ( ph -> ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) e. ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) )
152		rescncf	\|- ( ( ( X + A ) (,) ( X + B ) ) C_ ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -> ( ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) e. ( ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) -cn-> RR ) -> ( ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) \|` ( ( X + A ) (,) ( X + B ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) ) )
153	136 151 152	sylc	\|- ( ph -> ( ( ( RR _D F ) \|` ( ( V ` U ) (,) ( V ` ( U + 1 ) ) ) ) \|` ( ( X + A ) (,) ( X + B ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) )
154	138 153	eqeltrd	\|- ( ph -> ( ( RR _D F ) \|` ( ( X + A ) (,) ( X + B ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) )
155	100 154	eqeltrd	\|- ( ph -> ( RR _D ( F \|` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) )
156	1 2 7 8 88 155 12 16	fourierdlem59	\|- ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) )
157	87 156	sseldd	\|- ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) )
158		iooretop	\|- ( A (,) B ) e. ( topGen ` ran (,) )
159	158	a1i	\|- ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
160	17 10 88 159	fourierdlem58	\|- ( ph -> ( RR _D K ) e. ( ( A (,) B ) -cn-> RR ) )
161	87 160	sseldd	\|- ( ph -> ( RR _D K ) e. ( ( A (,) B ) -cn-> CC ) )
162	66 76 81 157 161	dvmulcncf	\|- ( ph -> ( RR _D ( H oF x. K ) ) e. ( ( A (,) B ) -cn-> CC ) )
163	64 162	eqeltrd	\|- ( ph -> ( RR _D O ) e. ( ( A (,) B ) -cn-> CC ) )

Metamath Proof Explorer

Theorem fourierdlem72

Proof