fourierdlem98

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem98.f	\|- ( ph -> F : RR --> RR )
	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 ) ) ) } )
	fourierdlem98.t	\|- T = ( B - A )
	fourierdlem98.m	\|- ( ph -> M e. NN )
	fourierdlem98.q	\|- ( ph -> Q e. ( P ` M ) )
	fourierdlem98.fper	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
	fourierdlem98.qcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem98.c	\|- ( ph -> C e. RR )
	fourierdlem98.d	\|- ( ph -> D e. ( C (,) +oo ) )
	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 ) ) )
	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 } ) ) )
Assertion	fourierdlem98	\|- ( ph -> ( F \|` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )

Proof

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 ) )

Metamath Proof Explorer

Theorem fourierdlem98

Proof