Metamath Proof Explorer

Theorem fourierdlem74

Description: Given a piecewise smooth function F , the derived function H has a limit at the upper bound of each interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem74.xre 
|- ( ph -> X e. RR )
fourierdlem74.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 ) ) ) } )
fourierdlem74.f 
|- ( ph -> F : RR --> RR )
fourierdlem74.x 
|- ( ph -> X e. ran V )
fourierdlem74.y 
|- ( ph -> Y e. RR )
fourierdlem74.w 
|- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem74.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem74.m 
|- ( ph -> M e. NN )
fourierdlem74.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem74.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
fourierdlem74.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem74.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 ) ) ) } )
fourierdlem74.g 
|- G = ( RR _D F )
fourierdlem74.gcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
fourierdlem74.e 
|- ( ph -> E e. ( ( G |` ( -oo (,) X ) ) limCC X ) )
fourierdlem74.a 
|- A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem74 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem74.xre 
 |-  ( ph -> X e. RR )
2 fourierdlem74.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 ) ) ) } )
3 fourierdlem74.f 
 |-  ( ph -> F : RR --> RR )
4 fourierdlem74.x 
 |-  ( ph -> X e. ran V )
5 fourierdlem74.y 
 |-  ( ph -> Y e. RR )
6 fourierdlem74.w 
 |-  ( ph -> W e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
7 fourierdlem74.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
8 fourierdlem74.m 
 |-  ( ph -> M e. NN )
9 fourierdlem74.v 
 |-  ( ph -> V e. ( P ` M ) )
10 fourierdlem74.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
11 fourierdlem74.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
12 fourierdlem74.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 ) ) ) } )
13 fourierdlem74.g 
 |-  G = ( RR _D F )
14 fourierdlem74.gcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
15 fourierdlem74.e 
 |-  ( ph -> E e. ( ( G |` ( -oo (,) X ) ) limCC X ) )
16 fourierdlem74.a 
 |-  A = if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
17 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
18 pire 
 |-  _pi e. RR
19 18 renegcli 
 |-  -u _pi e. RR
20 19 a1i 
 |-  ( ph -> -u _pi e. RR )
21 20 1 readdcld 
 |-  ( ph -> ( -u _pi + X ) e. RR )
22 18 a1i 
 |-  ( ph -> _pi e. RR )
23 22 1 readdcld 
 |-  ( ph -> ( _pi + X ) e. RR )
24 21 23 iccssred 
 |-  ( ph -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
25 24 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
26 2 8 9 fourierdlem15 
 |-  ( ph -> V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) )
27 26 ffvelrnda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) )
28 25 27 sseldd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. RR )
29 17 28 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
30 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) e. RR )
31 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X e. RR )
32 2 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 ) ) ) ) ) )
33 8 32 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 ) ) ) ) ) )
34 9 33 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 ) ) ) ) )
35 34 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
36 35 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
37 36 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
38 eqcom 
 |-  ( ( V ` ( i + 1 ) ) = X <-> X = ( V ` ( i + 1 ) ) )
39 38 biimpi 
 |-  ( ( V ` ( i + 1 ) ) = X -> X = ( V ` ( i + 1 ) ) )
40 39 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X = ( V ` ( i + 1 ) ) )
41 37 40 breqtrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( V ` i ) < X )
42 ioossre 
 |-  ( ( V ` i ) (,) X ) C_ RR
