Metamath Proof Explorer

Theorem fourierdlem81

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . In this lemma, T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem81.a 
|- ( ph -> A e. RR )
fourierdlem81.b 
|- ( ph -> B e. RR )
fourierdlem81.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem81.m 
|- ( ph -> M e. NN )
fourierdlem81.t 
|- ( ph -> T e. RR+ )
fourierdlem81.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem81.fper 
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem81.s 
|- S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
fourierdlem81.f 
|- ( ph -> F : RR --> CC )
fourierdlem81.cncf 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem81.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem81.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem81.g 
|- G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
fourierdlem81.h 
|- H = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( G ` ( x - T ) ) )
Assertion fourierdlem81 
|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 fourierdlem81.a 
 |-  ( ph -> A e. RR )
2 fourierdlem81.b 
 |-  ( ph -> B e. RR )
3 fourierdlem81.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4 fourierdlem81.m 
 |-  ( ph -> M e. NN )
5 fourierdlem81.t 
 |-  ( ph -> T e. RR+ )
6 fourierdlem81.q 
 |-  ( ph -> Q e. ( P ` M ) )
7 fourierdlem81.fper 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
8 fourierdlem81.s 
 |-  S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) )
9 fourierdlem81.f 
 |-  ( ph -> F : RR --> CC )
10 fourierdlem81.cncf 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem81.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12 fourierdlem81.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13 fourierdlem81.g 
 |-  G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) )
14 fourierdlem81.h 
 |-  H = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( G ` ( x - T ) ) )
15 3 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
16 4 15 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
17 6 16 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
18 17 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
19 18 simpld 
 |-  ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
20 19 simpld 
 |-  ( ph -> ( Q ` 0 ) = A )
21 20 eqcomd 
 |-  ( ph -> A = ( Q ` 0 ) )
22 19 simprd 
 |-  ( ph -> ( Q ` M ) = B )
23 22 eqcomd 
 |-  ( ph -> B = ( Q ` M ) )
24 21 23 oveq12d 
 |-  ( ph -> ( A [,] B ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
25 24 itgeq1d 
 |-  ( ph -> S. ( A [,] B ) ( F ` x ) _d x = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x )
26 0zd 
 |-  ( ph -> 0 e. ZZ )
27 nnuz 
 |-  NN = ( ZZ>= ` 1 )
28 0p1e1 
 |-  ( 0 + 1 ) = 1
29 28 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
30 27 29 eqtr4i 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
31 4 30 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
32 17 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
33 reex 
 |-  RR e. _V
34 33 a1i 
 |-  ( ph -> RR e. _V )
35 ovex 
 |-  ( 0 ... M ) e. _V
36 35 a1i 
 |-  ( ph -> ( 0 ... M ) e. _V )
37 34 36 elmapd 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
38 32 37 mpbid 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
39 18 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
40 39 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
41 9 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : RR --> CC )
42 20 1 eqeltrd 
 |-  ( ph -> ( Q ` 0 ) e. RR )
43 22 2 eqeltrd 
 |-  ( ph -> ( Q ` M ) e. RR )
44 42 43 iccssred 
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
45 44 sselda 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> x e. RR )
46 41 45 ffvelcdmd 
 |-  ( ( ph /\ x e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` x ) e. CC )
47 38 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
48 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
49 48 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
50 47 49 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
51 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
52 51 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
53 47 52 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
54 9 feqmptd 
 |-  ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
55 54 reseq1d 
 |-  ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
56 55 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
57 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
58 57 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
59 58 resmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. RR |-> ( F ` x ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
60 56 59 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
61 50 53 10 12 11 iblcncfioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. L^1 )
62 60 61 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
63 9 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : RR --> CC )
64 50 53 iccssred 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ RR )
65 64 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. RR )
66 63 65 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
67 50 53 62 66 ibliooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
68 26 31 38 40 46 67 itgspltprt 
 |-  ( ph -> S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` x ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x )
69 8 a1i 
 |-  ( ph -> S = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) )
70 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
71 70 oveq1d 
 |-  ( i = 0 -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
72 71 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( ( Q ` i ) + T ) = ( ( Q ` 0 ) + T ) )
73 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
74 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
75 73 74 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
76 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
77 75 76 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
78 5 rpred 
 |-  ( ph -> T e. RR )
79 42 78 readdcld 
 |-  ( ph -> ( ( Q ` 0 ) + T ) e. RR )
80 69 72 77 79 fvmptd 
 |-  ( ph -> ( S ` 0 ) = ( ( Q ` 0 ) + T ) )
81 20 oveq1d 
 |-  ( ph -> ( ( Q ` 0 ) + T ) = ( A + T ) )
82 80 81 eqtr2d 
 |-  ( ph -> ( A + T ) = ( S ` 0 ) )
83 fveq2 
 |-  ( i = M -> ( Q ` i ) = ( Q ` M ) )
84 83 oveq1d 
 |-  ( i = M -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
85 84 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( Q ` i ) + T ) = ( ( Q ` M ) + T ) )
86 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
87 75 86 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
88 43 78 readdcld 
 |-  ( ph -> ( ( Q ` M ) + T ) e. RR )
