Theorem fourierdlem89 37346

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

Hypotheses

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

Assertion

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

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, 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, V, 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)   R( x, y, f, i, k, m, p)   S( m)   T( m, p)   U( f, i, k, m, p)   E( m, p)   F( f, k, m, p)   H( x, y, f, i, k, m, p)   I( m, p)   J( f, k, m, p)   M( y, f, k)   O( x, y, f, i, k, m, p)   V( f, i, k, m, p)   Z( f, k, m, p)

Proof of Theorem fourierdlem89

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem89.q	. . . . . . . . . . . 12 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem89.m	. . . . . . . . . . . . 13 |- ( ph -> M e. NN )
3		fourierdlem89.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		fourierdlem89.t	. . . . . . . . . . . . 13 |- T = ( B - A )
12		fourierdlem89.e	. . . . . . . . . . . . 13 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
13		fourierdlem89.z	. . . . . . . . . . . . 13 |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
14		fourierdlem89.20	. . . . . . . . . . . . 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		fourierdlem89.c	. . . . . . . . . . . . . . . . . 18 |- ( ph -> C e. RR )
18		fourierdlem89.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		fourierdlem89.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		fourierdlem89.n	. . . . . . . . . . . . . . . . . . 19 |- N = ( ( # ` H ) - 1 )
32		fourierdlem89.12	. . . . . . . . . . . . . . . . . . . . 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		fourierdlem89.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		fourierdlem89.j	. . . . . . . . . . . . 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 /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( 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 /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
65	3, 2, 1	fourierdlem11 37268	. . . . . . . . . 10 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
66	65	simp1d 1009	. . . . . . . . 9 |- ( ph -> A e. RR )
67	65	simp2d 1010	. . . . . . . . 9 |- ( ph -> B e. RR )
68	66, 67	iccssred 36907	. . . . . . . 8 |- ( ph -> ( A [,] B ) C_ RR )
69	65	simp3d 1011	. . . . . . . . . 10 |- ( ph -> A < B )
70	66, 67, 69, 13	fourierdlem17 37274	. . . . . . . . 9 |- ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
71	66, 67, 69, 11, 12	fourierdlem4 37261	. . . . . . . . . 10 |- ( ph -> E : RR --> ( A (,] B ) )
72	71, 54	ffvelrnd 6010	. . . . . . . . 9 |- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
73	70, 72	ffvelrnd 6010	. . . . . . . 8 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
74	68, 73	sseldd 3443	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
75	74	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
76	57	adantr 463	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
77	66	rexrd 9673	. . . . . . . . . . . 12 |- ( ph -> A e. RR* )
78		iocssre 11658	. . . . . . . . . . . 12 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
79	77, 67, 78	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( A (,] B ) C_ RR )
80		fzofzp1 11946	. . . . . . . . . . . . . 14 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
81	51, 80	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
82	50, 81	ffvelrnd 6010	. . . . . . . . . . . 12 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
83	71, 82	ffvelrnd 6010	. . . . . . . . . . 11 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
84	79, 83	sseldd 3443	. . . . . . . . . 10 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
85	47	simprrd 759	. . . . . . . . . . . . . 14 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
86		fveq2 5849	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` i ) = ( S ` J ) )
87		oveq1 6285	. . . . . . . . . . . . . . . . 17 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
88	87	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
89	86, 88	breq12d 4408	. . . . . . . . . . . . . . 15 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
90	89	rspccva 3159	. . . . . . . . . . . . . 14 |- ( ( A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) /\ J e. ( 0..^ N ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
91	85, 51, 90	syl2anc 659	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
92	54, 82	posdifd 10179	. . . . . . . . . . . . 13 |- ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
93	91, 92	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
94	51	ancli 549	. . . . . . . . . . . . 13 |- ( ph -> ( ph /\ J e. ( 0..^ N ) ) )
95		eleq1 2474	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
96	95	anbi2d 702	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
97		oveq1 6285	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
98	97	fveq2d 5853	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
99	98	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
100		fveq2 5849	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( S ` j ) = ( S ` J ) )
101	100	fveq2d 5853	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
102	101	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
103	99, 102	oveq12d 6296	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
104	98, 100	oveq12d 6296	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
105	103, 104	eqeq12d 2424	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
106	96, 105	imbi12d 318	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) )
107	11	oveq2i 6289	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k x. T ) = ( k x. ( B - A ) )
108	107	oveq2i 6289	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
109	108	eleq1i 2479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
110	109	rexbii 2906	. . . . . . . . . . . . . . . . . . . . 21 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
111	110	rgenw 2765	. . . . . . . . . . . . . . . . . . . 20 |- 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 )
112		rabbi 2986	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 } )
113	111, 112	mpbi 208	. . . . . . . . . . . . . . . . . . 19 |- { 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 }
114	113	uneq2i 3594	. . . . . . . . . . . . . . . . . 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 } )
115	114	fveq2i 5852	. . . . . . . . . . . . . . . . 17 |- ( # ` ( { 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 } ) )
116	115	oveq1i 6288	. . . . . . . . . . . . . . . 16 |- ( ( # ` ( { 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 )
117	35, 116	eqtri 2431	. . . . . . . . . . . . . . 15 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
118		isoeq5 6202	. . . . . . . . . . . . . . . . . 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 } ) -> ( 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 } ) ) ) )
119	114, 118	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( 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 } ) ) )
120	119	iotabii 5555	. . . . . . . . . . . . . . . 16 |- ( 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 } ) ) )
121	40, 120	eqtri 2431	. . . . . . . . . . . . . . 15 |- 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 } ) ) )
122		eqid 2402	. . . . . . . . . . . . . . 15 |- ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
123	3, 11, 2, 1, 17, 18, 25, 117, 121, 12, 13, 122	fourierdlem65 37322	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
124	106, 123	vtoclg 3117	. . . . . . . . . . . . 13 |- ( J e. ( 0..^ N ) -> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
125	51, 94, 124	sylc 59	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
126	93, 125	breqtrrd 4421	. . . . . . . . . . 11 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
127	74, 84	posdifd 10179	. . . . . . . . . . 11 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
128	126, 127	mpbird 232	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
129		id 22	. . . . . . . . . . 11 |- ( ph -> ph )
130	102, 99	oveq12d 6296	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
131	100	fveq2d 5853	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
132	131	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
133	131	oveq1d 6293	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
134	133	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
135	132, 134	oveq12d 6296	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
136	130, 135	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 ) ) ) ) )
137	96, 136	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 ) ) ) ) ) )
138		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 ) ) )
139	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40, 12, 13, 138, 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 ) ) ) )
140	137, 139	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 ) ) ) ) )
141	140	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 ) ) ) )
142	129, 51, 141	syl2anc 659	. . . . . . . . . 10 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
143	57, 62, 74, 84, 128, 142	fourierdlem10 37267	. . . . . . . . 9 |- ( ph -> ( ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) /\ ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
144	143	simpld 457	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
145	144	adantr 463	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
146		neqne 36810	. . . . . . . 8 |- ( -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
147	146	adantl 464	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
148	76, 75, 145, 147	leneltd 36864	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( Z ` ( E ` ( S ` J ) ) ) )
149	143	simprd 461	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
150	74, 84, 62, 128, 149	ltletrd 9776	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
151	150	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
152	59, 64, 75, 148, 151	eliood 36900	. . . . 5 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
153		fvres 5863	. . . . 5 |- ( ( Z ` ( E ` ( S ` J ) ) ) e. ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) )
154	152, 153	syl 17	. . . 4 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) )
155	154	eqcomd 2410	. . 3 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) )
156	155	ifeq2da 3916	. 2 |- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( F ` ( Z ` ( E ` ( S ` J ) ) ) ) ) = if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) )
157		fourierdlem89.f	. . . . . 6 |- ( ph -> F : RR --> CC )
158		fdm 5718	. . . . . . . 8 |- ( F : RR --> CC -> dom F = RR )
159	157, 158	syl 17	. . . . . . 7 |- ( ph -> dom F = RR )
160	159	feq2d 5701	. . . . . 6 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
161	157, 160	mpbird 232	. . . . 5 |- ( ph -> F : dom F --> CC )
162		ioosscn 36896	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC
163	162	a1i 11	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC )
164		ioossre 11640	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
165	164, 159	syl5sseqr 3491	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ dom F )
166		fourierdlem89.u	. . . . . . 7 |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
167	82, 84	resubcld 10028	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
168	166, 167	syl5eqel 2494	. . . . . 6 |- ( ph -> U e. RR )
169	168	recnd 9652	. . . . 5 |- ( ph -> U e. CC )
170		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 ) }
171	74, 84, 168	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 ) } )
172		ioossre 11640	. . . . . . 7 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
173	172, 159	syl5sseqr 3491	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
174	171, 173	eqsstr3d 3477	. . . . 5 |- ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
175		elioore 11612	. . . . . 6 |- ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
176	67, 66	resubcld 10028	. . . . . . . . . . . . . 14 |- ( ph -> ( B - A ) e. RR )
177	11, 176	syl5eqel 2494	. . . . . . . . . . . . 13 |- ( ph -> T e. RR )
178	177	recnd 9652	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
179	66, 67	posdifd 10179	. . . . . . . . . . . . . . 15 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
180	69, 179	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( B - A ) )
181	180, 11	syl6breqr 4435	. . . . . . . . . . . . 13 |- ( ph -> 0 < T )
182	181	gt0ne0d 10157	. . . . . . . . . . . 12 |- ( ph -> T =/= 0 )
183	169, 178, 182	divcan1d 10362	. . . . . . . . . . 11 |- ( ph -> ( ( U / T ) x. T ) = U )
184	183	eqcomd 2410	. . . . . . . . . 10 |- ( ph -> U = ( ( U / T ) x. T ) )
185	184	oveq2d 6294	. . . . . . . . 9 |- ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
186	185	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
187	186	fveq2d 5853	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
188	157	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
189	177	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> T e. RR )
190	84	recnd 9652	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
191	82	recnd 9652	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
192	190, 191	negsubdi2d 9983	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
193	192	eqcomd 2410	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
194	193	oveq1d 6293	. . . . . . . . . . 11 |- ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
195	166	oveq1i 6288	. . . . . . . . . . . 12 |- ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T )
196	195	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) )
197	12	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
198		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
199		oveq2 6286	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
200	199	oveq1d 6293	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
201	200	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
202	201	oveq1d 6293	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
203	198, 202	oveq12d 6296	. . . . . . . . . . . . . . . . 17 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
204	203	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
205	67, 82	resubcld 10028	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
206	205, 177, 182	redivcld 10413	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
207	206	flcld 11972	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
208	207	zred 11008	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
209	208, 177	remulcld 9654	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
210	82, 209	readdcld 9653	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
211	197, 204, 82, 210	fvmptd 5938	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
212	211	oveq1d 6293	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) )
213	208	recnd 9652	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
214	213, 178	mulcld 9646	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
215	191, 214	pncan2d 9969	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
216	212, 215	eqtrd 2443	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
217	216, 214	eqeltrd 2490	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
218	217, 178, 182	divnegd 10374	. . . . . . . . . . 11 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
219	194, 196, 218	3eqtr4d 2453	. . . . . . . . . 10 |- ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
220	216	oveq1d 6293	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
221	213, 178, 182	divcan4d 10367	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
222	220, 221	eqtrd 2443	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
223	222, 207	eqeltrd 2490	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
224	223	znegcld 11010	. . . . . . . . . 10 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
225	219, 224	eqeltrd 2490	. . . . . . . . 9 |- ( ph -> ( U / T ) e. ZZ )
226	225	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
227		simpr 459	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> y e. RR )
228		fourierdlem89.per	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
229	228	adantlr 713	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
230	188, 189, 226, 227, 229	fperiodmul 36873	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
231	187, 230	eqtrd 2443	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
232	175, 231	sylan2 472	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
233	6	simprrd 759	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
234		fveq2 5849	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
235		oveq1 6285	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
236	235	fveq2d 5853	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
237	234, 236	breq12d 4408	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
238	237	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 ) ) )
239	233, 55, 238	syl2anc 659	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
240	55	ancli 549	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
241		eleq1 2474	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
242	241	anbi2d 702	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
243	234, 236	oveq12d 6296	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
244	243	reseq2d 5094	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
245	243	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 ) )
246	244, 245	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 ) ) )
247	242, 246	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 ) ) ) )
248		fourierdlem89.fcn	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
249	247, 248	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 ) ) )
250	55, 240, 249	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 ) )
251		nfv 1728	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
252		fourierdlem89.21	. . . . . . . . . . . . 13 |- V = ( i e. ( 0..^ M ) |-> R )
253		nfmpt1 4484	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> R )
254	252, 253	nfcxfr 2562	. . . . . . . . . . . 12 |- F/_ i V
255		nfcv 2564	. . . . . . . . . . . 12 |- F/_ i ( I ` ( S ` J ) )
256	254, 255	nffv 5856	. . . . . . . . . . 11 |- F/_ i ( V ` ( I ` ( S ` J ) ) )
257	256	nfel1 2580	. . . . . . . . . 10 |- F/ i ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) )
258	251, 257	nfim 1948	. . . . . . . . 9 |- F/ i ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) )
259	242	biimpar 483	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
260	259	3adant2 1016	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
261		fourierdlem89.limc	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
262	260, 261	syl 17	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
263		fveq2 5849	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( V ` i ) = ( V ` ( I ` ( S ` J ) ) ) )
264	263	eqcomd 2410	. . . . . . . . . . . . . . 15 |- ( i = ( I ` ( S ` J ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
265	264	adantr 463	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
266	259	simprd 461	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
267		elex 3068	. . . . . . . . . . . . . . . 16 |- ( R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) -> R e. _V )
268	259, 261, 267	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> R e. _V )
269	252	fvmpt2 5941	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0..^ M ) /\ R e. _V ) -> ( V ` i ) = R )
270	266, 268, 269	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` i ) = R )
271	265, 270	eqtrd 2443	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
272	271	3adant2 1016	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
273	244, 234	oveq12d 6296	. . . . . . . . . . . . . 14 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) )
274	273	eqcomd 2410	. . . . . . . . . . . . 13 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
275	274	3ad2ant1 1018	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
276	262, 272, 275	3eltr4d 2505	. . . . . . . . . . 11 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) )
277	276	3exp 1196	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) ) ) )
278	261	a1ii 12	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) ) )
279	277, 278	impbid 190	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) ) ) )
280	258, 279, 261	vtoclg1f 3116	. . . . . . . 8 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) ) )
281	55, 240, 280	sylc 59	. . . . . . 7 |- ( ph -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) )
282		eqid 2402	. . . . . . 7 |- if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) = if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) )
283		eqid 2402	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( Q ` ( I ` ( S ` J ) ) ) [,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( Q ` ( I ` ( S ` J ) ) ) [,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
284	57, 62, 239, 250, 281, 74, 84, 128, 142, 282, 283	fourierdlem32 37289	. . . . . 6 |- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( Z ` ( E ` ( S ` J ) ) ) ) )
285	142	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 ) ) ) ) ) )
286	285	oveq1d 6293	. . . . . 6 |- ( ph -> ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( Z ` ( E ` ( S ` J ) ) ) ) )
287	284, 286	eleqtrd 2492	. . . . 5 |- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( Z ` ( E ` ( S ` J ) ) ) ) )
288	161, 163, 165, 169, 170, 174, 232, 287	limcperiod 37002	. . . 4 |- ( ph -> if ( ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) , ( V ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( Z ` ( E ` ( S ` J ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( Z ` ( E ` ( S ` J ) ) ) + U ) ) )
289	166	oveq2i 6289	. . . . . . 7 |- ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
290	289	a1i 11	. . . . . 6 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
291	17, 20	iccssred 36907	. . . . . . . . . . . . 13 |- ( ph -> ( C [,] D ) C_ RR )
292		ax-resscn 9579	. . . . . . . . . . . . 13 |- RR C_ CC
293	291, 292	syl6ss 3454	. . . . . . . . . . . 12 |- ( ph -> ( C [,] D ) C_ CC )
294	25, 44, 43	fourierdlem15 37272	. . . . . . . . . . . . 13 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
295	294, 53	ffvelrnd 6010	. . . . . . . . . . . 12 |- ( ph -> ( S ` J ) e. ( C [,] D ) )
296	293, 295	sseldd 3443	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. CC )
297	191, 296	subcld 9967	. . . . . . . . . 10 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
298	74	recnd 9652	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
299	190, 297, 298	subsub23d 36847	. . . . . . . . 9 |- ( 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 ) ) ) )
300	125, 299	mpbird 232	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
301	300	eqcomd 2410	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
302	301	oveq1d 6293	. . . . . 6 |- ( 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 ) ) ) ) ) )
303	190, 297	subcld 9967	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
304	303, 191, 190	addsub12d 9990	. . . . . . 7 |- ( 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 ` ( S ` ( J + 1 ) ) ) ) ) )
305	190, 297, 190	sub32d 9999	. . . . . . . . 9 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
306	190	subidd 9955	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = 0 )
307	306	oveq1d 6293	. . . . . . . . 9 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
308		df-neg 9844	. . . . . . . . . 10 |- -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
309	191, 296	negsubdi2d 9983	. . . . . . . . . 10 |- ( ph -> -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
310	308, 309	syl5eqr 2457	. . . . . . . . 9 |- ( ph -> ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
311	305, 307, 310	3eqtrd 2447	. . . . . . . 8 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
312	311	oveq2d 6294	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) )
313	191, 296	pncan3d 9970	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) = ( S ` J ) )
314	304, 312, 313	3eqtrd 2447	. . . . . 6 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` J ) )
315	290, 302, 314	3eqtrd 2447	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( S ` J ) )
316	315	oveq2d 6294	. . . 4 |- ( ph -> ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( Z ` ( E ` ( S ` J ) ) ) + U ) ) = ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( S ` J ) ) )
317	288, 316