This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem75

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

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

Proof

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