89 69 85 87 88 fvmptd 
 |-  ( ph -> ( S ` M ) = ( ( Q ` M ) + T ) )
90 22 oveq1d 
 |-  ( ph -> ( ( Q ` M ) + T ) = ( B + T ) )
91 89 90 eqtr2d 
 |-  ( ph -> ( B + T ) = ( S ` M ) )
92 82 91 oveq12d 
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) = ( ( S ` 0 ) [,] ( S ` M ) ) )
93 92 itgeq1d 
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x )
94 38 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
95 78 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> T e. RR )
96 94 95 readdcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) + T ) e. RR )
97 96 8 fmptd 
 |-  ( ph -> S : ( 0 ... M ) --> RR )
98 78 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. RR )
99 50 53 98 40 ltadd1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
100 48 96 sylan2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) e. RR )
101 8 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) + T ) e. RR ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
102 49 100 101 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
103 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
104 103 oveq1d 
 |-  ( i = j -> ( ( Q ` i ) + T ) = ( ( Q ` j ) + T ) )
105 104 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( Q ` i ) + T ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
106 8 105 eqtri 
 |-  S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) )
107 106 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) + T ) ) )
108 fveq2 
 |-  ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
109 108 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
110 109 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
111 53 98 readdcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
112 107 110 52 111 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
113 99 102 112 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) < ( S ` ( i + 1 ) ) )
114 9 adantr 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> F : RR --> CC )
115 80 79 eqeltrd 
 |-  ( ph -> ( S ` 0 ) e. RR )
116 115 adantr 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` 0 ) e. RR )
117 89 88 eqeltrd 
 |-  ( ph -> ( S ` M ) e. RR )
118 117 adantr 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( S ` M ) e. RR )
119 116 118 iccssred 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( ( S ` 0 ) [,] ( S ` M ) ) C_ RR )
120 simpr 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. ( ( S ` 0 ) [,] ( S ` M ) ) )
121 119 120 sseldd 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> x e. RR )
122 114 121 ffvelcdmd 
 |-  ( ( ph /\ x e. ( ( S ` 0 ) [,] ( S ` M ) ) ) -> ( F ` x ) e. CC )
123 102 100 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) e. RR )
124 112 111 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR )
125 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
126 125 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
127 eqeq1 
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
128 127 rexbidv 
 |-  ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
129 oveq1 
 |-  ( z = y -> ( z + T ) = ( y + T ) )
130 129 eqeq2d 
 |-  ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
131 130 cbvrexvw 
 |-  ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) )
132 128 131 bitrdi 
 |-  ( w = x -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) <-> E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) ) )
133 132 cbvrabv 
 |-  { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = { x e. CC | E. y e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( y + T ) }
134 fdm 
 |-  ( F : RR --> CC -> dom F = RR )
135 9 134 syl 
 |-  ( ph -> dom F = RR )
136 135 feq2d 
 |-  ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
137 9 136 mpbird 
 |-  ( ph -> F : dom F --> CC )
138 137 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : dom F --> CC )
139 elioore 
 |-  ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> z e. RR )
140 139 adantl 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
141 78 adantr 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
142 140 141 readdcld 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
143 142 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) e. RR )
144 143 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> ( z + T ) e. RR )
145 simp3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w = ( z + T ) )
146 135 3ad2ant1 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
147 146 3adant1r 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> dom F = RR )
148 144 145 147 3eltr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ w = ( z + T ) ) -> w e. dom F )
149 148 3exp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
150 149 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. CC ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( w = ( z + T ) -> w e. dom F ) ) )
151 150 rexlimdv 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. CC ) -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
152 151 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. w e. CC ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
153 rabss 
 |-  ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F <-> A. w e. CC ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) -> w e. dom F ) )
154 152 153 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } C_ dom F )
155 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
156 1 rexrd 
 |-  ( ph -> A e. RR* )
157 156 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
158 2 rexrd 
 |-  ( ph -> B e. RR* )
159 158 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
160 3 4 6 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
161 160 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
162 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
163 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
164 163 sseli 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
165 164 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
166 157 159 161 162 165 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> x e. ( A [,] B ) )
167 155 166 7 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
168 126 98 133 138 154 167 10 cncfperiod 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) e. ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) )
169 128 elrab 
 |-  ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> ( x e. CC /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) )
170 169 simprbi 
 |-  ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
171 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
172 nfv 
 |-  F/ z ( ph /\ i e. ( 0 ..^ M ) )
173 nfre1 
 |-  F/ z E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T )
174 172 173 nfan 
 |-  F/ z ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
175 nfv 
 |-  F/ z ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) )
176 simp3 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
177 142 3adant3 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) e. RR )
178 176 177 eqeltrd 
 |-  ( ( ph /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
179 178 3adant1r 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x e. RR )
180 50 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
181 139 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. RR )
182 78 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> T e. RR )
183 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
184 50 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
185 184 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
186 53 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
187 186 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
188 elioo2 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) ) )
189 185 187 188 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) ) )
190 183 189 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z e. RR /\ ( Q ` i ) < z /\ z < ( Q ` ( i + 1 ) ) ) )
191 190 simp2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < z )
192 180 181 182 191 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
193 192 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( ( Q ` i ) + T ) < ( z + T ) )
194 102 3ad2ant1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) = ( ( Q ` i ) + T ) )
195 simp3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x = ( z + T ) )
196 193 194 195 3brtr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` i ) < x )
197 53 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
198 190 simp3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z < ( Q ` ( i + 1 ) ) )
199 181 197 182 198 ltadd1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
200 199 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( z + T ) < ( ( Q ` ( i + 1 ) ) + T ) )
201 112 3ad2ant1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( S ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) + T ) )
202 200 195 201 3brtr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> x < ( S ` ( i + 1 ) ) )
203 179 196 202 3jca 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( z + T ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
204 203 3exp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) ) )
205 204 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) ) )
206 174 175 205 rexlimd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
207 171 206 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
208 123 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` i ) e. RR* )
209 208 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` i ) e. RR* )
210 124 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( i + 1 ) ) e. RR* )
211 210 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( S ` ( i + 1 ) ) e. RR* )
212 elioo2 
 |-  ( ( ( S ` i ) e. RR* /\ ( S ` ( i + 1 ) ) e. RR* ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
213 209 211 212 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
214 207 213 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
215 170 214 sylan2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
216 elioore 
 |-  ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. RR )
217 216 recnd 
 |-  ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. CC )