43 42 a1i 
 |-  ( ph -> ( ( V ` i ) (,) X ) C_ RR )
44 3 43 fssresd 
 |-  ( ph -> ( F |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
45 44 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( F |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
46 limcresi 
 |-  ( ( F |` ( -oo (,) X ) ) limCC X ) C_ ( ( ( F |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X )
47 46 6 sselid 
 |-  ( ph -> W e. ( ( ( F |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X ) )
48 47 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( ( F |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X ) )
49 mnfxr 
 |-  -oo e. RR*
50 49 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo e. RR* )
51 29 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR* )
52 29 mnfltd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo < ( V ` i ) )
53 50 51 52 xrltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -oo <_ ( V ` i ) )
54 iooss1 
 |-  ( ( -oo e. RR* /\ -oo <_ ( V ` i ) ) -> ( ( V ` i ) (,) X ) C_ ( -oo (,) X ) )
55 50 53 54 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) (,) X ) C_ ( -oo (,) X ) )
56 55 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) = ( F |` ( ( V ` i ) (,) X ) ) )
57 56 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( F |` ( ( V ` i ) (,) X ) ) limCC X ) )
58 48 57 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( F |` ( ( V ` i ) (,) X ) ) limCC X ) )
59 58 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> W e. ( ( F |` ( ( V ` i ) (,) X ) ) limCC X ) )
60 eqid 
 |-  ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = ( RR _D ( F |` ( ( V ` i ) (,) X ) ) )
61 ax-resscn 
 |-  RR C_ CC
62 61 a1i 
 |-  ( ph -> RR C_ CC )
63 3 62 fssd 
 |-  ( ph -> F : RR --> CC )
64 ssid 
 |-  RR C_ RR
65 64 a1i 
 |-  ( ph -> RR C_ RR )
66 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
67 66 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
68 66 67 dvres 
 |-  ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( V ` i ) (,) X ) C_ RR ) ) -> ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) )
69 62 63 65 43 68 syl22anc 
 |-  ( ph -> ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) )
70 13 eqcomi 
 |-  ( RR _D F ) = G
71 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X )
72 70 71 reseq12i 
 |-  ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) = ( G |` ( ( V ` i ) (,) X ) )
73 72 a1i 
 |-  ( ph -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( V ` i ) (,) X ) ) ) = ( G |` ( ( V ` i ) (,) X ) ) )
74 69 73 eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = ( G |` ( ( V ` i ) (,) X ) ) )
75 74 dmeqd 
 |-  ( ph -> dom ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = dom ( G |` ( ( V ` i ) (,) X ) ) )
76 75 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = dom ( G |` ( ( V ` i ) (,) X ) ) )
77 14 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
78 oveq2 
 |-  ( ( V ` ( i + 1 ) ) = X -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) = ( ( V ` i ) (,) X ) )
79 78 reseq2d 
 |-  ( ( V ` ( i + 1 ) ) = X -> ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( G |` ( ( V ` i ) (,) X ) ) )
80 79 78 feq12d 
 |-  ( ( V ` ( i + 1 ) ) = X -> ( ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR <-> ( G |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR ) )
81 80 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( G |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR <-> ( G |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR ) )
82 77 81 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( G |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR )
83 fdm 
 |-  ( ( G |` ( ( V ` i ) (,) X ) ) : ( ( V ` i ) (,) X ) --> RR -> dom ( G |` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X ) )
84 82 83 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( G |` ( ( V ` i ) (,) X ) ) = ( ( V ` i ) (,) X ) )
85 76 84 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> dom ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) = ( ( V ` i ) (,) X ) )
86 limcresi 
 |-  ( ( G |` ( -oo (,) X ) ) limCC X ) C_ ( ( ( G |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X )
87 55 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) = ( G |` ( ( V ` i ) (,) X ) ) )
88 87 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( G |` ( -oo (,) X ) ) |` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( G |` ( ( V ` i ) (,) X ) ) limCC X ) )
89 86 88 sseqtrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( -oo (,) X ) ) limCC X ) C_ ( ( G |` ( ( V ` i ) (,) X ) ) limCC X ) )
90 15 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( G |` ( -oo (,) X ) ) limCC X ) )
91 89 90 sseldd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( G |` ( ( V ` i ) (,) X ) ) limCC X ) )
92 69 73 eqtr2d 
 |-  ( ph -> ( G |` ( ( V ` i ) (,) X ) ) = ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) )
