Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem99.f |
|- ( ph -> F : RR --> RR ) |
2 |
|
fourierdlem99.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 ) ) ) } ) |
3 |
|
fourierdlem99.t |
|- T = ( B - A ) |
4 |
|
fourierdlem99.m |
|- ( ph -> M e. NN ) |
5 |
|
fourierdlem99.q |
|- ( ph -> Q e. ( P ` M ) ) |
6 |
|
fourierdlem99.fper |
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) |
7 |
|
fourierdlem99.qcn |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) |
8 |
|
fourierdlem99.l |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) |
9 |
|
fourierdlem99.c |
|- ( ph -> C e. RR ) |
10 |
|
fourierdlem99.d |
|- ( ph -> D e. ( C (,) +oo ) ) |
11 |
|
fourierdlem99.j |
|- ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) ) |
12 |
|
fourierdlem99.v |
|- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) |
13 |
|
ax-resscn |
|- RR C_ CC |
14 |
13
|
a1i |
|- ( ph -> RR C_ CC ) |
15 |
1 14
|
fssd |
|- ( ph -> F : RR --> CC ) |
16 |
|
eqid |
|- ( 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 ) ) ) } ) = ( 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 ) ) ) } ) |
17 |
|
oveq1 |
|- ( z = y -> ( z + ( l x. T ) ) = ( y + ( l x. T ) ) ) |
18 |
17
|
eleq1d |
|- ( z = y -> ( ( z + ( l x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) ) |
19 |
18
|
rexbidv |
|- ( z = y -> ( E. l e. ZZ ( z + ( l x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) ) |
20 |
19
|
cbvrabv |
|- { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } |
21 |
20
|
uneq2i |
|- ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) |
22 |
21
|
eqcomi |
|- ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } ) |
23 |
|
oveq1 |
|- ( k = l -> ( k x. T ) = ( l x. T ) ) |
24 |
23
|
oveq2d |
|- ( k = l -> ( y + ( k x. T ) ) = ( y + ( l x. T ) ) ) |
25 |
24
|
eleq1d |
|- ( k = l -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) ) |
26 |
25
|
cbvrexvw |
|- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) |
27 |
26
|
a1i |
|- ( y e. ( C [,] D ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) ) |
28 |
27
|
rabbiia |
|- { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } |
29 |
28
|
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. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) |
30 |
29
|
fveq2i |
|- ( # ` ( { 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. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) |
31 |
30
|
oveq1i |
|- ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 ) |
32 |
|
oveq1 |
|- ( l = h -> ( l x. T ) = ( h x. T ) ) |
33 |
32
|
oveq2d |
|- ( l = h -> ( y + ( l x. T ) ) = ( y + ( h x. T ) ) ) |
34 |
33
|
eleq1d |
|- ( l = h -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) ) |
35 |
34
|
cbvrexvw |
|- ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) |
36 |
35
|
a1i |
|- ( y e. ( C [,] D ) -> ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) ) |
37 |
36
|
rabbiia |
|- { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } |
38 |
37
|
uneq2i |
|- ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) |
39 |
|
isoeq5 |
|- ( ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) ) |
40 |
38 39
|
ax-mp |
|- ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) |
41 |
40
|
iotabii |
|- ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) |
42 |
|
isoeq1 |
|- ( f = g -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) ) |
43 |
42
|
cbviotavw |
|- ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) |
44 |
41 43 12
|
3eqtr4ri |
|- V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) |
45 |
|
id |
|- ( v = x -> v = x ) |
46 |
|
oveq2 |
|- ( v = x -> ( B - v ) = ( B - x ) ) |
47 |
46
|
oveq1d |
|- ( v = x -> ( ( B - v ) / T ) = ( ( B - x ) / T ) ) |
48 |
47
|
fveq2d |
|- ( v = x -> ( |_ ` ( ( B - v ) / T ) ) = ( |_ ` ( ( B - x ) / T ) ) ) |
49 |
48
|
oveq1d |
|- ( v = x -> ( ( |_ ` ( ( B - v ) / T ) ) x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) |
50 |
45 49
|
oveq12d |
|- ( v = x -> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) |
51 |
50
|
cbvmptv |
|- ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) |
52 |
|
eqeq1 |
|- ( u = z -> ( u = B <-> z = B ) ) |
53 |
|
id |
|- ( u = z -> u = z ) |
54 |
52 53
|
ifbieq2d |
|- ( u = z -> if ( u = B , A , u ) = if ( z = B , A , z ) ) |
55 |
54
|
cbvmptv |
|- ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) = ( z e. ( A (,] B ) |-> if ( z = B , A , z ) ) |
56 |
|
eqid |
|- ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) = ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) |
57 |
|
fveq2 |
|- ( j = i -> ( Q ` j ) = ( Q ` i ) ) |
58 |
57
|
breq1d |
|- ( j = i -> ( ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) <-> ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) ) ) |
59 |
58
|
cbvrabv |
|- { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } |
60 |
|
fveq2 |
|- ( y = x -> ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) = ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) |
61 |
60
|
fveq2d |
|- ( y = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) ) |
62 |
61
|
breq2d |
|- ( y = x -> ( ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) <-> ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) ) ) |
63 |
62
|
rabbidv |
|- ( y = x -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } ) |
64 |
59 63
|
syl5eq |
|- ( y = x -> { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } ) |
65 |
64
|
supeq1d |
|- ( y = x -> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) ) |
66 |
65
|
cbvmptv |
|- ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) ) |
67 |
|
eqid |
|- ( i e. ( 0 ..^ M ) |-> L ) = ( i e. ( 0 ..^ M ) |-> L ) |
68 |
2 3 4 5 15 6 7 8 9 10 16 22 31 44 51 55 11 56 66 67
|
fourierdlem91 |
|- ( ph -> if ( ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) = ( Q ` ( ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) + 1 ) ) , ( ( i e. ( 0 ..^ M ) |-> L ) ` ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( F ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) limCC ( V ` ( J + 1 ) ) ) ) |