218 217 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
219 184 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
220 186 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
221 216 adantl 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
222 78 adantr 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
223 221 222 resubcld 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
224 223 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
225 102 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) - T ) = ( ( ( Q ` i ) + T ) - T ) )
226 50 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
227 98 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. CC )
228 226 227 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + T ) - T ) = ( Q ` i ) )
229 225 228 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
230 229 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
231 123 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
232 216 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. RR )
233 78 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. RR )
234 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
235 208 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR* )
236 210 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
237 235 236 212 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) <-> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) ) )
238 234 237 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x e. RR /\ ( S ` i ) < x /\ x < ( S ` ( i + 1 ) ) ) )
239 238 simp2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) < x )
240 231 232 233 239 ltsub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) - T ) < ( x - T ) )
241 230 240 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( x - T ) )
242 124 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
243 238 simp3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x < ( S ` ( i + 1 ) ) )
244 232 242 233 243 ltsub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( ( S ` ( i + 1 ) ) - T ) )
245 112 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
246 53 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
247 246 227 pncand 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
248 245 247 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
249 248 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
250 244 249 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
251 219 220 224 241 250 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
252 221 recnd 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. CC )
253 222 recnd 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> T e. CC )
254 252 253 npcand 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) + T ) = x )
255 254 eqcomd 
 |-  ( ( ph /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
256 255 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
257 oveq1 
 |-  ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
258 257 eqeq2d 
 |-  ( z = ( x - T ) -> ( x = ( z + T ) <-> x = ( ( x - T ) + T ) ) )
259 258 rspcev 
 |-  ( ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
260 251 256 259 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) x = ( z + T ) )
261 218 260 169 sylanbrc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } )
262 215 261 impbida 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } <-> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
263 262 eqrdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
264 263 reseq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) = ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) )
265 9 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> CC )
266 ioossre 
 |-  ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR
267 266 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ RR )
268 265 267 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
269 264 268 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) = ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
270 263 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } -cn-> CC ) = ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
271 168 269 270 3eltr3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. ( ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -cn-> CC ) )
272 57 135 sseqtrrid 
 |-  ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
273 272 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
274 eqid 
 |-  { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } = { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) }
275 simpll 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
276 156 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A e. RR* )
277 158 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> B e. RR* )
278 160 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
279 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
280 163 183 sselid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
281 276 277 278 279 280 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> z e. ( A [,] B ) )
282 eleq1 
 |-  ( x = z -> ( x e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
283 282 anbi2d 
 |-  ( x = z -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
284 oveq1 
 |-  ( x = z -> ( x + T ) = ( z + T ) )
285 284 fveq2d 
 |-  ( x = z -> ( F ` ( x + T ) ) = ( F ` ( z + T ) ) )
286 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
287 285 286 eqeq12d 
 |-  ( x = z -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( z + T ) ) = ( F ` z ) ) )
288 283 287 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) ) ) )
289 288 7 chvarvv 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
290 275 281 289 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( z + T ) ) = ( F ` z ) )
291 138 126 273 227 274 154 290 12 limcperiod 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) limCC ( ( Q ` ( i + 1 ) ) + T ) ) )
292 112 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
293 269 292 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) limCC ( ( Q ` ( i + 1 ) ) + T ) ) = ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( S ` ( i + 1 ) ) ) )
294 291 293 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( S ` ( i + 1 ) ) ) )
295 138 126 273 227 274 154 290 11 limcperiod 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) limCC ( ( Q ` i ) + T ) ) )
296 102 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
297 269 296 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` { w e. CC | E. z e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) w = ( z + T ) } ) limCC ( ( Q ` i ) + T ) ) = ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( S ` i ) ) )
298 295 297 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) limCC ( S ` i ) ) )
299 123 124 271 294 298 iblcncfioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
300 9 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> F : RR --> CC )
301 123 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR )
302 124 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
303 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
304 eliccre 
 |-  ( ( ( S ` i ) e. RR /\ ( S ` ( i + 1 ) ) e. RR /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
305 301 302 303 304 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. RR )
306 300 305 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` x ) e. CC )
307 123 124 299 306 ibliooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> ( F ` x ) ) e. L^1 )
308 26 31 97 113 122 307 itgspltprt 
 |-  ( ph -> S. ( ( S ` 0 ) [,] ( S ` M ) ) ( F ` x ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x )