93 92 oveq1d 
 |-  ( ph -> ( ( G |` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) limCC X ) )
94 93 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( ( V ` i ) (,) X ) ) limCC X ) = ( ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) limCC X ) )
95 91 94 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E e. ( ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) limCC X ) )
96 95 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> E e. ( ( RR _D ( F |` ( ( V ` i ) (,) X ) ) ) limCC X ) )
97 eqid 
 |-  ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
98 oveq2 
 |-  ( x = s -> ( X + x ) = ( X + s ) )
99 98 fveq2d 
 |-  ( x = s -> ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) = ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
100 99 oveq1d 
 |-  ( x = s -> ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) - W ) = ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
101 100 cbvmptv 
 |-  ( x e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + x ) ) - W ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
102 id 
 |-  ( x = s -> x = s )
103 102 cbvmptv 
 |-  ( x e. ( ( ( V ` i ) - X ) (,) 0 ) |-> x ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> s )
104 30 31 41 45 59 60 85 96 97 101 103 fourierdlem60 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> E e. ( ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) limCC 0 ) )
105 iftrue 
 |-  ( ( V ` ( i + 1 ) ) = X -> if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) = E )
106 16 105 syl5eq 
 |-  ( ( V ` ( i + 1 ) ) = X -> A = E )
107 106 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> A = E )
108 7 reseq1i 
 |-  ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
109 108 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
110 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
111 19 rexri 
 |-  -u _pi e. RR*
112 111 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
113 18 rexri 
 |-  _pi e. RR*
114 113 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
115 19 a1i 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi e. RR )
116 18 a1i 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> _pi e. RR )
117 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
118 28 117 resubcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. RR )
119 20 recnd 
 |-  ( ph -> -u _pi e. CC )
120 1 recnd 
 |-  ( ph -> X e. CC )
121 119 120 pncand 
 |-  ( ph -> ( ( -u _pi + X ) - X ) = -u _pi )
122 121 eqcomd 
 |-  ( ph -> -u _pi = ( ( -u _pi + X ) - X ) )
123 122 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi = ( ( -u _pi + X ) - X ) )
124 21 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( -u _pi + X ) e. RR )
125 23 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( _pi + X ) e. RR )
126 elicc2 
 |-  ( ( ( -u _pi + X ) e. RR /\ ( _pi + X ) e. RR ) -> ( ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) <-> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) ) )
127 124 125 126 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) <-> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) ) )
128 27 127 mpbid 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) e. RR /\ ( -u _pi + X ) <_ ( V ` i ) /\ ( V ` i ) <_ ( _pi + X ) ) )
129 128 simp2d 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( -u _pi + X ) <_ ( V ` i ) )
130 124 28 117 129 lesub1dd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( -u _pi + X ) - X ) <_ ( ( V ` i ) - X ) )
131 123 130 eqbrtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> -u _pi <_ ( ( V ` i ) - X ) )
132 128 simp3d 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) <_ ( _pi + X ) )
133 28 125 117 132 lesub1dd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) <_ ( ( _pi + X ) - X ) )
134 116 recnd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> _pi e. CC )
135 120 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> X e. CC )
136 134 135 pncand 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( _pi + X ) - X ) = _pi )
137 133 136 breqtrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) <_ _pi )
138 115 116 118 131 137 eliccd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. ( -u _pi [,] _pi ) )
139 138 11 fmptd 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
140 139 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
141 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
142 112 114 140 141 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
143 110 142 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
144 143 resmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) )
145 144 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) )
146 17 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
147 17 118 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
148 11 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
149 146 147 148 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
150 149 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
151 fveq2 
 |-  ( i = j -> ( V ` i ) = ( V ` j ) )
152 151 oveq1d 
 |-  ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
153 152 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
154 11 153 eqtri 
 |-  Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
155 154 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
156 fveq2 
 |-  ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
157 156 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
158 157 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
159 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
160 159 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
161 34 simpld 
 |-  ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
162 elmapi 
 |-  ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
163 161 162 syl 
 |-  ( ph -> V : ( 0 ... M ) --> RR )
