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