309 iftrue 
 |-  ( x = ( S ` i ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
310 309 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
311 iftrue 
 |-  ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = R )
312 iftrue 
 |-  ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = R )
313 311 312 eqtr4d 
 |-  ( x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
314 313 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ x = ( Q ` i ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
315 iffalse 
 |-  ( -. x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
316 315 adantr 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
317 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
318 317 adantl 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = L )
319 iffalse 
 |-  ( -. x = ( Q ` i ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
320 319 adantr 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
321 iftrue 
 |-  ( x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
322 321 adantl 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = L )
323 320 322 eqtr2d 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> L = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
324 316 318 323 3eqtrd 
 |-  ( ( -. x = ( Q ` i ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
325 324 adantll 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
326 315 ad2antlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) )
327 iffalse 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
328 327 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) = ( F ` x ) )
329 319 ad2antlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) )
330 iffalse 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
331 330 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) )
332 184 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
333 186 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
334 65 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. RR )
335 50 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR )
336 65 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. RR )
337 184 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) e. RR* )
338 186 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
339 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
340 iccgelb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ x )
341 337 338 339 340 syl3anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) <_ x )
342 neqne 
 |-  ( -. x = ( Q ` i ) -> x =/= ( Q ` i ) )
343 342 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> x =/= ( Q ` i ) )
344 335 336 341 343 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> ( Q ` i ) < x )
345 344 adantr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < x )
346 53 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
347 184 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
348 186 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
349 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
350 iccleub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
351 347 348 349 350 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
352 351 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x <_ ( Q ` ( i + 1 ) ) )
353 neqne 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> x =/= ( Q ` ( i + 1 ) ) )
354 353 necomd 
 |-  ( -. x = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= x )
355 354 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= x )
356 334 346 352 355 leneltd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x < ( Q ` ( i + 1 ) ) )
357 332 333 334 345 356 eliood 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
358 fvres 
 |-  ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
359 357 358 syl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
360 329 331 359 3eqtrrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> ( F ` x ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
361 326 328 360 3eqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) /\ -. x = ( Q ` ( i + 1 ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
362 325 361 pm2.61dan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) /\ -. x = ( Q ` i ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
363 314 362 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) = if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
364 363 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( F ` x ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) )
365 13 364 eqtrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) )
366 eqeq1 
 |-  ( x = w -> ( x = ( Q ` i ) <-> w = ( Q ` i ) ) )
367 eqeq1 
 |-  ( x = w -> ( x = ( Q ` ( i + 1 ) ) <-> w = ( Q ` ( i + 1 ) ) ) )
368 fveq2 
 |-  ( x = w -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) )
369 367 368 ifbieq2d 
 |-  ( x = w -> if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) = if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) )
370 366 369 ifbieq2d 
 |-  ( x = w -> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) )
371 370 cbvmptv 
 |-  ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) )
372 365 371 eqtrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) ) )
373 372 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> G = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) ) )
374 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) /\ w = ( x - T ) ) -> w = ( x - T ) )
375 oveq1 
 |-  ( x = ( S ` i ) -> ( x - T ) = ( ( S ` i ) - T ) )
376 375 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) /\ w = ( x - T ) ) -> ( x - T ) = ( ( S ` i ) - T ) )
377 229 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) - T ) = ( Q ` i ) )
378 377 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) /\ w = ( x - T ) ) -> ( ( S ` i ) - T ) = ( Q ` i ) )
379 374 376 378 3eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) /\ w = ( x - T ) ) -> w = ( Q ` i ) )
380 379 iftrued 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) /\ w = ( x - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = R )
381 375 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> ( x - T ) = ( ( S ` i ) - T ) )
382 50 53 40 ltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
383 lbicc2 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
384 184 186 382 383 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
385 377 384 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
386 385 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> ( ( S ` i ) - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
387 381 386 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> ( x - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
388 limccl 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) C_ CC
389 388 11 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. CC )
390 389 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> R e. CC )
391 373 380 387 390 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> ( G ` ( x - T ) ) = R )
392 310 391 eqtr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = ( G ` ( x - T ) ) )
393 392 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = ( G ` ( x - T ) ) )
394 iffalse 
 |-  ( -. x = ( S ` i ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) )
395 394 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) )
396 372 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> G = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) ) )
397 eqeq1 
 |-  ( w = ( ( S ` ( i + 1 ) ) - T ) -> ( w = ( Q ` i ) <-> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) ) )
398 eqeq1 
 |-  ( w = ( ( S ` ( i + 1 ) ) - T ) -> ( w = ( Q ` ( i + 1 ) ) <-> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) ) )
399 fveq2 
 |-  ( w = ( ( S ` ( i + 1 ) ) - T ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) )