164 163 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> RR )
165 164 160 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
166 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
167 165 166 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
168 155 158 160 167 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
169 168 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
170 oveq1 
 |-  ( ( V ` ( i + 1 ) ) = X -> ( ( V ` ( i + 1 ) ) - X ) = ( X - X ) )
171 170 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( V ` ( i + 1 ) ) - X ) = ( X - X ) )
172 120 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> X e. CC )
173 172 subidd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( X - X ) = 0 )
174 17 173 sylanl2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( X - X ) = 0 )
175 169 171 174 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = 0 )
176 150 175 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( V ` i ) - X ) (,) 0 ) )
177 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = 0 ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
178 8 adantr 
 |-  ( ( ph /\ s = 0 ) -> M e. NN )
179 20 22 1 2 12 8 9 11 fourierdlem14 
 |-  ( ph -> Q e. ( O ` M ) )
180 179 adantr 
 |-  ( ( ph /\ s = 0 ) -> Q e. ( O ` M ) )
181 simpr 
 |-  ( ( ph /\ s = 0 ) -> s = 0 )
182 ffn 
 |-  ( V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) -> V Fn ( 0 ... M ) )
183 fvelrnb 
 |-  ( V Fn ( 0 ... M ) -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
184 26 182 183 3syl 
 |-  ( ph -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
185 4 184 mpbid 
 |-  ( ph -> E. i e. ( 0 ... M ) ( V ` i ) = X )
186 simpr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( 0 ... M ) )
187 11 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. ( -u _pi [,] _pi ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
188 186 138 187 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
189 188 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
190 oveq1 
 |-  ( ( V ` i ) = X -> ( ( V ` i ) - X ) = ( X - X ) )
191 190 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( ( V ` i ) - X ) = ( X - X ) )
192 120 subidd 
 |-  ( ph -> ( X - X ) = 0 )
193 192 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( X - X ) = 0 )
194 189 191 193 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( Q ` i ) = 0 )
195 194 ex 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) = X -> ( Q ` i ) = 0 ) )
196 195 reximdva 
 |-  ( ph -> ( E. i e. ( 0 ... M ) ( V ` i ) = X -> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
197 185 196 mpd 
 |-  ( ph -> E. i e. ( 0 ... M ) ( Q ` i ) = 0 )
198 118 11 fmptd 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
199 ffn 
 |-  ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
200 fvelrnb 
 |-  ( Q Fn ( 0 ... M ) -> ( 0 e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
201 198 199 200 3syl 
 |-  ( ph -> ( 0 e. ran Q <-> E. i e. ( 0 ... M ) ( Q ` i ) = 0 ) )
202 197 201 mpbird 
 |-  ( ph -> 0 e. ran Q )
203 202 adantr 
 |-  ( ( ph /\ s = 0 ) -> 0 e. ran Q )
204 181 203 eqeltrd 
 |-  ( ( ph /\ s = 0 ) -> s e. ran Q )
205 12 178 180 204 fourierdlem12 
 |-  ( ( ( ph /\ s = 0 ) /\ i e. ( 0 ..^ M ) ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
206 205 an32s 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = 0 ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
207 206 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = 0 ) -> -. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
208 177 207 pm2.65da 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
209 208 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
210 209 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
211 elioore 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
212 211 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
213 0red 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
214 elioo3g 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. RR* ) /\ ( ( Q ` i ) < s /\ s < ( Q ` ( i + 1 ) ) ) ) )
215 214 biimpi 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. RR* ) /\ ( ( Q ` i ) < s /\ s < ( Q ` ( i + 1 ) ) ) ) )
216 215 simprrd 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s < ( Q ` ( i + 1 ) ) )
217 216 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
218 175 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) = 0 )
219 217 218 breqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < 0 )
220 212 213 219 ltnsymd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. 0 < s )
221 220 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = W )
222 221 oveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - W ) )
223 222 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) = ( ( ( F ` ( X + s ) ) - W ) / s ) )
224 51 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
225 1 rexrd 
 |-  ( ph -> X e. RR* )
226 225 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR* )
227 166 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
228 227 212 readdcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
229 120 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. CC )
230 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
231 19 18 230 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
232 231 61 sstri 
 |-  ( -u _pi [,] _pi ) C_ CC
233 188 138 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
234 17 233 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
235 232 234 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
236 229 235 addcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` i ) ) = ( ( Q ` i ) + X ) )
237 149 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + X ) = ( ( ( V ` i ) - X ) + X ) )
238 29 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. CC )
239 238 229 npcand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( V ` i ) - X ) + X ) = ( V ` i ) )
240 236 237 239 3eqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
241 240 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
242 149 147 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
243 242 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
244 211 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
245 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
246 215 simprld 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < s )
247 246 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
248 243 244 245 247 ltadd2dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` i ) ) < ( X + s ) )
249 241 248 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
250 249 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
251 ltaddneg 
 |-  ( ( s e. RR /\ X e. RR ) -> ( s < 0 <-> ( X + s ) < X ) )
252 212 227 251 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s < 0 <-> ( X + s ) < X ) )
253 219 252 mpbid 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < X )
254 224 226 228 250 253 eliood 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) X ) )
255 fvres 
 |-  ( ( X + s ) e. ( ( V ` i ) (,) X ) -> ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
