Theorem fourierdlem89 38096

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 38008	. . . . . . . . . . . . 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 215	. . . . . . . . . . 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 465	. . . . . . . . . 10 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		elmapi 7518	. . . . . . . . . 10 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
9	7, 8	syl 17	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> RR )
10		fzossfz 11968	. . . . . . . . . 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 38044	. . . . . . . . . . . 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 465	. . . . . . . . . . 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 11694	. . . . . . . . . . . . . . . . . . 19 |- ( D e. ( C (,) +oo ) -> D e. RR )
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D e. RR )
21		elioo4g 11723	. . . . . . . . . . . . . . . . . . . . 21 |- ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
22	18, 21	sylib 201	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
23	22	simprd 469	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( C < D /\ D < +oo ) )
24	23	simpld 465	. . . . . . . . . . . . . . . . . 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 6321	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
27	26	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
28	27	rexbidv 2912	. . . . . . . . . . . . . . . . . . . 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 3055	. . . . . . . . . . . . . . . . . . 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 3596	. . . . . . . . . . . . . . . . . 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 5890	. . . . . . . . . . . . . . . . . . . 20 |- ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
34	33	oveq1i 6324	. . . . . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . . . . . 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 6238	. . . . . . . . . . . . . . . . . . . . 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 5586	. . . . . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . . . . . 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 38061	. . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
43	42	simprd 469	. . . . . . . . . . . . . . 15 |- ( ph -> S e. ( O ` N ) )
44	42	simpld 465	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. NN )
45	25	fourierdlem2 38008	. . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . 13 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
49		elmapi 7518	. . . . . . . . . . . . 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 11965	. . . . . . . . . . . . 13 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
53	51, 52	syl 17	. . . . . . . . . . . 12 |- ( ph -> J e. ( 0 ... N ) )
54	50, 53	ffvelrnd 6045	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. RR )
55	16, 54	ffvelrnd 6045	. . . . . . . . . 10 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
56	10, 55	sseldi 3441	. . . . . . . . 9 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
57	9, 56	ffvelrnd 6045	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
58	57	rexrd 9715	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
59	58	adantr 471	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR* )
60		fzofzp1 12038	. . . . . . . . . 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 6045	. . . . . . . 8 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
63	62	rexrd 9715	. . . . . . 7 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
64	63	adantr 471	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR* )
65	3, 2, 1	fourierdlem11 38017	. . . . . . . . . 10 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
66	65	simp1d 1026	. . . . . . . . 9 |- ( ph -> A e. RR )
67	65	simp2d 1027	. . . . . . . . 9 |- ( ph -> B e. RR )
68	66, 67	iccssred 37639	. . . . . . . 8 |- ( ph -> ( A [,] B ) C_ RR )
69	65	simp3d 1028	. . . . . . . . . 10 |- ( ph -> A < B )
70	66, 67, 69, 13	fourierdlem17 38023	. . . . . . . . 9 |- ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
71	66, 67, 69, 11, 12	fourierdlem4 38010	. . . . . . . . . 10 |- ( ph -> E : RR --> ( A (,] B ) )
72	71, 54	ffvelrnd 6045	. . . . . . . . 9 |- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
73	70, 72	ffvelrnd 6045	. . . . . . . 8 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
74	68, 73	sseldd 3444	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
75	74	adantr 471	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
76	57	adantr 471	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
77	66	rexrd 9715	. . . . . . . . . . . 12 |- ( ph -> A e. RR* )
78		iocssre 11742	. . . . . . . . . . . 12 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
79	77, 67, 78	syl2anc 671	. . . . . . . . . . 11 |- ( ph -> ( A (,] B ) C_ RR )
80		fzofzp1 12038	. . . . . . . . . . . . . 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 6045	. . . . . . . . . . . 12 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
83	71, 82	ffvelrnd 6045	. . . . . . . . . . 11 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
84	79, 83	sseldd 3444	. . . . . . . . . 10 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
85	47	simprrd 772	. . . . . . . . . . . . . 14 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
86		fveq2 5887	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` i ) = ( S ` J ) )
87		oveq1 6321	. . . . . . . . . . . . . . . . 17 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
88	87	fveq2d 5891	. . . . . . . . . . . . . . . 16 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
89	86, 88	breq12d 4428	. . . . . . . . . . . . . . 15 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
90	89	rspccva 3160	. . . . . . . . . . . . . 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 671	. . . . . . . . . . . . 13 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
92	54, 82	posdifd 10227	. . . . . . . . . . . . 13 |- ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
93	91, 92	mpbid 215	. . . . . . . . . . . 12 |- ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
94	51	ancli 558	. . . . . . . . . . . . 13 |- ( ph -> ( ph /\ J e. ( 0..^ N ) ) )
95		eleq1 2527	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
96	95	anbi2d 715	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
97		oveq1 6321	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
98	97	fveq2d 5891	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
99	98	fveq2d 5891	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
100		fveq2 5887	. . . . . . . . . . . . . . . . . . 19 |- ( j = J -> ( S ` j ) = ( S ` J ) )
101	100	fveq2d 5891	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
102	101	fveq2d 5891	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
103	99, 102	oveq12d 6332	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
104	98, 100	oveq12d 6332	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
105	103, 104	eqeq12d 2476	. . . . . . . . . . . . . . 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 326	. . . . . . . . . . . . . 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 6325	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k x. T ) = ( k x. ( B - A ) )
108	107	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
109	108	eleq1i 2530	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
110	109	rexbii 2900	. . . . . . . . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . . . . 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 2980	. . . . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . . . 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 3596	. . . . . . . . . . . . . . . . . 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 5890	. . . . . . . . . . . . . . . . 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 6324	. . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . . 15 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
118		isoeq5 6238	. . . . . . . . . . . . . . . . . 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 5586	. . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . . 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 38072	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
124	106, 123	vtoclg 3118	. . . . . . . . . . . . 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 62	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
126	93, 125	breqtrrd 4442	. . . . . . . . . . 11 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
127	74, 84	posdifd 10227	. . . . . . . . . . 11 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
128	126, 127	mpbird 240	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
129		id 22	. . . . . . . . . . 11 |- ( ph -> ph )
130	102, 99	oveq12d 6332	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
131	100	fveq2d 5891	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
132	131	fveq2d 5891	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
133	131	oveq1d 6329	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
134	133	fveq2d 5891	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
135	132, 134	oveq12d 6332	. . . . . . . . . . . . . . 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 3472	. . . . . . . . . . . . . 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 326	. . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . 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 38086	. . . . . . . . . . . . 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 3118	. . . . . . . . . . . 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 833	. . . . . . . . . . 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 671	. . . . . . . . . 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 38016	. . . . . . . . 9 |- ( ph -> ( ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) /\ ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
144	143	simpld 465	. . . . . . . 8 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
145	144	adantr 471	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) <_ ( Z ` ( E ` ( S ` J ) ) ) )
146		neqne 2642	. . . . . . . 8 |- ( -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
147	146	adantl 472	. . . . . . 7 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Z ` ( E ` ( S ` J ) ) ) =/= ( Q ` ( I ` ( S ` J ) ) ) )
148	76, 75, 145, 147	leneltd 9814	. . . . . 6 |- ( ( ph /\ -. ( Z ` ( E ` ( S ` J ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) ) -> ( Q ` ( I ` ( S ` J ) ) ) < ( Z ` ( E ` ( S ` J ) ) ) )
149	143	simprd 469	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
150	74, 84, 62, 128, 149	ltletrd 9820	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
151	150	adantr 471	. . . . . 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 37632	. . . . 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 5901	. . . . 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 2467	. . 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 3923	. 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 5755	. . . . . . . 8 |- ( F : RR --> CC -> dom F = RR )
159	157, 158	syl 17	. . . . . . 7 |- ( ph -> dom F = RR )
160	159	feq2d 5736	. . . . . 6 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
161	157, 160	mpbird 240	. . . . 5 |- ( ph -> F : dom F --> CC )
162		ioosscn 37628	. . . . . 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 11724	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
165	164, 159	syl5sseqr 3492	. . . . 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 10074	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
168	166, 167	syl5eqel 2543	. . . . . 6 |- ( ph -> U e. RR )
169	168	recnd 9694	. . . . 5 |- ( ph -> U e. CC )
170		eqid 2461	. . . . 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 37660	. . . . . 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 11724	. . . . . . 7 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
173	172, 159	syl5sseqr 3492	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
174	171, 173	eqsstr3d 3478	. . . . 5 |- ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
175		elioore 11694	. . . . . 6 |- ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
176	67, 66	resubcld 10074	. . . . . . . . . . . . . 14 |- ( ph -> ( B - A ) e. RR )
177	11, 176	syl5eqel 2543	. . . . . . . . . . . . 13 |- ( ph -> T e. RR )
178	177	recnd 9694	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
179	66, 67	posdifd 10227	. . . . . . . . . . . . . . 15 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
180	69, 179	mpbid 215	. . . . . . . . . . . . . 14 |- ( ph -> 0 < ( B - A ) )
181	180, 11	syl6breqr 4456	. . . . . . . . . . . . 13 |- ( ph -> 0 < T )
182	181	gt0ne0d 10205	. . . . . . . . . . . 12 |- ( ph -> T =/= 0 )
183	169, 178, 182	divcan1d 10411	. . . . . . . . . . 11 |- ( ph -> ( ( U / T ) x. T ) = U )
184	183	eqcomd 2467	. . . . . . . . . 10 |- ( ph -> U = ( ( U / T ) x. T ) )
185	184	oveq2d 6330	. . . . . . . . 9 |- ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
186	185	adantr 471	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
187	186	fveq2d 5891	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
188	157	adantr 471	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
189	177	adantr 471	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> T e. RR )
190	84	recnd 9694	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
191	82	recnd 9694	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
192	190, 191	negsubdi2d 10027	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
193	192	eqcomd 2467	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
194	193	oveq1d 6329	. . . . . . . . . . 11 |- ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
195	166	oveq1i 6324	. . . . . . . . . . . 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 6322	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
200	199	oveq1d 6329	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
201	200	fveq2d 5891	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
202	201	oveq1d 6329	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
203	198, 202	oveq12d 6332	. . . . . . . . . . . . . . . . 17 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
204	203	adantl 472	. . . . . . . . . . . . . . . 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 10074	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
206	205, 177, 182	redivcld 10462	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
207	206	flcld 12065	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
208	207	zred 11068	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
209	208, 177	remulcld 9696	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
210	82, 209	readdcld 9695	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
211	197, 204, 82, 210	fvmptd 5976	. . . . . . . . . . . . . . 15 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
212	211	oveq1d 6329	. . . . . . . . . . . . . 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 9694	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
214	213, 178	mulcld 9688	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
215	191, 214	pncan2d 10013	. . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
217	216, 214	eqeltrd 2539	. . . . . . . . . . . 12 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
218	217, 178, 182	divnegd 10423	. . . . . . . . . . 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 2505	. . . . . . . . . 10 |- ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
220	216	oveq1d 6329	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
221	213, 178, 182	divcan4d 10416	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
222	220, 221	eqtrd 2495	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
223	222, 207	eqeltrd 2539	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
224	223	znegcld 11070	. . . . . . . . . 10 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
225	219, 224	eqeltrd 2539	. . . . . . . . 9 |- ( ph -> ( U / T ) e. ZZ )
226	225	adantr 471	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
227		simpr 467	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> y e. RR )
228		fourierdlem89.per	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
229	228	adantlr 726	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
230	188, 189, 226, 227, 229	fperiodmul 37559	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
231	187, 230	eqtrd 2495	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
232	175, 231	sylan2 481	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
233	6	simprrd 772	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
234		fveq2 5887	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
235		oveq1 6321	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
236	235	fveq2d 5891	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
237	234, 236	breq12d 4428	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
238	237	rspccva 3160	. . . . . . . 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 671	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
240	55	ancli 558	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
241		eleq1 2527	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
242	241	anbi2d 715	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
243	234, 236	oveq12d 6332	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
244	243	reseq2d 5123	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
245	243	oveq1d 6329	. . . . . . . . . . 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 2533	. . . . . . . . . 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 326	. . . . . . . . 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 3118	. . . . . . . 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 62	. . . . . . 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 1771	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
252		fourierdlem89.21	. . . . . . . . . . . . 13 |- V = ( i e. ( 0..^ M ) |-> R )
253		nfmpt1 4505	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> R )
254	252, 253	nfcxfr 2600	. . . . . . . . . . . 12 |- F/_ i V
255		nfcv 2602	. . . . . . . . . . . 12 |- F/_ i ( I ` ( S ` J ) )
256	254, 255	nffv 5894	. . . . . . . . . . 11 |- F/_ i ( V ` ( I ` ( S ` J ) ) )
257	256	nfel1 2616	. . . . . . . . . 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 2013	. . . . . . . . 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 492	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
260	259	3adant2 1033	. . . . . . . . . . . . 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 5887	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( V ` i ) = ( V ` ( I ` ( S ` J ) ) ) )
264	263	eqcomd 2467	. . . . . . . . . . . . . . 15 |- ( i = ( I ` ( S ` J ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
265	264	adantr 471	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
266	259	simprd 469	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
267		elex 3065	. . . . . . . . . . . . . . . 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 5979	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0..^ M ) /\ R e. _V ) -> ( V ` i ) = R )
270	266, 268, 269	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` i ) = R )
271	265, 270	eqtrd 2495	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
272	271	3adant2 1033	. . . . . . . . . . . 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 6332	. . . . . . . . . . . . . 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 2467	. . . . . . . . . . . . 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 1035	. . . . . . . . . . . 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 2554	. . . . . . . . . . 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 1214	. . . . . . . . . 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	2a1i 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 195	. . . . . . . . 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 3117	. . . . . . . 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 62	. . . . . . 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 2461	. . . . . . 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 2461	. . . . . . 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 38039	. . . . . 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 5152	. . . . . . 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 6329	. . . . . 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 2541	. . . . 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 37745	. . . 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 6325	. . . . . . 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 37639	. . . . . . . . . . . . 13 |- ( ph -> ( C [,] D ) C_ RR )
292		ax-resscn 9621	. . . . . . . . . . . . 13 |- RR C_ CC
293	291, 292	syl6ss 3455	. . . . . . . . . . . 12 |- ( ph -> ( C [,] D ) C_ CC )
294	25, 44, 43	fourierdlem15 38021	. . . . . . . . . . . . 13 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
295	294, 53	ffvelrnd 6045	. . . . . . . . . . . 12 |- ( ph -> ( S ` J ) e. ( C [,] D ) )
296	293, 295	sseldd 3444	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. CC )
297	191, 296	subcld 10011	. . . . . . . . . 10 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
298	74	recnd 9694	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
299	190, 297, 298	subsub23d 37537	. . . . . . . . 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 240	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
301	300	eqcomd 2467	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
302	301	oveq1d 6329	. . . . . 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 10011	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
304	303, 191, 190	addsub12d 10034	. . . . . . 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 10043	. . . . . . . . 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 9999	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = 0 )
307	306	oveq1d 6329	. . . . . . . . 9 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
308		df-neg 9888	. . . . . . . . . 10 |- -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
309	191, 296	negsubdi2d 10027	. . . . . . . . . 10 |- ( ph -> -u ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
310	308, 309	syl5eqr 2509	. . . . . . . . 9 |- ( ph -> ( 0 - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
311	305, 307, 310	3eqtrd 2499	. . . . . . . 8 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( S ` J ) - ( S ` ( J + 1 ) ) ) )
312	311	oveq2d 6330	. . . . . . 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 10014	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( S ` J ) - ( S ` ( J + 1 ) ) ) ) = ( S ` J ) )
314	304, 312, 313	3eqtrd 2499	. . . . . 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 2499	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( S ` J ) )
316	315	oveq2d 6330	. . . 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