400 398 399 ifbieq2d 
 |-  ( w = ( ( S ` ( i + 1 ) ) - T ) -> if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) = if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) )
401 397 400 ifbieq2d 
 |-  ( w = ( ( S ` ( i + 1 ) ) - T ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) , R , if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) ) )
402 401 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w = ( ( S ` ( i + 1 ) ) - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) , R , if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) ) )
403 eqeq1 
 |-  ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) -> ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) <-> ( Q ` ( i + 1 ) ) = ( Q ` i ) ) )
404 iftrue 
 |-  ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) -> if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) = L )
405 403 404 ifbieq2d 
 |-  ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) -> if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) , R , if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) ) = if ( ( Q ` ( i + 1 ) ) = ( Q ` i ) , R , L ) )
406 248 405 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) , R , if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) ) = if ( ( Q ` ( i + 1 ) ) = ( Q ` i ) , R , L ) )
407 406 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w = ( ( S ` ( i + 1 ) ) - T ) ) -> if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` i ) , R , if ( ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( S ` ( i + 1 ) ) - T ) ) ) ) = if ( ( Q ` ( i + 1 ) ) = ( Q ` i ) , R , L ) )
408 50 40 gtned 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) =/= ( Q ` i ) )
409 408 neneqd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. ( Q ` ( i + 1 ) ) = ( Q ` i ) )
410 409 iffalsed 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> if ( ( Q ` ( i + 1 ) ) = ( Q ` i ) , R , L ) = L )
411 410 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w = ( ( S ` ( i + 1 ) ) - T ) ) -> if ( ( Q ` ( i + 1 ) ) = ( Q ` i ) , R , L ) = L )
412 402 407 411 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w = ( ( S ` ( i + 1 ) ) - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = L )
413 412 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) /\ w = ( ( S ` ( i + 1 ) ) - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = L )
414 ubicc2 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
415 184 186 382 414 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
416 248 415 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` ( i + 1 ) ) - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
417 416 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
418 limccl 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) C_ CC
419 418 12 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. CC )
420 419 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> L e. CC )
421 396 413 417 420 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> ( G ` ( ( S ` ( i + 1 ) ) - T ) ) = L )
422 oveq1 
 |-  ( x = ( S ` ( i + 1 ) ) -> ( x - T ) = ( ( S ` ( i + 1 ) ) - T ) )
423 422 fveq2d 
 |-  ( x = ( S ` ( i + 1 ) ) -> ( G ` ( x - T ) ) = ( G ` ( ( S ` ( i + 1 ) ) - T ) ) )
424 423 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> ( G ` ( x - T ) ) = ( G ` ( ( S ` ( i + 1 ) ) - T ) ) )
425 iftrue 
 |-  ( x = ( S ` ( i + 1 ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = L )
426 425 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = L )
427 421 424 426 3eqtr4rd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( G ` ( x - T ) ) )
428 427 ad4ant14 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( G ` ( x - T ) ) )
429 iffalse 
 |-  ( -. x = ( S ` ( i + 1 ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) )
430 429 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) )
431 372 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> G = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) ) )
432 431 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> G = ( w e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) ) )
433 eqeq1 
 |-  ( w = ( x - T ) -> ( w = ( Q ` i ) <-> ( x - T ) = ( Q ` i ) ) )
434 eqeq1 
 |-  ( w = ( x - T ) -> ( w = ( Q ` ( i + 1 ) ) <-> ( x - T ) = ( Q ` ( i + 1 ) ) ) )