256 255 eqcomd 
 |-  ( ( X + s ) e. ( ( V ` i ) (,) X ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
257 254 256 syl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) )
258 257 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - W ) = ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) )
259 258 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - W ) / s ) = ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
260 210 223 259 3eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) )
261 176 260 mpteq12dva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) )
262 109 145 261 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) )
263 262 175 oveq12d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( ( V ` i ) - X ) (,) 0 ) |-> ( ( ( ( F |` ( ( V ` i ) (,) X ) ) ` ( X + s ) ) - W ) / s ) ) limCC 0 ) )
264 104 107 263 3eltr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
265 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) )
266 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> s ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> s )
267 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
268 3 adantr 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> F : RR --> RR )
269 1 adantr 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
270 211 adantl 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
271 269 270 readdcld 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
272 268 271 ffvelrnd 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. RR )
273 272 recnd 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
274 273 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
275 274 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
276 5 recnd 
 |-  ( ph -> Y e. CC )
277 limccl 
 |-  ( ( F |` ( -oo (,) X ) ) limCC X ) C_ CC
278 277 6 sselid 
 |-  ( ph -> W e. CC )
279 276 278 ifcld 
 |-  ( ph -> if ( 0 < s , Y , W ) e. CC )
280 279 adantr 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
281 280 3ad2antl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
282 275 281 subcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC )
283 211 recnd 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. CC )
284 283 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. CC )
285 velsn 
 |-  ( s e. { 0 } <-> s = 0 )
286 208 285 sylnibr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s e. { 0 } )
287 286 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s e. { 0 } )
288 284 287 eldifd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( CC \ { 0 } ) )
289 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) )
290 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> W ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> W )
291 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) )
292 278 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> W e. CC )
293 3 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> RR )
294 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
295 294 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
296 51 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
297 165 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR* )
298 297 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` ( i + 1 ) ) e. RR* )
299 271 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
300 198 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
301 300 160 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
302 301 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
303 216 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
304 244 302 245 303 ltadd2dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( X + ( Q ` ( i + 1 ) ) ) )
305 168 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( X + ( ( V ` ( i + 1 ) ) - X ) ) )
306 165 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. CC )
307 229 306 pncan3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( V ` ( i + 1 ) ) - X ) ) = ( V ` ( i + 1 ) ) )
308 305 307 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
309 308 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
310 304 309 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( V ` ( i + 1 ) ) )
311 296 298 299 249 310 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
312 ioossre 
 |-  ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR
