Metamath Proof Explorer

Theorem 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 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 ) ) ) } )
fourierdlem88.f 
|- ( ph -> F : RR --> RR )
fourierdlem88.x 
|- ( ph -> X e. ran V )
fourierdlem88.y 
|- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem88.w 
|- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem88.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem88.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem88.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem88.n 
|- ( ph -> N e. RR )
fourierdlem88.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
fourierdlem88.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem88.m 
|- ( ph -> M e. NN )
fourierdlem88.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem88.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem88.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
fourierdlem88.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
fourierdlem88.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem88.o 
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem88.i 
|- I = ( RR _D F )
fourierdlem88.ifn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
fourierdlem88.c 
|- ( ph -> C e. ( ( I |` ( -oo (,) X ) ) limCC X ) )
fourierdlem88.d 
|- ( ph -> D e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
Assertion fourierdlem88 
|- ( ph -> G e. L^1 )

Proof

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