435 fveq2 
 |-  ( w = ( x - T ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
436 434 435 ifbieq2d 
 |-  ( w = ( x - T ) -> if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) = if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
437 433 436 ifbieq2d 
 |-  ( w = ( x - T ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = if ( ( x - T ) = ( Q ` i ) , R , if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) ) )
438 437 adantl 
 |-  ( ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) /\ w = ( x - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = if ( ( x - T ) = ( Q ` i ) , R , if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) ) )
439 305 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x e. CC )
440 227 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> T e. CC )
441 439 440 npcand 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) + T ) = x )
442 441 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x = ( ( x - T ) + T ) )
443 442 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` i ) ) -> x = ( ( x - T ) + T ) )
444 oveq1 
 |-  ( ( x - T ) = ( Q ` i ) -> ( ( x - T ) + T ) = ( ( Q ` i ) + T ) )
445 444 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` i ) ) -> ( ( x - T ) + T ) = ( ( Q ` i ) + T ) )
446 296 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` i ) ) -> ( ( Q ` i ) + T ) = ( S ` i ) )
447 443 445 446 3eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` i ) ) -> x = ( S ` i ) )
448 447 stoic1a 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> -. ( x - T ) = ( Q ` i ) )
449 448 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( ( x - T ) = ( Q ` i ) , R , if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) ) = if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
450 449 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) /\ w = ( x - T ) ) -> if ( ( x - T ) = ( Q ` i ) , R , if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) ) = if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) )
451 442 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` ( i + 1 ) ) ) -> x = ( ( x - T ) + T ) )
452 oveq1 
 |-  ( ( x - T ) = ( Q ` ( i + 1 ) ) -> ( ( x - T ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
453 452 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` ( i + 1 ) ) ) -> ( ( x - T ) + T ) = ( ( Q ` ( i + 1 ) ) + T ) )
454 292 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` ( i + 1 ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) = ( S ` ( i + 1 ) ) )
455 451 453 454 3eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ ( x - T ) = ( Q ` ( i + 1 ) ) ) -> x = ( S ` ( i + 1 ) ) )
456 455 stoic1a 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> -. ( x - T ) = ( Q ` ( i + 1 ) ) )
457 456 iffalsed 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
458 457 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
459 458 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) /\ w = ( x - T ) ) -> if ( ( x - T ) = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
460 438 450 459 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) /\ w = ( x - T ) ) -> if ( w = ( Q ` i ) , R , if ( w = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` w ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
461 50 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
462 53 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
463 78 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> T e. RR )
464 305 463 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. RR )
465 229 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( ( S ` i ) - T ) )
466 208 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) e. RR* )
467 210 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
468 iccgelb 
 |-  ( ( ( S ` i ) e. RR* /\ ( S ` ( i + 1 ) ) e. RR* /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) <_ x )
469 466 467 303 468 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( S ` i ) <_ x )
470 301 305 463 469 lesub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( S ` i ) - T ) <_ ( x - T ) )
471 465 470 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( x - T ) )
472 iccleub 
 |-  ( ( ( S ` i ) e. RR* /\ ( S ` ( i + 1 ) ) e. RR* /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x <_ ( S ` ( i + 1 ) ) )
473 466 467 303 472 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> x <_ ( S ` ( i + 1 ) ) )
474 305 302 463 473 lesub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) <_ ( ( S ` ( i + 1 ) ) - T ) )
475 248 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( S ` ( i + 1 ) ) - T ) = ( Q ` ( i + 1 ) ) )
476 474 475 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) <_ ( Q ` ( i + 1 ) ) )
477 461 462 464 471 476 eliccd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
478 477 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
479 138 273 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
480 479 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
481 184 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
482 186 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
483 305 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> x e. RR )
484 98 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> T e. RR )
485 483 484 resubcld 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. RR )
486 50 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( Q ` i ) e. RR )
487 464 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( x - T ) e. RR )
488 471 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( Q ` i ) <_ ( x - T ) )
489 448 neqned 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( x - T ) =/= ( Q ` i ) )
490 486 487 488 489 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( Q ` i ) < ( x - T ) )
491 490 adantr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( Q ` i ) < ( x - T ) )
492 464 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. RR )
493 53 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
494 476 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) <_ ( Q ` ( i + 1 ) ) )
495 eqcom 
 |-  ( ( x - T ) = ( Q ` ( i + 1 ) ) <-> ( Q ` ( i + 1 ) ) = ( x - T ) )
496 455 ex 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( x - T ) = ( Q ` ( i + 1 ) ) -> x = ( S ` ( i + 1 ) ) ) )
497 495 496 biimtrrid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( Q ` ( i + 1 ) ) = ( x - T ) -> x = ( S ` ( i + 1 ) ) ) )
498 497 con3dimp 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> -. ( Q ` ( i + 1 ) ) = ( x - T ) )
499 498 neqned 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= ( x - T ) )
500 492 493 494 499 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
501 500 adantlr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) < ( Q ` ( i + 1 ) ) )
502 481 482 485 491 501 eliood 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
503 480 502 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) e. CC )
504 432 460 478 503 fvmptd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( G ` ( x - T ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) )
505 fvres 
 |-  ( ( x - T ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
506 502 505 syl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( x - T ) ) = ( F ` ( x - T ) ) )
507 504 506 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( G ` ( x - T ) ) = ( F ` ( x - T ) ) )
508 466 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( S ` i ) e. RR* )
509 467 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( S ` ( i + 1 ) ) e. RR* )
510 123 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( S ` i ) e. RR )
511 305 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> x e. RR )
512 469 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( S ` i ) <_ x )
513 neqne 
 |-  ( -. x = ( S ` i ) -> x =/= ( S ` i ) )
514 513 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> x =/= ( S ` i ) )
515 510 511 512 514 leneltd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> ( S ` i ) < x )
516 515 adantr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( S ` i ) < x )
517 302 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( S ` ( i + 1 ) ) e. RR )
518 473 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> x <_ ( S ` ( i + 1 ) ) )
519 neqne 
 |-  ( -. x = ( S ` ( i + 1 ) ) -> x =/= ( S ` ( i + 1 ) ) )
