Metamath Proof Explorer

Theorem 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 ffvelrnd 
 |-  ( ( 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 ffvelrnda 
 |-  ( ( 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 ffvelrnda 
 |-  ( ( 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 94 tgioo2 
 |-  ( 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 ffvelrnd 
 |-  ( 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 ffvelrnd 
 |-  ( 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 ) )