313 312 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR )
314 244 303 ltned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= ( Q ` ( i + 1 ) ) )
315 308 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) = ( X + ( Q ` ( i + 1 ) ) ) )
316 315 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 ) ) ) ) )
317 10 316 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` ( i + 1 ) ) ) ) )
318 301 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
319 293 166 295 289 311 313 314 317 318 fourierdlem53 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
320 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
321 320 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
322 278 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. CC )
323 290 321 322 318 constlimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> W e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> W ) limCC ( Q ` ( i + 1 ) ) ) )
324 289 290 291 274 292 319 323 sublimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R - W ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
325 324 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - W ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
326 iftrue 
 |-  ( ( V ` ( i + 1 ) ) < X -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) = W )
327 326 oveq2d 
 |-  ( ( V ` ( i + 1 ) ) < X -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) = ( R - W ) )
328 327 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) = ( R - W ) )
329 211 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
330 0red 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
331 301 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
332 216 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
333 168 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
334 165 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
335 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> X e. RR )
336 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) < X )
337 334 335 336 ltled 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) <_ X )
338 334 335 suble0d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( ( V ` ( i + 1 ) ) - X ) <_ 0 <-> ( V ` ( i + 1 ) ) <_ X ) )
339 337 338 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( V ` ( i + 1 ) ) - X ) <_ 0 )
340 333 339 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( Q ` ( i + 1 ) ) <_ 0 )
341 340 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) <_ 0 )
342 329 331 330 332 341 ltletrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < 0 )
343 329 330 342 ltnsymd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. 0 < s )
344 343 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = W )
345 344 oveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - W ) )
346 345 mpteq2dva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) ) )
347 346 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - W ) ) limCC ( Q ` ( i + 1 ) ) ) )
348 325 328 347 3eltr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
349 348 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
350 simpl1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ph )
351 simpl2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> i e. ( 0 ..^ M ) )
352 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X e. RR )
353 352 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X e. RR )
354 165 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
355 354 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( V ` ( i + 1 ) ) e. RR )
356 neqne 
 |-  ( -. ( V ` ( i + 1 ) ) = X -> ( V ` ( i + 1 ) ) =/= X )
357 356 necomd 
 |-  ( -. ( V ` ( i + 1 ) ) = X -> X =/= ( V ` ( i + 1 ) ) )