520 519 necomd 
 |-  ( -. x = ( S ` ( i + 1 ) ) -> ( S ` ( i + 1 ) ) =/= x )
521 520 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( S ` ( i + 1 ) ) =/= x )
522 483 517 518 521 leneltd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> x < ( S ` ( i + 1 ) ) )
523 508 509 483 516 522 eliood 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) )
524 fvres 
 |-  ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
525 523 524 syl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
526 441 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` x ) )
527 526 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( F ` x ) = ( F ` ( ( x - T ) + T ) ) )
528 527 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( F ` x ) = ( F ` ( ( x - T ) + T ) ) )
529 439 440 subcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. CC )
530 elex 
 |-  ( ( x - T ) e. CC -> ( x - T ) e. _V )
531 529 530 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. _V )
532 531 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. _V )
533 simp-4l 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ph )
534 156 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. RR* )
535 158 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> B e. RR* )
536 160 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
537 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
538 534 535 536 537 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
539 538 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( A [,] B ) )
540 539 477 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( x - T ) e. ( A [,] B ) )
541 540 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( x - T ) e. ( A [,] B ) )
542 533 541 jca 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ph /\ ( x - T ) e. ( A [,] B ) ) )
543 eleq1 
 |-  ( y = ( x - T ) -> ( y e. ( A [,] B ) <-> ( x - T ) e. ( A [,] B ) ) )
544 543 anbi2d 
 |-  ( y = ( x - T ) -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ ( x - T ) e. ( A [,] B ) ) ) )
545 oveq1 
 |-  ( y = ( x - T ) -> ( y + T ) = ( ( x - T ) + T ) )
546 545 fveq2d 
 |-  ( y = ( x - T ) -> ( F ` ( y + T ) ) = ( F ` ( ( x - T ) + T ) ) )
547 fveq2 
 |-  ( y = ( x - T ) -> ( F ` y ) = ( F ` ( x - T ) ) )
548 546 547 eqeq12d 
 |-  ( y = ( x - T ) -> ( ( F ` ( y + T ) ) = ( F ` y ) <-> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
549 544 548 imbi12d 
 |-  ( y = ( x - T ) -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) <-> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) ) )
550 eleq1 
 |-  ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
551 550 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. ( A [,] B ) ) <-> ( ph /\ y e. ( A [,] B ) ) ) )
552 oveq1 
 |-  ( x = y -> ( x + T ) = ( y + T ) )
553 552 fveq2d 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
554 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
555 553 554 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
556 551 555 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
557 556 7 chvarvv 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) = ( F ` y ) )
558 549 557 vtoclg 
 |-  ( ( x - T ) e. _V -> ( ( ph /\ ( x - T ) e. ( A [,] B ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) ) )
559 532 542 558 sylc 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( F ` ( ( x - T ) + T ) ) = ( F ` ( x - T ) ) )
560 525 528 559 3eqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) = ( F ` ( x - T ) ) )
561 507 560 eqtr4d 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( G ` ( x - T ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) )
562 430 561 eqtr4d 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( G ` ( x - T ) ) )
563 428 562 pm2.61dan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( G ` ( x - T ) ) )
564 395 563 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = ( G ` ( x - T ) ) )
565 393 564 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = ( G ` ( x - T ) ) )
566 310 390 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC )
567 566 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC )
568 426 420 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) e. CC )
569 568 ad4ant14 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) e. CC )
570 265 267 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) : ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) --> CC )
571 570 ad3antrrr 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) : ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) --> CC )
572 571 523 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) e. CC )
573 430 572 eqeltrd 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) /\ -. x = ( S ` ( i + 1 ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) e. CC )
574 569 573 pm2.61dan 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) e. CC )
575 395 574 eqeltrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) /\ -. x = ( S ` i ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC )
576 567 575 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC )
577 eqid 
 |-  ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) )
578 577 fvmpt2 
 |-  ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) /\ if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC ) -> ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) = if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) )
579 303 576 578 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) = if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) )
580 nfv 
 |-  F/ x ( ph /\ i e. ( 0 ..^ M ) )
581 eqid 
 |-  ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
582 580 581 50 53 10 12 11 cncfiooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
583 365 582 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
584 cncff 
 |-  ( G e. ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> G : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
585 583 584 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
586 585 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> G : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
587 586 477 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( G ` ( x - T ) ) e. CC )
588 14 fvmpt2 
 |-  ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) /\ ( G ` ( x - T ) ) e. CC ) -> ( H ` x ) = ( G ` ( x - T ) ) )
589 303 587 588 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( H ` x ) = ( G ` ( x - T ) ) )
590 565 579 589 3eqtr4rd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( H ` x ) = ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) )
591 590 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( H ` x ) _d x = S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) _d x )
592 ioossicc 
 |-  ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) C_ ( ( S ` i ) [,] ( S ` ( i + 1 ) ) )
