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