358 357 adantr 
 |-  ( ( -. ( V ` ( i + 1 ) ) = X /\ -. ( V ` ( i + 1 ) ) < X ) -> X =/= ( V ` ( i + 1 ) ) )
359 358 3ad2antl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X =/= ( V ` ( i + 1 ) ) )
360 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> -. ( V ` ( i + 1 ) ) < X )
361 353 355 359 360 lttri5d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> X < ( V ` ( i + 1 ) ) )
362 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( 0 < s , Y , W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( 0 < s , Y , W ) )
363 274 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
364 279 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
365 319 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> R e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
366 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y )
367 276 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Y e. CC )
368 366 321 367 318 constlimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Y e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
369 368 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> Y e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
370 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X e. RR )
371 165 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( V ` ( i + 1 ) ) e. RR )
372 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X < ( V ` ( i + 1 ) ) )
373 370 371 372 ltnsymd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> -. ( V ` ( i + 1 ) ) < X )
374 373 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) = Y )
375 0red 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. RR )
376 242 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
377 211 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
378 192 eqcomd 
 |-  ( ph -> 0 = ( X - X ) )
379 378 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 = ( X - X ) )
380 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( V ` i ) e. RR )
381 51 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) e. RR* )
382 297 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` ( i + 1 ) ) e. RR* )
383 166 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X e. RR )
384 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> -. X <_ ( V ` i ) )
385 29 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) e. RR )
386 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> X e. RR )
387 385 386 ltnled 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( ( V ` i ) < X <-> -. X <_ ( V ` i ) ) )
388 384 387 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) < X )
389 388 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> ( V ` i ) < X )
390 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X < ( V ` ( i + 1 ) ) )
391 381 382 383 389 390 eliood 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
392 2 8 9 4 fourierdlem12 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
393 392 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ -. X <_ ( V ` i ) ) -> -. X e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
394 391 393 condan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> X <_ ( V ` i ) )
395 370 380 370 394 lesub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( X - X ) <_ ( ( V ` i ) - X ) )
396 379 395 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 <_ ( ( V ` i ) - X ) )
397 149 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) = ( Q ` i ) )
398 397 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( ( V ` i ) - X ) = ( Q ` i ) )
399 396 398 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> 0 <_ ( Q ` i ) )
400 399 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 <_ ( Q ` i ) )
401 246 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
402 375 376 377 400 401 lelttrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 < s )
403 402 iftrued 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) = Y )
404 403 mpteq2dva 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( 0 < s , Y , W ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y ) )
405 404 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( 0 < s , Y , W ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> Y ) limCC ( Q ` ( i + 1 ) ) ) )
406 369 374 405 3eltr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> if ( ( V ` ( i + 1 ) ) < X , W , Y ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> if ( 0 < s , Y , W ) ) limCC ( Q ` ( i + 1 ) ) ) )
407 289 362 265 363 364 365 406 sublimc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ X < ( V ` ( i + 1 ) ) ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
408 350 351 361 407 syl21anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ -. ( V ` ( i + 1 ) ) < X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
409 349 408 pm2.61dan 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
410 321 266 318 idlimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> s ) limCC ( Q ` ( i + 1 ) ) ) )
411 410 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> s ) limCC ( Q ` ( i + 1 ) ) ) )
412 168 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
413 306 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( V ` ( i + 1 ) ) e. CC )
414 229 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> X e. CC )
415 356 3ad2ant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( V ` ( i + 1 ) ) =/= X )
416 413 414 415 subne0d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( V ` ( i + 1 ) ) - X ) =/= 0 )
417 412 416 eqnetrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( Q ` ( i + 1 ) ) =/= 0 )
418 208 3adantl3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -. s = 0 )
419 418 neqned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= 0 )
420 265 266 267 282 288 409 411 417 419 divlimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) limCC ( Q ` ( i + 1 ) ) ) )
421 iffalse 
 |-  ( -. ( V ` ( i + 1 ) ) = X -> if ( ( V ` ( i + 1 ) ) = X , E , ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
422 16 421 syl5eq 
 |-  ( -. ( V ` ( i + 1 ) ) = X -> A = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
423 422 3ad2ant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A = ( ( R - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
424 ioossre 
 |-  ( -oo (,) X ) C_ RR
425 424 a1i 
 |-  ( ph -> ( -oo (,) X ) C_ RR )
426 3 425 fssresd 
 |-  ( ph -> ( F |` ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
427 424 62 sstrid 
 |-  ( ph -> ( -oo (,) X ) C_ CC )
428 49 a1i 
 |-  ( ph -> -oo e. RR* )
429 1 mnfltd 
 |-  ( ph -> -oo < X )
430 66 428 1 429 lptioo2cn 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( -oo (,) X ) ) )
431 426 427 430 6 limcrecl 
 |-  ( ph -> W e. RR )
432 3 1 5 431 7 fourierdlem9 
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> RR )
433 432 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> H : ( -u _pi [,] _pi ) --> RR )
434 433 143 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) )
435 143 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( -u _pi [,] _pi ) )
436 0cnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> 0 e. CC )
437 279 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( 0 < s , Y , W ) e. CC )
438 274 437 subcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) e. CC )
439 283 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. CC )
440 208 neqned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= 0 )
441 438 439 440 divcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) e. CC )
442 436 441 ifcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. CC )
443 7 fvmpt2 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. CC ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
444 435 442 443 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
445 208 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
446 444 445 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
447 446 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
448 434 447 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
449 448 3adant3 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
450 449 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) limCC ( Q ` ( i + 1 ) ) ) )
451 420 423 450 3eltr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
452 451 3expa 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ -. ( V ` ( i + 1 ) ) = X ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
453 264 452 pm2.61dan 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )