Theorem fourierdlem91 37348

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 37259	. . . . . . . . . . . . 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 17	. . . . . . . . . . . 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 457	. . . . . . . . . 10 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		elmapi 7478	. . . . . . . . . 10 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
9	7, 8	syl 17	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> RR )
10		fzossfz 11877	. . . . . . . . . 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 37294	. . . . . . . . . . . 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 457	. . . . . . . . . . 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 11612	. . . . . . . . . . . . . . . . . . 19 |- ( D e. ( C (,) +oo ) -> D e. RR )
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D e. RR )
21		elioo4g 11639	. . . . . . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( C < D /\ D < +oo ) )
24	23	simpld 457	. . . . . . . . . . . . . . . . . 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 6285	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
27	26	eleq1d 2471	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
28	27	rexbidv 2918	. . . . . . . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . . . . 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 3594	. . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . . . . 20 |- ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
34	33	oveq1i 6288	. . . . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . . . 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 6202	. . . . . . . . . . . . . . . . . . . . 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 5555	. . . . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . . . 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 37311	. . . . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
43	42	simprd 461	. . . . . . . . . . . . . . 15 |- ( ph -> S e. ( O ` N ) )
44	42	simpld 457	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. NN )
45	25	fourierdlem2 37259	. . . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . 13 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
49		elmapi 7478	. . . . . . . . . . . . 13 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
50	48, 49	syl 17	. . . . . . . . . . . 12 |- ( ph -> S : ( 0 ... N ) --> RR )
51		fourierdlem91.17	. . . . . . . . . . . . 13 |- ( ph -> J e. ( 0..^ N ) )
52		elfzofz 11874	. . . . . . . . . . . . 13 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
53	51, 52	syl 17	. . . . . . . . . . . 12 |- ( ph -> J e. ( 0 ... N ) )
54	50, 53	ffvelrnd 6010	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. RR )
55	16, 54	ffvelrnd 6010	. . . . . . . . . 10 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
56	10, 55	sseldi 3440	. . . . . . . . 9 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
57	9, 56	ffvelrnd 6010	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
58	57	rexrd 9673	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
59	58	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
60		fzofzp1 11946	. . . . . . . . . 10 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
61	55, 60	syl 17	. . . . . . . . 9 |- ( ph -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
62	9, 61	ffvelrnd 6010	. . . . . . . 8 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
63	62	rexrd 9673	. . . . . . 7 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
64	63	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
65	3, 2, 1	fourierdlem11 37268	. . . . . . . . . . 11 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
66	65	simp1d 1009	. . . . . . . . . 10 |- ( ph -> A e. RR )
67	66	rexrd 9673	. . . . . . . . 9 |- ( ph -> A e. RR* )
68	65	simp2d 1010	. . . . . . . . 9 |- ( ph -> B e. RR )
69		iocssre 11658	. . . . . . . . 9 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
70	67, 68, 69	syl2anc 659	. . . . . . . 8 |- ( ph -> ( A (,] B ) C_ RR )
71	65	simp3d 1011	. . . . . . . . . 10 |- ( ph -> A < B )
72	66, 68, 71, 11, 12	fourierdlem4 37261	. . . . . . . . 9 |- ( ph -> E : RR --> ( A (,] B ) )
73		fzofzp1 11946	. . . . . . . . . . 11 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
74	51, 73	syl 17	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
75	50, 74	ffvelrnd 6010	. . . . . . . . 9 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
76	72, 75	ffvelrnd 6010	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
77	70, 76	sseldd 3443	. . . . . . 7 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
78	77	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
79	66, 68	iccssred 36907	. . . . . . . . 9 |- ( ph -> ( A [,] B ) C_ RR )
80	66, 68, 71, 13	fourierdlem17 37274	. . . . . . . . . 10 |- ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
81	72, 54	ffvelrnd 6010	. . . . . . . . . 10 |- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
82	80, 81	ffvelrnd 6010	. . . . . . . . 9 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
83	79, 82	sseldd 3443	. . . . . . . 8 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
84	47	simprrd 759	. . . . . . . . . . . . . 14 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
85		fveq2 5849	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` i ) = ( S ` J ) )
86		oveq1 6285	. . . . . . . . . . . . . . . . 17 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
87	86	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
88	85, 87	breq12d 4408	. . . . . . . . . . . . . . 15 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
89	88	rspccva 3159	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
91	54, 75	posdifd 10179	. . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
94	93	anbi2d 702	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
95		oveq1 6285	. . . . . . . . . . . . . . . . . . . 20 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
96	95	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
97	96	fveq2d 5853	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
98		fveq2 5849	. . . . . . . . . . . . . . . . . . . 20 |- ( j = J -> ( S ` j ) = ( S ` J ) )
99	98	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
100	99	fveq2d 5853	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
101	97, 100	oveq12d 6296	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
102	96, 98	oveq12d 6296	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
103	101, 102	eqeq12d 2424	. . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . 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 6289	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k x. T ) = ( k x. ( B - A ) )
106	105	oveq2i 6289	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
107	106	eleq1i 2479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
108	107	rexbii 2906	. . . . . . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . . . . . . 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 2986	. . . . . . . . . . . . . . . . . . . . 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 3594	. . . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . . 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 6288	. . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . 16 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
116		isoeq5 6202	. . . . . . . . . . . . . . . . . . 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 5555	. . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . 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 2402	. . . . . . . . . . . . . . . 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 37322	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
122	104, 121	vtoclg 3117	. . . . . . . . . . . . . 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 820	. . . . . . . . . . . . 13 |- ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
124	51, 123	mpdan 666	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
125	92, 124	breqtrrd 4421	. . . . . . . . . . 11 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
126	83, 77	posdifd 10179	. . . . . . . . . . 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 6296	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
129	98	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
130	129	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
131	129	oveq1d 6293	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
132	131	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
133	130, 132	oveq12d 6296	. . . . . . . . . . . . . . 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 3471	. . . . . . . . . . . . . 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 318	. . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . 14 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
137		eqid 2402	. . . . . . . . . . . . . 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 37336	. . . . . . . . . . . . 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 3117	. . . . . . . . . . . 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 820	. . . . . . . . . . 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 666	. . . . . . . . . 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 37267	. . . . . . . . 9 |- ( ph -> ( ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) /\ ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
143	142	simpld 457	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
144	57, 83, 77, 143, 127	lelttrd 9774	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
145	144	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
146	62	adantr 463	. . . . . . 7 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
147	142	simprd 461	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
148	147	adantr 463	. . . . . . 7 |- ( ( ph /\ -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
149		neqne 36810	. . . . . . . . 9 |- ( -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) -> ( E ` ( S ` ( J + 1 ) ) ) =/= ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
150	149	necomd 2674	. . . . . . . 8 |- ( -. ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) =/= ( E ` ( S ` ( J + 1 ) ) ) )
151	150	adantl 464	. . . . . . 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 36864	. . . . . 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 36900	. . . . 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 5863	. . . . 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 17	. . . 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 2410	. . 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 3916	. 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 5718	. . . . . . . 8 |- ( F : RR --> CC -> dom F = RR )
160	158, 159	syl 17	. . . . . . 7 |- ( ph -> dom F = RR )
161	160	feq2d 5701	. . . . . 6 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
162	158, 161	mpbird 232	. . . . 5 |- ( ph -> F : dom F --> CC )
163		ioosscn 36896	. . . . . 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 11640	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
166	165, 160	syl5sseqr 3491	. . . . 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 10028	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
169	167, 168	syl5eqel 2494	. . . . . 6 |- ( ph -> U e. RR )
170	169	recnd 9652	. . . . 5 |- ( ph -> U e. CC )
171		eqid 2402	. . . . 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 36930	. . . . . 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 11640	. . . . . . 7 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
174	173, 160	syl5sseqr 3491	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
175	172, 174	eqsstr3d 3477	. . . . 5 |- ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
176		elioore 11612	. . . . . 6 |- ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
177	68, 66	resubcld 10028	. . . . . . . . . . . . . 14 |- ( ph -> ( B - A ) e. RR )
178	11, 177	syl5eqel 2494	. . . . . . . . . . . . 13 |- ( ph -> T e. RR )
179	178	recnd 9652	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
180	66, 68	posdifd 10179	. . . . . . . . . . . . . . 15 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
181	71, 180	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( B - A ) )
182	181, 11	syl6breqr 4435	. . . . . . . . . . . . 13 |- ( ph -> 0 < T )
183	182	gt0ne0d 10157	. . . . . . . . . . . 12 |- ( ph -> T =/= 0 )
184	170, 179, 183	divcan1d 10362	. . . . . . . . . . 11 |- ( ph -> ( ( U / T ) x. T ) = U )
185	184	eqcomd 2410	. . . . . . . . . 10 |- ( ph -> U = ( ( U / T ) x. T ) )
186	185	oveq2d 6294	. . . . . . . . 9 |- ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
187	186	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
188	187	fveq2d 5853	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
189	158	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
190	178	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> T e. RR )
191	77	recnd 9652	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
192	75	recnd 9652	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
193	191, 192	negsubdi2d 9983	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
194	193	eqcomd 2410	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
195	194	oveq1d 6293	. . . . . . . . . . 11 |- ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
196	167	oveq1i 6288	. . . . . . . . . . . 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 6286	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
201	200	oveq1d 6293	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
202	201	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
203	202	oveq1d 6293	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
204	199, 203	oveq12d 6296	. . . . . . . . . . . . . . . . 17 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
205	204	adantl 464	. . . . . . . . . . . . . . . 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 10028	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
207	206, 178, 183	redivcld 10413	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
208	207	flcld 11972	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
209	208	zred 11008	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
210	209, 178	remulcld 9654	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
211	75, 210	readdcld 9653	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
212	198, 205, 75, 211	fvmptd 5938	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
213	212	oveq1d 6293	. . . . . . . . . . . . . 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 11009	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
215	214, 179	mulcld 9646	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
216	192, 215	pncan2d 9969	. . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
218	217, 215	eqeltrd 2490	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
219	218, 179, 183	divnegd 10374	. . . . . . . . . . 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 2453	. . . . . . . . . 10 |- ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
221	217	oveq1d 6293	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
222	214, 179, 183	divcan4d 10367	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
223	221, 222	eqtrd 2443	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
224	223, 208	eqeltrd 2490	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
225	224	znegcld 11010	. . . . . . . . . 10 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
226	220, 225	eqeltrd 2490	. . . . . . . . 9 |- ( ph -> ( U / T ) e. ZZ )
227	226	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
228		simpr 459	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> y e. RR )
229		fourierdlem91.6	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
230	229	adantlr 713	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
231	189, 190, 227, 228, 230	fperiodmul 36873	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
232	188, 231	eqtrd 2443	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
233	176, 232	sylan2 472	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
234	6	simprrd 759	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
235		fveq2 5849	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
236		oveq1 6285	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
237	236	fveq2d 5853	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
238	235, 237	breq12d 4408	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
239	238	rspccva 3159	. . . . . . . 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 659	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
241	55	ancli 549	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
242		eleq1 2474	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
243	242	anbi2d 702	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
244	235, 237	oveq12d 6296	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
245	244	reseq2d 5094	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
246	244	oveq1d 6293	. . . . . . . . . . 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 2484	. . . . . . . . . 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 318	. . . . . . . . 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 3117	. . . . . . . 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 59	. . . . . . 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 1728	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
253		fourierdlem91.w	. . . . . . . . . . . . 13 |- W = ( i e. ( 0..^ M ) |-> L )
254		nfmpt1 4484	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> L )
255	253, 254	nfcxfr 2562	. . . . . . . . . . . 12 |- F/_ i W
256		nfcv 2564	. . . . . . . . . . . 12 |- F/_ i ( I ` ( S ` J ) )
257	255, 256	nffv 5856	. . . . . . . . . . 11 |- F/_ i ( W ` ( I ` ( S ` J ) ) )
258	257	nfel1 2580	. . . . . . . . . 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 1948	. . . . . . . . 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 483	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
261	260	3adant2 1016	. . . . . . . . . . . . 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 17	. . . . . . . . . . . 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 5849	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( W ` i ) = ( W ` ( I ` ( S ` J ) ) ) )
265	264	eqcomd 2410	. . . . . . . . . . . . . . 15 |- ( i = ( I ` ( S ` J ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
266	265	adantr 463	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
267	260	simprd 461	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
268		elex 3068	. . . . . . . . . . . . . . . 16 |- ( L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) -> L e. _V )
269	260, 262, 268	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> L e. _V )
270	253	fvmpt2 5941	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0..^ M ) /\ L e. _V ) -> ( W ` i ) = L )
271	267, 269, 270	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` i ) = L )
272	266, 271	eqtrd 2443	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = L )
273	272	3adant2 1016	. . . . . . . . . . . 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 6296	. . . . . . . . . . . . . 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 2410	. . . . . . . . . . . . 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 1018	. . . . . . . . . . . 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 2505	. . . . . . . . . . 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 1196	. . . . . . . . . 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 12	. . . . . . . . . 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 190	. . . . . . . . 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 3116	. . . . . . . 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 59	. . . . . . 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 2402	. . . . . . 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 2402	. . . . . . 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 37290	. . . . . 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 5123	. . . . . . 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 6293	. . . . . 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 2492	. . . . 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 37002	. . . 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 6289	. . . . . 6 |- ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
291	191, 192	pncan3d 9970	. . . . . 6 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` ( J + 1 ) ) )
292	290, 291	syl5eq 2455	. . . . 5 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
293	292	oveq2d 6294	. . . 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 2492	. . 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 6289	. . . . . . . . 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 36907	. . . . . . . . . . . . . . 15 |- ( ph -> ( C [,] D ) C_ RR )
298		ax-resscn 9579	. . . . . . . . . . . . . . 15 |- RR C_ CC
299	297, 298	syl6ss 3454	. . . . . . . . . . . . . 14 |- ( ph -> ( C [,] D ) C_ CC )
300	25, 44, 43	fourierdlem15 37272	. . . . . . . . . . . . . . 15 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
301	300, 53	ffvelrnd 6010	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` J ) e. ( C [,] D ) )
302	299, 301	sseldd 3443	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) e. CC )
303	192, 302	subcld 9967	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
304	83	recnd 9652	. . . . . . . . . . . 12 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
305	191, 303, 304	subsub23d 36847	. . . . . . . . . . 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 2410	. . . . . . . . 9 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
308	307	oveq1d 6293	. . . . . . . 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 9967	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
310	309, 192, 191	addsub12d 9990	. . . . . . . . 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