Metamath Proof Explorer

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