Theorem fourierdlem91 32162

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

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

Assertion

Ref	Expression
fourierdlem91	|- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( S ` J ) (,) ( S ` ( J + 1 ) ) ) ) lim CC ( S ` ( J + 1 ) ) ) )

Distinct variable groups:   A, f, k, y   A, i, x, k, y   A, m, p, i   B, f, k, y   B, i, x   B, m, p   C, f, y   C, i, m, p   x, C   D, f, y   D, i, m, p   x, D   f, E, k, y   i, E, x   i, F, x, y   f, H   x, H   f, I, k, y   i, I, x   i, J, x, y   i, M, x   m, M, p   f, N, k, y   i, N, x   m, N, p   Q, f, k, y   Q, i, x   Q, p   S, f, k, y   S, i, x   S, p   T, f, k, y   T, i, x   x, U, y   x, W, y   i, Z, x, y   ph, f, k, y   ph, i, x

Allowed substitution hints:   ph( m, p)   C( k)   D( k)   P( x, y, f, i, k, m, p)   Q( m)   S( m)   T( m, p)   U( f, i, k, m, p)   E( m, p)   F( f, k, m, p)   H( y, i, k, m, p)   I( m, p)   J( f, k, m, p)   L( x, y, f, i, k, m, p)   M( y, f, k)   O( x, y, f, i, k, m, p)   W( f, i, k, m, p)   Z( f, k, m, p)

Proof of Theorem fourierdlem91

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem91.q	. . . . . . . . . . . 12 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem91.m	. . . . . . . . . . . . 13 |- ( ph -> M e. NN )
3		fourierdlem91.p	. . . . . . . . . . . . . 14 |- 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	3	fourierdlem2 32073	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) ) )
5	2, 4	syl 16	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
6	1, 5	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simpld 459	. . . . . . . . . 10 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		elmapi 7459	. . . . . . . . . 10 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
9	7, 8	syl 16	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> RR )
10		fzossfz 11844	. . . . . . . . . 10 |- ( 0..^ M ) C_ ( 0 ... M )
11		fourierdlem91.t	. . . . . . . . . . . . 13 |- T = ( B - A )
12		fourierdlem91.e	. . . . . . . . . . . . 13 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13		fourierdlem91.J	. . . . . . . . . . . . 13 |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
14		fourierdlem91.i	. . . . . . . . . . . . 13 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 32108	. . . . . . . . . . . 12 |- ( ph -> ( I : RR --> ( 0..^ M ) /\ ( x e. RR -> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) e. { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } ) ) )
16	15	simpld 459	. . . . . . . . . . 11 |- ( ph -> I : RR --> ( 0..^ M ) )
17		fourierdlem91.c	. . . . . . . . . . . . . . . . . 18 |- ( ph -> C e. RR )
18		fourierdlem91.d	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D e. ( C (,) +oo ) )
19		elioore 11584	. . . . . . . . . . . . . . . . . . 19 |- ( D e. ( C (,) +oo ) -> D e. RR )
20	18, 19	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D e. RR )
21		elioo4g 11610	. . . . . . . . . . . . . . . . . . . . 21 |- ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
22	18, 21	sylib 196	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
23	22	simprd 463	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( C < D /\ D < +oo ) )
24	23	simpld 459	. . . . . . . . . . . . . . . . . 18 |- ( ph -> C < D )
25		fourierdlem91.o	. . . . . . . . . . . . . . . . . 18 |- 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 ) ) ) } )
26		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
27	26	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
28	27	rexbidv 2968	. . . . . . . . . . . . . . . . . . . 20 |- ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
29	28	cbvrabv 3108	. . . . . . . . . . . . . . . . . . 19 |- { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
30	29	uneq2i 3651	. . . . . . . . . . . . . . . . . 18 |- ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
31		fourierdlem91.n	. . . . . . . . . . . . . . . . . . 19 |- N = ( ( # ` H ) - 1 )
32		fourierdlem91.h	. . . . . . . . . . . . . . . . . . . . 21 |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
33	32	fveq2i 5875	. . . . . . . . . . . . . . . . . . . 20 |- ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
34	33	oveq1i 6306	. . . . . . . . . . . . . . . . . . 19 |- ( ( # ` H ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
35	31, 34	eqtri 2486	. . . . . . . . . . . . . . . . . 18 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
36		fourierdlem91.s	. . . . . . . . . . . . . . . . . . 19 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
37		isoeq5 6220	. . . . . . . . . . . . . . . . . . . . 21 |- ( H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) 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. T ) ) e. ran Q } ) ) ) )
38	32, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
39	38	iotabii 5579	. . . . . . . . . . . . . . . . . . 19 |- ( 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. T ) ) e. ran Q } ) ) )
40	36, 39	eqtri 2486	. . . . . . . . . . . . . . . . . 18 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
41	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40	fourierdlem54 32125	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
42	41	simpld 459	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
43	42	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> S e. ( O ` N ) )
44	42	simpld 459	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. NN )
45	25	fourierdlem2 32073	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) ) )
46	44, 45	syl 16	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
47	43, 46	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
48	47	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
49		elmapi 7459	. . . . . . . . . . . . 13 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
50	48, 49	syl 16	. . . . . . . . . . . 12 |- ( ph -> S : ( 0 ... N ) --> RR )
51		fourierdlem91.17	. . . . . . . . . . . . 13 |- ( ph -> J e. ( 0..^ N ) )
52		elfzofz 11841	. . . . . . . . . . . . 13 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
53	51, 52	syl 16	. . . . . . . . . . . 12 |- ( ph -> J e. ( 0 ... N ) )
54	50, 53	ffvelrnd 6033	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. RR )
55	16, 54	ffvelrnd 6033	. . . . . . . . . 10 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
56	10, 55	sseldi 3497	. . . . . . . . 9 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
57	9, 56	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
58	57	rexrd 9660	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
59	58	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
60		fzofzp1 11912	. . . . . . . . . 10 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
61	55, 60	syl 16	. . . . . . . . 9 |- ( ph -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
62	9, 61	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
63	62	rexrd 9660	. . . . . . 7 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
64	63	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
65	3, 2, 1	fourierdlem11 32082	. . . . . . . . . . 11 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
66	65	simp1d 1008	. . . . . . . . . 10 |- ( ph -> A e. RR )
67	66	rexrd 9660	. . . . . . . . 9 |- ( ph -> A e. RR* )
68	65	simp2d 1009	. . . . . . . . 9 |- ( ph -> B e. RR )
69		iocssre 11629	. . . . . . . . 9 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
70	67, 68, 69	syl2anc 661	. . . . . . . 8 |- ( ph -> ( A (,] B ) C_ RR )
71	65	simp3d 1010	. . . . . . . . . 10 |- ( ph -> A < B )
72	66, 68, 71, 11, 12	fourierdlem4 32075	. . . . . . . . 9 |- ( ph -> E : RR --> ( A (,] B ) )
73		fzofzp1 11912	. . . . . . . . . . 11 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
74	51, 73	syl 16	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
75	50, 74	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
76	72, 75	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
77	70, 76	sseldd 3500	. . . . . . 7 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
78	77	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
79	66, 68	iccssred 31721	. . . . . . . . 9 |- ( ph -> ( A [,] B ) C_ RR )
80	66, 68, 71, 13	fourierdlem17 32088	. . . . . . . . . 10 |- ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
81	72, 54	ffvelrnd 6033	. . . . . . . . . 10 |- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
82	80, 81	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
83	79, 82	sseldd 3500	. . . . . . . 8 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
84	47	simprrd 758	. . . . . . . . . . . . . 14 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
85		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` i ) = ( S ` J ) )
86		oveq1 6303	. . . . . . . . . . . . . . . . 17 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
87	86	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
88	85, 87	breq12d 4469	. . . . . . . . . . . . . . 15 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
89	88	rspccva 3209	. . . . . . . . . . . . . 14 |- ( ( A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) /\ J e. ( 0..^ N ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
90	84, 51, 89	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
91	54, 75	posdifd 10160	. . . . . . . . . . . . 13 |- ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
92	90, 91	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
93		eleq1 2529	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
94	93	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
95		oveq1 6303	. . . . . . . . . . . . . . . . . . . 20 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
96	95	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
97	96	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
98		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( j = J -> ( S ` j ) = ( S ` J ) )
99	98	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
100	99	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
101	97, 100	oveq12d 6314	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
102	96, 98	oveq12d 6314	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
103	101, 102	eqeq12d 2479	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
104	94, 103	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) ) <-> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) ) )
105	11	oveq2i 6307	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k x. T ) = ( k x. ( B - A ) )
106	105	oveq2i 6307	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
107	106	eleq1i 2534	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
108	107	rexbii 2959	. . . . . . . . . . . . . . . . . . . . . 22 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
109	108	rgenw 2818	. . . . . . . . . . . . . . . . . . . . 21 |- A. 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 )
110		rabbi 3036	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. 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 ) <-> { 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 } )
111	109, 110	mpbi 208	. . . . . . . . . . . . . . . . . . . 20 |- { 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 }
112	111	uneq2i 3651	. . . . . . . . . . . . . . . . . . 19 |- ( { 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 } )
113	112	fveq2i 5875	. . . . . . . . . . . . . . . . . 18 |- ( # ` ( { 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 } ) )
114	113	oveq1i 6306	. . . . . . . . . . . . . . . . 17 |- ( ( # ` ( { 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. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
115	35, 114	eqtri 2486	. . . . . . . . . . . . . . . 16 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
116		isoeq5 6220	. . . . . . . . . . . . . . . . . . 19 |- ( ( { 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 } ) -> ( f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
117	112, 116	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
118	117	iotabii 5579	. . . . . . . . . . . . . . . . 17 |- ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( 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 } ) ) )
119	40, 118	eqtri 2486	. . . . . . . . . . . . . . . 16 |- 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 } ) ) )
120		eqid 2457	. . . . . . . . . . . . . . . 16 |- ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
121	3, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120	fourierdlem65 32136	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
122	104, 121	vtoclg 3167	. . . . . . . . . . . . . 14 |- ( J e. ( 0..^ N ) -> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
123	122	anabsi7 819	. . . . . . . . . . . . 13 |- ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
124	51, 123	mpdan 668	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
125	92, 124	breqtrrd 4482	. . . . . . . . . . 11 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
126	83, 77	posdifd 10160	. . . . . . . . . . 11 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
127	125, 126	mpbird 232	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
128	100, 97	oveq12d 6314	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
129	98	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
130	129	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
131	129	oveq1d 6311	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
132	131	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
133	130, 132	oveq12d 6314	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
134	128, 133	sseq12d 3528	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) <-> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
135	94, 134	imbi12d 320	. . . . . . . . . . . . 13 |- ( j = J -> ( ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) ) <-> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
136	32, 30	eqtri 2486	. . . . . . . . . . . . . 14 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
137		eqid 2457	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
138	11, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14	fourierdlem79 32150	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
139	135, 138	vtoclg 3167	. . . . . . . . . . . 12 |- ( J e. ( 0..^ N ) -> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
140	139	anabsi7 819	. . . . . . . . . . 11 |- ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
141	51, 140	mpdan 668	. . . . . . . . . 10 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
142	57, 62, 83, 77, 127, 141	fourierdlem10 32081	. . . . . . . . 9 |- ( ph -> ( ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) /\ ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
143	142	simpld 459	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
144	57, 83, 77, 143, 127	lelttrd 9757	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
145	144	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
146	62	adantr 465	. . . . . . 7 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
147	142	simprd 463	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
148	147	adantr 465	. . . . . . 7 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
149		neqne 31616	. . . . . . . . 9 |- ( -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) -> ( E ` ( S ` ( J + 1 ) ) ) =/= ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
150	149	necomd 2728	. . . . . . . 8 |- ( -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) =/= ( E ` ( S ` ( J + 1 ) ) ) )
151	150	adantl 466	. . . . . . 7 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) =/= ( E ` ( S ` ( J + 1 ) ) ) )
152	78, 146, 148, 151	leneltd 31676	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
153	59, 64, 78, 145, 152	eliood 31713	. . . . 5 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
154		fvres 5886	. . . . 5 |- ( ( E ` ( S ` ( J + 1 ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) = ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) )
155	153, 154	syl 16	. . . 4 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) = ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) )
156	155	eqcomd 2465	. . 3 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) )
157	156	ifeq2da 3975	. 2 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( F ` ( E ` ( S ` ( J + 1 ) ) ) ) ) = if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) )
158		fourierdlem91.f	. . . . . 6 |- ( ph -> F : RR --> CC )
159		fdm 5741	. . . . . . . 8 |- ( F : RR --> CC -> dom F = RR )
160	158, 159	syl 16	. . . . . . 7 |- ( ph -> dom F = RR )
161	160	feq2d 5724	. . . . . 6 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
162	158, 161	mpbird 232	. . . . 5 |- ( ph -> F : dom F --> CC )
163		ioosscn 31709	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC
164	163	a1i 11	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC )
165		ioossre 11611	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
166	165, 160	syl5sseqr 3548	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ dom F )
167		fourierdlem91.u	. . . . . . 7 |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
168	75, 77	resubcld 10008	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
169	167, 168	syl5eqel 2549	. . . . . 6 |- ( ph -> U e. RR )
170	169	recnd 9639	. . . . 5 |- ( ph -> U e. CC )
171		eqid 2457	. . . . 5 |- { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } = { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) }
172	83, 77, 169	iooshift 31744	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } )
173		ioossre 11611	. . . . . . 7 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
174	173, 160	syl5sseqr 3548	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
175	172, 174	eqsstr3d 3534	. . . . 5 |- ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
176		elioore 11584	. . . . . 6 |- ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
177	68, 66	resubcld 10008	. . . . . . . . . . . . . 14 |- ( ph -> ( B - A ) e. RR )
178	11, 177	syl5eqel 2549	. . . . . . . . . . . . 13 |- ( ph -> T e. RR )
179	178	recnd 9639	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
180	66, 68	posdifd 10160	. . . . . . . . . . . . . . 15 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
181	71, 180	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( B - A ) )
182	181, 11	syl6breqr 4496	. . . . . . . . . . . . 13 |- ( ph -> 0 < T )
183	182	gt0ne0d 10138	. . . . . . . . . . . 12 |- ( ph -> T =/= 0 )
184	170, 179, 183	divcan1d 10342	. . . . . . . . . . 11 |- ( ph -> ( ( U / T ) x. T ) = U )
185	184	eqcomd 2465	. . . . . . . . . 10 |- ( ph -> U = ( ( U / T ) x. T ) )
186	185	oveq2d 6312	. . . . . . . . 9 |- ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
187	186	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
188	187	fveq2d 5876	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
189	158	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
190	178	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> T e. RR )
191	77	recnd 9639	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
192	75	recnd 9639	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
193	191, 192	negsubdi2d 9966	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
194	193	eqcomd 2465	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
195	194	oveq1d 6311	. . . . . . . . . . 11 |- ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
196	167	oveq1i 6306	. . . . . . . . . . . 12 |- ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T )
197	196	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) )
198	12	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
199		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
200		oveq2 6304	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
201	200	oveq1d 6311	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
202	201	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
203	202	oveq1d 6311	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
204	199, 203	oveq12d 6314	. . . . . . . . . . . . . . . . 17 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
205	204	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
206	68, 75	resubcld 10008	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
207	206, 178, 183	redivcld 10393	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
208	207	flcld 11938	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
209	208	zred 10990	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
210	209, 178	remulcld 9641	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
211	75, 210	readdcld 9640	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
212	198, 205, 75, 211	fvmptd 5961	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
213	212	oveq1d 6311	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) )
214	208	zcnd 10991	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
215	214, 179	mulcld 9633	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
216	192, 215	pncan2d 9952	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
217	213, 216	eqtrd 2498	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
218	217, 215	eqeltrd 2545	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
219	218, 179, 183	divnegd 10354	. . . . . . . . . . 11 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
220	195, 197, 219	3eqtr4d 2508	. . . . . . . . . 10 |- ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
221	217	oveq1d 6311	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
222	214, 179, 183	divcan4d 10347	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
223	221, 222	eqtrd 2498	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
224	223, 208	eqeltrd 2545	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
225	224	znegcld 10992	. . . . . . . . . 10 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
226	220, 225	eqeltrd 2545	. . . . . . . . 9 |- ( ph -> ( U / T ) e. ZZ )
227	226	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
228		simpr 461	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> y e. RR )
229		fourierdlem91.6	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
230	229	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
231	189, 190, 227, 228, 230	fperiodmul 31686	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
232	188, 231	eqtrd 2498	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
233	176, 232	sylan2 474	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
234	6	simprrd 758	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
235		fveq2 5872	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
236		oveq1 6303	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
237	236	fveq2d 5876	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
238	235, 237	breq12d 4469	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
239	238	rspccva 3209	. . . . . . . 8 |- ( ( A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
240	234, 55, 239	syl2anc 661	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
241	55	ancli 551	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
242		eleq1 2529	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
243	242	anbi2d 703	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
244	235, 237	oveq12d 6314	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
245	244	reseq2d 5283	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
246	244	oveq1d 6311	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
247	245, 246	eleq12d 2539	. . . . . . . . . 10 |- ( 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 ) ) )
248	243, 247	imbi12d 320	. . . . . . . . 9 |- ( 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 ) ) ) )
249		fourierdlem91.fcn	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
250	248, 249	vtoclg 3167	. . . . . . . 8 |- ( ( 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 ) ) )
251	55, 241, 250	sylc 60	. . . . . . 7 |- ( ph -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
252		nfv 1708	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
253		fourierdlem91.w	. . . . . . . . . . . . 13 |- W = ( i e. ( 0..^ M ) |-> L )
254		nfmpt1 4546	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> L )
255	253, 254	nfcxfr 2617	. . . . . . . . . . . 12 |- F/_ i W
256		nfcv 2619	. . . . . . . . . . . 12 |- F/_ i ( I ` ( S ` J ) )
257	255, 256	nffv 5879	. . . . . . . . . . 11 |- F/_ i ( W ` ( I ` ( S ` J ) ) )
258	257	nfel1 2635	. . . . . . . . . 10 |- F/ i ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
259	252, 258	nfim 1921	. . . . . . . . 9 |- F/ i ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
260	243	biimpar 485	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
261	260	3adant2 1015	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
262		fourierdlem91.l	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
263	261, 262	syl 16	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
264		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( W ` i ) = ( W ` ( I ` ( S ` J ) ) ) )
265	264	eqcomd 2465	. . . . . . . . . . . . . . 15 |- ( i = ( I ` ( S ` J ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
266	265	adantr 465	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
267	260	simprd 463	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
268		elex 3118	. . . . . . . . . . . . . . . 16 |- ( L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) -> L e. _V )
269	260, 262, 268	3syl 20	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> L e. _V )
270	253	fvmpt2 5964	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0..^ M ) /\ L e. _V ) -> ( W ` i ) = L )
271	267, 269, 270	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` i ) = L )
272	266, 271	eqtrd 2498	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = L )
273	272	3adant2 1015	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = L )
274	245, 237	oveq12d 6314	. . . . . . . . . . . . . 14 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
275	274	eqcomd 2465	. . . . . . . . . . . . 13 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
276	275	3ad2ant1 1017	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
277	263, 273, 276	3eltr4d 2560	. . . . . . . . . . 11 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
278	277	3exp 1195	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
279	262	a1ii 27	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) ) )
280	278, 279	impbid 191	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
281	259, 280, 262	vtoclg1f 3166	. . . . . . . 8 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
282	55, 241, 281	sylc 60	. . . . . . 7 |- ( ph -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
283		eqid 2457	. . . . . . 7 |- if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) = if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) )
284		eqid 2457	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) u. { ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) u. { ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) } ) )
285	57, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284	fourierdlem33 32104	. . . . . 6 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
286	141	resabs1d 5313	. . . . . . 7 |- ( ph -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) )
287	286	oveq1d 6311	. . . . . 6 |- ( ph -> ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
288	285, 287	eleqtrd 2547	. . . . 5 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
289	162, 164, 166, 170, 171, 175, 233, 288	limcperiod 31816	. . . 4 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) )
290	167	oveq2i 6307	. . . . . 6 |- ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
291	191, 192	pncan3d 9953	. . . . . 6 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` ( J + 1 ) ) )
292	290, 291	syl5eq 2510	. . . . 5 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
293	292	oveq2d 6312	. . . 4 |- ( ph -> ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( S ` ( J + 1 ) ) ) )
294	289, 293	eleqtrd 2547	. . 3 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( S ` ( J + 1 ) ) ) )
295	167	oveq2i 6307	. . . . . . . . 9 |- ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
296	295	a1i 11	. . . . . . . 8 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
297	17, 20	iccssred 31721	. . . . . . . . . . . . . . 15 |- ( ph -> ( C [,] D ) C_ RR )
298		ax-resscn 9566	. . . . . . . . . . . . . . 15 |- RR C_ CC
299	297, 298	syl6ss 3511	. . . . . . . . . . . . . 14 |- ( ph -> ( C [,] D ) C_ CC )
300	25, 44, 43	fourierdlem15 32086	. . . . . . . . . . . . . . 15 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
301	300, 53	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` J ) e. ( C [,] D ) )
302	299, 301	sseldd 3500	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) e. CC )
303	192, 302	subcld 9950	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
304	83	recnd 9639	. . . . . . . . . . . 12 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
305	191, 303, 304	subsub23d 31656	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) <-> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
306	124, 305	mpbird 232	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
307	306	eqcomd 2465	. . . . . . . . 9 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
308	307	oveq1d 6311	. . . . . . . 8 |- ( ph -> ( ( Z ` ( 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 ) ) ) ) ) )
309	191, 303	subcld 9950	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
310	309, 192, 191	addsub12d 9973	. . . . . . . . 9 |- ( 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