593 592 sseli 
 |-  ( x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
594 593 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
595 593 576 sylan2 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) e. CC )
596 594 595 578 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) = if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) )
597 231 239 gtned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x =/= ( S ` i ) )
598 597 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> -. x = ( S ` i ) )
599 598 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) = if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) )
600 232 243 ltned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> x =/= ( S ` ( i + 1 ) ) )
601 600 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> -. x = ( S ` ( i + 1 ) ) )
602 601 iffalsed 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) )
603 524 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) = ( F ` x ) )
604 602 603 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) = ( F ` x ) )
605 596 599 604 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) = ( F ` x ) )
606 605 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) _d x = S. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ( F ` x ) _d x )
607 579 576 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) e. CC )
608 123 124 607 itgioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) _d x = S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) _d x )
609 123 124 306 itgioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ( F ` x ) _d x = S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x )
610 606 608 609 3eqtr3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( ( x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) |-> if ( x = ( S ` i ) , R , if ( x = ( S ` ( i + 1 ) ) , L , ( ( F |` ( ( S ` i ) (,) ( S ` ( i + 1 ) ) ) ) ` x ) ) ) ) ` x ) _d x = S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x )
611 591 610 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x = S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( H ` x ) _d x )
612 102 112 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) = ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) )
613 612 itgeq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( H ` x ) _d x = S. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ( H ` x ) _d x )
614 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) )
615 612 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) = ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
616 615 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) = ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
617 614 616 eleqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) )
618 585 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> G : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
619 50 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) e. RR )
620 53 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
621 100 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR )
622 111 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR )
623 eliccre 
 |-  ( ( ( ( Q ` i ) + T ) e. RR /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
624 621 622 614 623 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x e. RR )
625 78 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> T e. RR )
626 624 625 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. RR )
627 228 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
628 627 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) = ( ( ( Q ` i ) + T ) - T ) )
629 621 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) e. RR* )
630 622 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` ( i + 1 ) ) + T ) e. RR* )
631 iccgelb 
 |-  ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) <_ x )
632 629 630 614 631 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( Q ` i ) + T ) <_ x )
633 621 624 625 632 lesub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` i ) + T ) - T ) <_ ( x - T ) )
634 628 633 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( Q ` i ) <_ ( x - T ) )
635 iccleub 
 |-  ( ( ( ( Q ` i ) + T ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + T ) e. RR* /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x <_ ( ( Q ` ( i + 1 ) ) + T ) )
636 629 630 614 635 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> x <_ ( ( Q ` ( i + 1 ) ) + T ) )
637 624 622 625 636 lesub1dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) <_ ( ( ( Q ` ( i + 1 ) ) + T ) - T ) )
638 247 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( ( Q ` ( i + 1 ) ) + T ) - T ) = ( Q ` ( i + 1 ) ) )
639 637 638 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) <_ ( Q ` ( i + 1 ) ) )
640 619 620 626 634 639 eliccd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( x - T ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
641 618 640 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( G ` ( x - T ) ) e. CC )
642 617 641 588 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( H ` x ) = ( G ` ( x - T ) ) )
643 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) = ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) )
644 oveq1 
 |-  ( y = x -> ( y - T ) = ( x - T ) )
645 644 fveq2d 
 |-  ( y = x -> ( G ` ( y - T ) ) = ( G ` ( x - T ) ) )
646 645 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) /\ y = x ) -> ( G ` ( y - T ) ) = ( G ` ( x - T ) ) )
647 643 646 614 641 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) ` x ) = ( G ` ( x - T ) ) )
648 642 647 eqtr4d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ) -> ( H ` x ) = ( ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) ` x ) )
649 648 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ( H ` x ) _d x = S. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ( ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) ` x ) _d x )
650 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> T e. RR+ )
651 645 cbvmptv 
 |-  ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) = ( x e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( x - T ) ) )
652 50 53 382 583 650 651 itgiccshift 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) ( ( y e. ( ( ( Q ` i ) + T ) [,] ( ( Q ` ( i + 1 ) ) + T ) ) |-> ( G ` ( y - T ) ) ) ` x ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( G ` x ) _d x )
653 613 649 652 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( H ` x ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( G ` x ) _d x )
654 135 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom F = RR )
655 64 654 sseqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ dom F )
656 50 53 138 10 655 11 12 13 itgioocnicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G e. L^1 /\ S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( G ` x ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x ) )
657 656 simprd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( G ` x ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x )
658 611 653 657 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x )
659 658 sumeq2dv 
 |-  ( ph -> sum_ i e. ( 0 ..^ M ) S. ( ( S ` i ) [,] ( S ` ( i + 1 ) ) ) ( F ` x ) _d x = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x )
660 93 308 659 3eqtrrd 
 |-  ( ph -> sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` x ) _d x = S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x )
661 25 68 660 3eqtrrd 
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )