Metamath Proof Explorer

Theorem fourierdlem90

Description: Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem90.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 ) ) ) } )
fourierdlem90.t 
|- T = ( B - A )
fourierdlem90.m 
|- ( ph -> M e. NN )
fourierdlem90.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem90.f 
|- ( ph -> F : RR --> CC )
fourierdlem90.6 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem90.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem90.c 
|- ( ph -> C e. RR )
fourierdlem90.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem90.o 
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem90.h 
|- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
fourierdlem90.n 
|- N = ( ( # ` H ) - 1 )
fourierdlem90.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
fourierdlem90.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
fourierdlem90.J 
|- L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
fourierdlem90.17 
|- ( ph -> J e. ( 0 ..^ N ) )
fourierdlem90.u 
|- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
fourierdlem90.g 
|- G = ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
fourierdlem90.r 
|- R = ( y e. ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) |-> ( G ` ( y - U ) ) )
fourierdlem90.i 
|- I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
Assertion fourierdlem90 
|- ( ph -> ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) e. ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fourierdlem90.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 ) ) ) } )
2 fourierdlem90.t 
 |-  T = ( B - A )
3 fourierdlem90.m 
 |-  ( ph -> M e. NN )
4 fourierdlem90.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem90.f 
 |-  ( ph -> F : RR --> CC )
6 fourierdlem90.6 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7 fourierdlem90.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
8 fourierdlem90.c 
 |-  ( ph -> C e. RR )
9 fourierdlem90.d 
 |-  ( ph -> D e. ( C (,) +oo ) )
10 fourierdlem90.o 
 |-  O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
11 fourierdlem90.h 
 |-  H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
12 fourierdlem90.n 
 |-  N = ( ( # ` H ) - 1 )
13 fourierdlem90.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
14 fourierdlem90.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
15 fourierdlem90.J 
 |-  L = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
16 fourierdlem90.17 
 |-  ( ph -> J e. ( 0 ..^ N ) )
17 fourierdlem90.u 
 |-  U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
18 fourierdlem90.g 
 |-  G = ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
19 fourierdlem90.r 
 |-  R = ( y e. ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) |-> ( G ` ( y - U ) ) )
20 fourierdlem90.i 
 |-  I = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) )
21 1 3 4 fourierdlem11 
 |-  ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
22 21 simp1d 
 |-  ( ph -> A e. RR )
23 21 simp2d 
 |-  ( ph -> B e. RR )
24 22 23 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
25 21 simp3d 
 |-  ( ph -> A < B )
26 22 23 25 15 fourierdlem17 
 |-  ( ph -> L : ( A (,] B ) --> ( A [,] B ) )
27 22 23 25 2 14 fourierdlem4 
 |-  ( ph -> E : RR --> ( A (,] B ) )
28 elioore 
 |-  ( D e. ( C (,) +oo ) -> D e. RR )
29 9 28 syl 
 |-  ( ph -> D e. RR )
30 elioo4g 
 |-  ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
31 9 30 sylib 
 |-  ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
32 31 simprd 
 |-  ( ph -> ( C < D /\ D < +oo ) )
33 32 simpld 
 |-  ( ph -> C < D )
34 2 1 3 4 8 29 33 10 11 12 13 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) )
35 34 simpld 
 |-  ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
36 35 simprd 
 |-  ( ph -> S e. ( O ` N ) )
37 35 simpld 
 |-  ( ph -> N e. NN )
38 10 fourierdlem2 
 |-  ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
39 37 38 syl 
 |-  ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) )
40 36 39 mpbid 
 |-  ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
41 40 simpld 
 |-  ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
42 elmapi 
 |-  ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
43 41 42 syl 
 |-  ( ph -> S : ( 0 ... N ) --> RR )
44 elfzofz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) )
45 16 44 syl 
 |-  ( ph -> J e. ( 0 ... N ) )
46 43 45 ffvelcdmd 
 |-  ( ph -> ( S ` J ) e. RR )
47 27 46 ffvelcdmd 
 |-  ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
48 26 47 ffvelcdmd 
 |-  ( ph -> ( L ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
49 24 48 sseldd 
 |-  ( ph -> ( L ` ( E ` ( S ` J ) ) ) e. RR )
50 22 rexrd 
 |-  ( ph -> A e. RR* )
51 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
52 50 23 51 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
53 fzofzp1 
 |-  ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
54 16 53 syl 
 |-  ( ph -> ( J + 1 ) e. ( 0 ... N ) )
55 43 54 ffvelcdmd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR )
56 27 55 ffvelcdmd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
57 52 56 sseldd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
58 eqid 
 |-  ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) )
59 55 57 resubcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
60 17 59 eqeltrid 
 |-  ( ph -> U e. RR )
61 eqid 
 |-  ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) )
62 eleq1 
 |-  ( j = J -> ( j e. ( 0 ..^ N ) <-> J e. ( 0 ..^ N ) ) )
63 62 anbi2d 
 |-  ( j = J -> ( ( ph /\ j e. ( 0 ..^ N ) ) <-> ( ph /\ J e. ( 0 ..^ N ) ) ) )
64 fveq2 
 |-  ( j = J -> ( S ` j ) = ( S ` J ) )
65 64 fveq2d 
 |-  ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
66 65 fveq2d 
 |-  ( j = J -> ( L ` ( E ` ( S ` j ) ) ) = ( L ` ( E ` ( S ` J ) ) ) )
67 oveq1 
 |-  ( j = J -> ( j + 1 ) = ( J + 1 ) )
68 67 fveq2d 
 |-  ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
69 68 fveq2d 
 |-  ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
70 66 69 oveq12d 
 |-  ( j = J -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
71 64 fveq2d 
 |-  ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
72 71 fveq2d 
 |-  ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
73 71 oveq1d 
 |-  ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
74 73 fveq2d 
 |-  ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
75 72 74 oveq12d 
 |-  ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
76 70 75 sseq12d 
 |-  ( j = J -> ( ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) <-> ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
77 63 76 imbi12d 
 |-  ( j = J -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) ) <-> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
78 2 oveq2i 
 |-  ( k x. T ) = ( k x. ( B - A ) )
79 78 oveq2i 
 |-  ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
80 79 eleq1i 
 |-  ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
81 80 rexbii 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
82 81 a1i 
 |-  ( y e. ( C [,] D ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q ) )
83 82 rabbiia 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q }
84 83 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
85 11 84 eqtri 
 |-  H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
86 id 
 |-  ( y = x -> y = x )
87 2 eqcomi 
 |-  ( B - A ) = T
88 87 oveq2i 
 |-  ( k x. ( B - A ) ) = ( k x. T )
89 88 a1i 
 |-  ( y = x -> ( k x. ( B - A ) ) = ( k x. T ) )
90 86 89 oveq12d 
 |-  ( y = x -> ( y + ( k x. ( B - A ) ) ) = ( x + ( k x. T ) ) )
91 90 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
92 91 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
93 92 cbvrabv 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } = { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
94 93 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
95 85 94 eqtri 
 |-  H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
96 eqid 
 |-  ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) ) = ( ( S ` j ) + if ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) < ( ( Q ` 1 ) - A ) , ( ( ( S ` ( j + 1 ) ) - ( S ` j ) ) / 2 ) , ( ( ( Q ` 1 ) - A ) / 2 ) ) )
97 2 1 3 4 8 29 33 10 95 12 13 14 15 96 20 fourierdlem79 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
98 77 97 vtoclg 
 |-  ( J e. ( 0 ..^ N ) -> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
99 98 anabsi7 
 |-  ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
100 16 99 mpdan 
 |-  ( ph -> ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
101 100 resabs1d 
 |-  ( ph -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) )
102 101 eqcomd 
 |-  ( ph -> ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) )
103 1 3 4 2 14 15 20 fourierdlem37 
 |-  ( ph -> ( I : RR --> ( 0 ..^ M ) /\ ( x e. RR -> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( L ` ( E ` x ) ) } ) ) )
104 103 simpld 
 |-  ( ph -> I : RR --> ( 0 ..^ M ) )
105 104 46 ffvelcdmd 
 |-  ( ph -> ( I ` ( S ` J ) ) e. ( 0 ..^ M ) )
106 105 ancli 
 |-  ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) )
107 eleq1 
 |-  ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0 ..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) )
108 107 anbi2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) ) )
109 fveq2 
 |-  ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
110 oveq1 
 |-  ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
111 110 fveq2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
112 109 111 oveq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
113 112 reseq2d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
114 112 oveq1d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
115 113 114 eleq12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) )
116 108 115 imbi12d 
 |-  ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) ) )
117 116 7 vtoclg 
 |-  ( ( I ` ( S ` J ) ) e. ( 0 ..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) )
118 105 106 117 sylc 
 |-  ( ph -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
119 rescncf 
 |-  ( ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -cn-> CC ) ) )
120 100 118 119 sylc 
 |-  ( ph -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -cn-> CC ) )
121 102 120 eqeltrd 
 |-  ( ph -> ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -cn-> CC ) )
122 18 121 eqeltrid 
 |-  ( ph -> G e. ( ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -cn-> CC ) )
123 49 57 58 60 61 122 19 cncfshiftioo 
 |-  ( ph -> R e. ( ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) -cn-> CC ) )
124 19 a1i 
 |-  ( ph -> R = ( y e. ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) |-> ( G ` ( y - U ) ) ) )
125 17 oveq2i 
 |-  ( ( L ` ( E ` ( S ` J ) ) ) + U ) = ( ( L ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
126 125 a1i 
 |-  ( ph -> ( ( L ` ( E ` ( S ` J ) ) ) + U ) = ( ( L ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
127 69 66 oveq12d 
 |-  ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) )
128 68 64 oveq12d 
 |-  ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
129 127 128 eqeq12d 
 |-  ( j = J -> ( ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
130 63 129 imbi12d 
 |-  ( j = J -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) <-> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) ) )
131 85 fveq2i 
 |-  ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
132 131 oveq1i 
 |-  ( ( # ` H ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
133 12 132 eqtri 
 |-  N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
134 isoeq5 
 |-  ( H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
135 85 134 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
136 135 iotabii 
 |-  ( iota f f Isom < , < ( ( 0 ... N ) , H ) ) = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
137 13 136 eqtri 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
138 eqid 
 |-  ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
139 1 2 3 4 8 9 10 133 137 14 15 138 fourierdlem65 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( L ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
140 130 139 vtoclg 
 |-  ( J e. ( 0 ..^ N ) -> ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
141 140 anabsi7 
 |-  ( ( ph /\ J e. ( 0 ..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
142 16 141 mpdan 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
143 57 recnd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
144 55 recnd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. CC )
145 8 29 iccssred 
 |-  ( ph -> ( C [,] D ) C_ RR )
146 ax-resscn 
 |-  RR C_ CC
147 145 146 sstrdi 
 |-  ( ph -> ( C [,] D ) C_ CC )
148 10 37 36 fourierdlem15 
 |-  ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
149 148 45 ffvelcdmd 
 |-  ( ph -> ( S ` J ) e. ( C [,] D ) )
150 147 149 sseldd 
 |-  ( ph -> ( S ` J ) e. CC )
151 144 150 subcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
152 49 recnd 
 |-  ( ph -> ( L ` ( E ` ( S ` J ) ) ) e. CC )
153 143 151 152 subsub23d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( L ` ( E ` ( S ` J ) ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( L ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
154 142 153 mpbird 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( L ` ( E ` ( S ` J ) ) ) )
155 154 eqcomd 
 |-  ( ph -> ( L ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
156 155 oveq1d 
 |-  ( ph -> ( ( L ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
157 143 151 subcld 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
158 157 144 143 addsub12d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
159 143 151 143 sub32d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
160 143 subidd 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = 0 )
161 160 oveq1d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
162 df-neg 
 |-  -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
163 144 150 negsubdi2d 
 |-  ( ph -> -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
164 162 163 eqtr3id 
 |-  ( ph -> ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
165 159 161 164 3eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
166 165 oveq2d 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) )
167 144 150 pncan3d 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) = ( S ` J ) )
168 158 166 167 3eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` J ) )
169 126 156 168 3eqtrd 
 |-  ( ph -> ( ( L ` ( E ` ( S ` J ) ) ) + U ) = ( S ` J ) )
170 17 oveq2i 
 |-  ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
171 143 144 pncan3d 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` ( J + 1 ) ) )
172 170 171 eqtrid 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
173 169 172 oveq12d 
 |-  ( ph -> ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) )
174 173 mpteq1d 
 |-  ( ph -> ( y e. ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) |-> ( G ` ( y - U ) ) ) = ( y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) |-> ( G ` ( y - U ) ) ) )
175 5 feqmptd 
 |-  ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
176 175 reseq1d 
 |-  ( ph -> ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) = ( ( y e. RR |-> ( F ` y ) ) |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) )
177 ioossre 
 |-  ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ RR
178 177 a1i 
 |-  ( ph -> ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) C_ RR )
179 178 resmptd 
 |-  ( ph -> ( ( y e. RR |-> ( F ` y ) ) |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) = ( y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) |-> ( F ` y ) ) )
180 18 fveq1i 
 |-  ( G ` ( y - U ) ) = ( ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) ` ( y - U ) )
181 180 a1i 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( G ` ( y - U ) ) = ( ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) ` ( y - U ) ) )
182 49 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( L ` ( E ` ( S ` J ) ) ) e. RR )
183 182 rexrd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( L ` ( E ` ( S ` J ) ) ) e. RR* )
184 57 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
185 184 rexrd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR* )
186 178 sselda 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> y e. RR )
187 60 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> U e. RR )
188 186 187 resubcld 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - U ) e. RR )
189 46 rexrd 
 |-  ( ph -> ( S ` J ) e. RR* )
190 189 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( S ` J ) e. RR* )
191 55 rexrd 
 |-  ( ph -> ( S ` ( J + 1 ) ) e. RR* )
192 191 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. RR* )
193 simpr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) )
194 ioogtlb 
 |-  ( ( ( S ` J ) e. RR* /\ ( S ` ( J + 1 ) ) e. RR* /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( S ` J ) < y )
195 190 192 193 194 syl3anc 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( S ` J ) < y )
196 169 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) + U ) = ( S ` J ) )
197 186 recnd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> y e. CC )
198 187 recnd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> U e. CC )
199 197 198 npcand 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( y - U ) + U ) = y )
200 195 196 199 3brtr4d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) + U ) < ( ( y - U ) + U ) )
201 182 188 187 ltadd1d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( L ` ( E ` ( S ` J ) ) ) < ( y - U ) <-> ( ( L ` ( E ` ( S ` J ) ) ) + U ) < ( ( y - U ) + U ) ) )
202 200 201 mpbird 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( L ` ( E ` ( S ` J ) ) ) < ( y - U ) )
203 iooltub 
 |-  ( ( ( S ` J ) e. RR* /\ ( S ` ( J + 1 ) ) e. RR* /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> y < ( S ` ( J + 1 ) ) )
204 190 192 193 203 syl3anc 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> y < ( S ` ( J + 1 ) ) )
205 172 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
206 204 199 205 3brtr4d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( y - U ) + U ) < ( ( E ` ( S ` ( J + 1 ) ) ) + U ) )
207 188 184 187 ltadd1d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( y - U ) < ( E ` ( S ` ( J + 1 ) ) ) <-> ( ( y - U ) + U ) < ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) )
208 206 207 mpbird 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - U ) < ( E ` ( S ` ( J + 1 ) ) ) )
209 183 185 188 202 208 eliood 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - U ) e. ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
210 fvres 
 |-  ( ( y - U ) e. ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) ` ( y - U ) ) = ( F ` ( y - U ) ) )
211 209 210 syl 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( F |` ( ( L ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) ` ( y - U ) ) = ( F ` ( y - U ) ) )
212 17 oveq2i 
 |-  ( y - U ) = ( y - ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
213 212 a1i 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - U ) = ( y - ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
214 144 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. CC )
215 143 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
216 197 214 215 subsub2d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( y + ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) )
217 215 214 subcld 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
218 23 22 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
219 2 218 eqeltrid 
 |-  ( ph -> T e. RR )
220 219 recnd 
 |-  ( ph -> T e. CC )
221 220 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> T e. CC )
222 22 23 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
223 25 222 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
224 223 2 breqtrrdi 
 |-  ( ph -> 0 < T )
225 224 gt0ne0d 
 |-  ( ph -> T =/= 0 )
226 225 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> T =/= 0 )
227 217 221 226 divcan1d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
228 227 eqcomd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) )
229 228 oveq2d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y + ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) = ( y + ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) ) )
230 213 216 229 3eqtrd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( y - U ) = ( y + ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) ) )
231 230 fveq2d 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( F ` ( y - U ) ) = ( F ` ( y + ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) ) ) )
232 5 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> F : RR --> CC )
233 219 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> T e. RR )
234 14 a1i 
 |-  ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
235 id 
 |-  ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
236 oveq2 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
237 236 oveq1d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
238 237 fveq2d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
239 238 oveq1d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
240 235 239 oveq12d 
 |-  ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
241 240 adantl 
 |-  ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
242 23 55 resubcld 
 |-  ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
243 242 219 225 redivcld 
 |-  ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
244 243 flcld 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
245 244 zred 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
246 245 219 remulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
247 55 246 readdcld 
 |-  ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
248 234 241 55 247 fvmptd 
 |-  ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
249 248 oveq1d 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) )
250 245 recnd 
 |-  ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
251 250 220 mulcld 
 |-  ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
252 144 251 pncan2d 
 |-  ( ph -> ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
253 249 252 eqtrd 
 |-  ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
254 253 oveq1d 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
255 250 220 225 divcan4d 
 |-  ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
256 254 255 eqtrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
257 256 244 eqeltrd 
 |-  ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
258 257 adantr 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
259 6 adantlr 
 |-  ( ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
260 232 233 258 186 259 fperiodmul 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( F ` ( y + ( ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) x. T ) ) ) = ( F ` y ) )
261 231 260 eqtrd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( F ` ( y - U ) ) = ( F ` y ) )
262 181 211 261 3eqtrrd 
 |-  ( ( ph /\ y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) -> ( F ` y ) = ( G ` ( y - U ) ) )
263 262 mpteq2dva 
 |-  ( ph -> ( y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) |-> ( F ` y ) ) = ( y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) |-> ( G ` ( y - U ) ) ) )
264 176 179 263 3eqtrrd 
 |-  ( ph -> ( y e. ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) |-> ( G ` ( y - U ) ) ) = ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) )
265 124 174 264 3eqtrd 
 |-  ( ph -> R = ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) )
266 173 oveq1d 
 |-  ( ph -> ( ( ( ( L ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) -cn-> CC ) = ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) -cn-> CC ) )
267 123 265 266 3eltr3d 
 |-  ( ph -> ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) e. ( ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) -cn-> CC ) )