Theorem fourierdlem89 31819

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.f	. . . . . 6 |- ( ph -> F : RR --> CC )
2		fdm 5741	. . . . . . . 8 |- ( F : RR --> CC -> dom F = RR )
3	1, 2	syl 16	. . . . . . 7 |- ( ph -> dom F = RR )
4	3	feq2d 5724	. . . . . 6 |- ( ph -> ( F : dom F --> CC <-> F : RR --> CC ) )
5	1, 4	mpbird 232	. . . . 5 |- ( ph -> F : dom F --> CC )
6		ioosscn 31414	. . . . . 6 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC
7	6	a1i 11	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ CC )
8		ioossre 11598	. . . . . . 7 |- ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR
9	8	a1i 11	. . . . . 6 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR )
10	3	sseq2d 3537	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ dom F <-> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ RR ) )
11	9, 10	mpbird 232	. . . . 5 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ dom F )
12		ax-resscn 9561	. . . . . 6 |- RR C_ CC
13		fourierdlem89.u	. . . . . . 7 |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
14		fourierdlem89.t	. . . . . . . . . . . . . . 15 |- T = ( B - A )
15		fourierdlem89.p	. . . . . . . . . . . . . . 15 |- 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 ) ) ) } )
16		fourierdlem89.m	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
17		fourierdlem89.q	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( P ` M ) )
18		fourierdlem89.c	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR )
19		fourierdlem89.d	. . . . . . . . . . . . . . . 16 |- ( ph -> D e. ( C (,) +oo ) )
20		elioore 11571	. . . . . . . . . . . . . . . 16 |- ( D e. ( C (,) +oo ) -> D e. RR )
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> D e. RR )
22		elioo4g 11597	. . . . . . . . . . . . . . . . . 18 |- ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
23	19, 22	sylib 196	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
24	23	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C < D /\ D < +oo ) )
25	24	simpld 459	. . . . . . . . . . . . . . 15 |- ( ph -> C < D )
26		fourierdlem89.o	. . . . . . . . . . . . . . 15 |- 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 ) ) ) } )
27		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
28	27	eleq1d 2536	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
29	28	rexbidv 2978	. . . . . . . . . . . . . . . . 17 |- ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
30	29	cbvrabv 3117	. . . . . . . . . . . . . . . 16 |- { 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 }
31	30	uneq2i 3660	. . . . . . . . . . . . . . 15 |- ( { 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 } )
32		fourierdlem89.n	. . . . . . . . . . . . . . . 16 |- N = ( ( # ` H ) - 1 )
33		fourierdlem89.12	. . . . . . . . . . . . . . . . . 18 |- H = ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
34	33	fveq2i 5875	. . . . . . . . . . . . . . . . 17 |- ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) )
35	34	oveq1i 6305	. . . . . . . . . . . . . . . 16 |- ( ( # ` H ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
36	32, 35	eqtri 2496	. . . . . . . . . . . . . . 15 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
37		fourierdlem89.s	. . . . . . . . . . . . . . . 16 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
38		isoeq5 6218	. . . . . . . . . . . . . . . . . . 19 |- ( 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 } ) ) ) )
39	33, 38	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( 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 } ) ) )
40	39	ax-gen 1601	. . . . . . . . . . . . . . . . 17 |- A. f ( 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 } ) ) )
41		iotabi 5566	. . . . . . . . . . . . . . . . 17 |- ( A. f ( 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 } ) ) ) -> ( 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 } ) ) ) )
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( 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 } ) ) )
43	37, 42	eqtri 2496	. . . . . . . . . . . . . . 15 |- 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 } ) ) )
44	14, 15, 16, 17, 18, 21, 25, 26, 31, 36, 43	fourierdlem54 31784	. . . . . . . . . . . . . 14 |- ( 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 } ) ) ) )
45	44	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
46	45	simprd 463	. . . . . . . . . . . 12 |- ( ph -> S e. ( O ` N ) )
47	45	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> N e. NN )
48	26	fourierdlem2 31732	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) ) )
49	47, 48	syl 16	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
50	46, 49	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) )
51	50	simpld 459	. . . . . . . . . 10 |- ( ph -> S e. ( RR ^m ( 0 ... N ) ) )
52		elmapi 7452	. . . . . . . . . 10 |- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR )
53	51, 52	syl 16	. . . . . . . . 9 |- ( ph -> S : ( 0 ... N ) --> RR )
54		fourierdlem89.j	. . . . . . . . . 10 |- ( ph -> J e. ( 0..^ N ) )
55		fzofzp1 11889	. . . . . . . . . 10 |- ( J e. ( 0..^ N ) -> ( J + 1 ) e. ( 0 ... N ) )
56	54, 55	syl 16	. . . . . . . . 9 |- ( ph -> ( J + 1 ) e. ( 0 ... N ) )
57	53, 56	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( S ` ( J + 1 ) ) e. RR )
58	15, 16, 17	fourierdlem11 31741	. . . . . . . . . . . 12 |- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) )
59	58	simp1d 1008	. . . . . . . . . . 11 |- ( ph -> A e. RR )
60	59	rexrd 9655	. . . . . . . . . 10 |- ( ph -> A e. RR* )
61	58	simp2d 1009	. . . . . . . . . 10 |- ( ph -> B e. RR )
62		iocssre 11616	. . . . . . . . . 10 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
63	60, 61, 62	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( A (,] B ) C_ RR )
64	58	simp3d 1010	. . . . . . . . . . 11 |- ( ph -> A < B )
65		fourierdlem89.e	. . . . . . . . . . 11 |- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
66	59, 61, 64, 14, 65	fourierdlem4 31734	. . . . . . . . . 10 |- ( ph -> E : RR --> ( A (,] B ) )
67	66, 57	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. ( A (,] B ) )
68	63, 67	sseldd 3510	. . . . . . . 8 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR )
69	57, 68	resubcld 9999	. . . . . . 7 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR )
70	13, 69	syl5eqel 2559	. . . . . 6 |- ( ph -> U e. RR )
71	12, 70	sseldi 3507	. . . . 5 |- ( ph -> U e. CC )
72		eqid 2467	. . . . 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 ) }
73		ioossre 11598	. . . . . . . 8 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR
74	73	a1i 11	. . . . . . 7 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR )
75	3	sseq2d 3537	. . . . . . 7 |- ( ph -> ( ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F <-> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ RR ) )
76	74, 75	mpbird 232	. . . . . 6 |- ( ph -> ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F )
77	59, 61	iccssred 31426	. . . . . . . . 9 |- ( ph -> ( A [,] B ) C_ RR )
78		fourierdlem89.z	. . . . . . . . . . 11 |- Z = ( y e. ( A (,] B ) |-> if ( y = B , A , y ) )
79	59, 61, 64, 78	fourierdlem17 31747	. . . . . . . . . 10 |- ( ph -> Z : ( A (,] B ) --> ( A [,] B ) )
80		ssid 3528	. . . . . . . . . . . . 13 |- RR C_ RR
81	80	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ RR )
82		elfzofz 11823	. . . . . . . . . . . . . 14 |- ( J e. ( 0..^ N ) -> J e. ( 0 ... N ) )
83	54, 82	syl 16	. . . . . . . . . . . . 13 |- ( ph -> J e. ( 0 ... N ) )
84	53, 83	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ph -> ( S ` J ) e. RR )
85	81, 84	sseldd 3510	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. RR )
86	66, 85	ffvelrnd 6033	. . . . . . . . . 10 |- ( ph -> ( E ` ( S ` J ) ) e. ( A (,] B ) )
87	79, 86	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. ( A [,] B ) )
88	77, 87	sseldd 3510	. . . . . . . 8 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. RR )
89	88, 68, 70	iooshift 31449	. . . . . . 7 |- ( 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 ) } )
90	89	sseq1d 3536	. . . . . 6 |- ( ph -> ( ( ( ( Z ` ( E ` ( S ` J ) ) ) + U ) (,) ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) C_ dom F <-> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F ) )
91	76, 90	mpbid 210	. . . . 5 |- ( ph -> { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } C_ dom F )
92		simpl 457	. . . . . 6 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ph )
93	8	sseli 3505	. . . . . . 7 |- ( y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) -> y e. RR )
94	93	adantl 466	. . . . . 6 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> y e. RR )
95		id 22	. . . . . . . . . . . . 13 |- ( ph -> ph )
96	61, 59	resubcld 9999	. . . . . . . . . . . . . . . 16 |- ( ph -> ( B - A ) e. RR )
97	14, 96	syl5eqel 2559	. . . . . . . . . . . . . . 15 |- ( ph -> T e. RR )
98	59, 61	posdifd 10151	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
99	64, 98	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 < ( B - A ) )
100	14	eqcomi 2480	. . . . . . . . . . . . . . . . 17 |- ( B - A ) = T
101	100	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( B - A ) = T )
102	99, 101	breqtrd 4477	. . . . . . . . . . . . . . 15 |- ( ph -> 0 < T )
103	97, 102	elrpd 11266	. . . . . . . . . . . . . 14 |- ( ph -> T e. RR+ )
104	103	rpcnd 11270	. . . . . . . . . . . . 13 |- ( ph -> T e. CC )
105	95, 104	syl 16	. . . . . . . . . . . 12 |- ( ph -> T e. CC )
106	102	gt0ne0d 10129	. . . . . . . . . . . . 13 |- ( ph -> T =/= 0 )
107	95, 106	syl 16	. . . . . . . . . . . 12 |- ( ph -> T =/= 0 )
108	71, 105, 107	divcan1d 10333	. . . . . . . . . . 11 |- ( ph -> ( ( U / T ) x. T ) = U )
109	108	eqcomd 2475	. . . . . . . . . 10 |- ( ph -> U = ( ( U / T ) x. T ) )
110	109	oveq2d 6311	. . . . . . . . 9 |- ( ph -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
111	110	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + U ) = ( y + ( ( U / T ) x. T ) ) )
112	111	fveq2d 5876	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
113		eqidd 2468	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` ( y + ( ( U / T ) x. T ) ) ) )
114	1	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> F : RR --> CC )
115	95, 97	syl 16	. . . . . . . . 9 |- ( ph -> T e. RR )
116	115	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> T e. RR )
117	13	oveq1i 6305	. . . . . . . . . . . 12 |- ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T )
118	117	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( U / T ) = ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) )
119	68	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC )
120	57	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> ( S ` ( J + 1 ) ) e. CC )
121	119, 120	negsubdi2d 9958	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
122	121	eqcomd 2475	. . . . . . . . . . . 12 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) = -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) )
123	122	oveq1d 6310	. . . . . . . . . . 11 |- ( ph -> ( ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
124	65	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
125		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) )
126		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) )
127	126	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) )
128	127	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
129	128	oveq1d 6310	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
130	125, 129	oveq12d 6313	. . . . . . . . . . . . . . . . . 18 |- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
131	130	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
132	61, 57	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR )
133	132, 115, 107	redivcld 10384	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR )
134	133	flcld 11915	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ )
135	134	zred 10978	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR )
136	135, 115	remulcld 9636	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR )
137	57, 136	readdcld 9635	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR )
138	124, 131, 57, 137	fvmptd 5962	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) )
139	138	oveq1d 6310	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) )
140	12, 135	sseldi 3507	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. CC )
141	140, 105	mulcld 9628	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. CC )
142	120, 141	pncan2d 9944	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
143	139, 142	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) )
144	143, 141	eqeltrd 2555	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. CC )
145	144, 105, 107	divnegd 10345	. . . . . . . . . . . 12 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
146	145	eqcomd 2475	. . . . . . . . . . 11 |- ( ph -> ( -u ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
147	118, 123, 146	3eqtrd 2512	. . . . . . . . . 10 |- ( ph -> ( U / T ) = -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) )
148	143	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) )
149	140, 105, 107	divcan4d 10338	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
150		eqidd 2468	. . . . . . . . . . . . 13 |- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
151	148, 149, 150	3eqtrd 2512	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) )
152	151, 134	eqeltrd 2555	. . . . . . . . . . 11 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
153	152	znegcld 10980	. . . . . . . . . 10 |- ( ph -> -u ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) / T ) e. ZZ )
154	147, 153	eqeltrd 2555	. . . . . . . . 9 |- ( ph -> ( U / T ) e. ZZ )
155	154	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( U / T ) e. ZZ )
156		simpr 461	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> y e. RR )
157		fourierdlem89.per	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
158	157	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
159	114, 116, 155, 156, 158	fperiodmul 31404	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
160	112, 113, 159	3eqtrd 2512	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
161	92, 94, 160	syl2anc 661	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
162	15	fourierdlem2 31732	. . . . . . . . . . . . 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 ) ) ) ) ) )
163	16, 162	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
164	17, 163	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 ) ) ) ) )
165	164	simpld 459	. . . . . . . . . 10 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
166		elmapi 7452	. . . . . . . . . 10 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
167	165, 166	syl 16	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> RR )
168	95, 167	syl 16	. . . . . . . 8 |- ( ph -> Q : ( 0 ... M ) --> RR )
169		elfzofz 11823	. . . . . . . . . . 11 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
170	169	ssriv 3513	. . . . . . . . . 10 |- ( 0..^ M ) C_ ( 0 ... M )
171	170	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ M ) C_ ( 0 ... M ) )
172	95, 16	syl 16	. . . . . . . . . . . 12 |- ( ph -> M e. NN )
173	95, 17	syl 16	. . . . . . . . . . . 12 |- ( ph -> Q e. ( P ` M ) )
174		fourierdlem89.20	. . . . . . . . . . . 12 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
175	15, 172, 173, 14, 65, 78, 174	fourierdlem37 31767	. . . . . . . . . . 11 |- ( 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 ) ) } ) ) )
176	175	simpld 459	. . . . . . . . . 10 |- ( ph -> I : RR --> ( 0..^ M ) )
177	176, 84	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
178	171, 177	sseldd 3510	. . . . . . . 8 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
179	168, 178	ffvelrnd 6033	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
180		fzofzp1 11889	. . . . . . . . 9 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
181	177, 180	syl 16	. . . . . . . 8 |- ( ph -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
182	168, 181	ffvelrnd 6033	. . . . . . 7 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
183	164	simprd 463	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
184	183	simprd 463	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
185	15, 16, 17, 14, 65, 78, 174	fourierdlem37 31767	. . . . . . . . . 10 |- ( 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 ) ) } ) ) )
186	185	simpld 459	. . . . . . . . 9 |- ( ph -> I : RR --> ( 0..^ M ) )
187	186, 84	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
188		fveq2 5872	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
189		oveq1 6302	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
190	189	fveq2d 5876	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
191	188, 190	breq12d 4466	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
192	191	rspccva 3218	. . . . . . . 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 ) ) )
193	184, 187, 192	syl2anc 661	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
194	95, 187	jca 532	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
195		eleq1 2539	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
196	195	anbi2d 703	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
197	188, 190	oveq12d 6313	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
198	197	reseq2d 5279	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
199	197	oveq1d 6310	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
200	198, 199	eleq12d 2549	. . . . . . . . . 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 ) ) )
201	196, 200	imbi12d 320	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) ) ) )
202		fourierdlem89.fcn	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
203	201, 202	vtoclg 3176	. . . . . . . 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 ) ) )
204	187, 194, 203	sylc 60	. . . . . . 7 |- ( ph -> ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) e. ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -cn-> CC ) )
205		nfcv 2629	. . . . . . . . 9 |- F/_ i ( I ` ( S ` J ) )
206		nfv 1683	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
207		fourierdlem89.21	. . . . . . . . . . . . 13 |- V = ( i e. ( 0..^ M ) |-> R )
208		nfmpt1 4542	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> R )
209	207, 208	nfcxfr 2627	. . . . . . . . . . . 12 |- F/_ i V
210	209, 205	nffv 5879	. . . . . . . . . . 11 |- F/_ i ( V ` ( I ` ( S ` J ) ) )
211		nfcv 2629	. . . . . . . . . . 11 |- F/_ i ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) )
212	210, 211	nfel 2642	. . . . . . . . . 10 |- F/ i ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) )
213	206, 212	nfim 1867	. . . . . . . . 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 ) ) ) ) )
214	196	biimpar 485	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
215	214	3adant2 1015	. . . . . . . . . . . . 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 ) ) )
216		simp2 997	. . . . . . . . . . . . 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 ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) )
217	215, 216	mpd 15	. . . . . . . . . . . 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 ) ) )
218		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( i = ( I ` ( S ` J ) ) -> ( V ` i ) = ( V ` ( I ` ( S ` J ) ) ) )
219	218	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
220	219	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = ( V ` i ) )
221	214	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
222		fourierdlem89.limc	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
223		elex 3127	. . . . . . . . . . . . . . . . 17 |- ( R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) -> R e. _V )
224	214, 222, 223	3syl 20	. . . . . . . . . . . . . . . 16 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> R e. _V )
225	207	fvmpt2 5964	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0..^ M ) /\ R e. _V ) -> ( V ` i ) = R )
226	221, 224, 225	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` i ) = R )
227	220, 226	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
228	227	3adant2 1015	. . . . . . . . . . . . 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 ) ) ) -> ( V ` ( I ` ( S ` J ) ) ) = R )
229	198, 188	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
230	229	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
231	230	3ad2ant1 1017	. . . . . . . . . . . . 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 ) ) ) -> ( ( 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 ) ) )
232	228, 231	eleq12d 2549	. . . . . . . . . . . 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 ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) <-> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) )
233	217, 232	mpbird 232	. . . . . . . . . . 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 ) ) ) ) )
234	233	3exp 1195	. . . . . . . . . 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 ) ) ) ) ) ) )
235	222	a1ii 27	. . . . . . . . . 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 ) ) ) ) )
236	234, 235	impbid 191	. . . . . . . . 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 ) ) ) ) ) ) )
237	205, 213, 236, 222	vtoclgf 3174	. . . . . . . 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 ) ) ) ) ) )
238	187, 194, 237	sylc 60	. . . . . . 7 |- ( ph -> ( V ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( I ` ( S ` J ) ) ) ) )
239	50	simprd 463	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) )
240	239	simprd 463	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
241		fveq2 5872	. . . . . . . . . . . . 13 |- ( i = J -> ( S ` i ) = ( S ` J ) )
242		oveq1 6302	. . . . . . . . . . . . . 14 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
243	242	fveq2d 5876	. . . . . . . . . . . . 13 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
244	241, 243	breq12d 4466	. . . . . . . . . . . 12 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
245	244	rspccva 3218	. . . . . . . . . . 11 |- ( ( A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) /\ J e. ( 0..^ N ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
246	240, 54, 245	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
247		posdif 10057	. . . . . . . . . . 11 |- ( ( ( S ` J ) e. RR /\ ( S ` ( J + 1 ) ) e. RR ) -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
248	84, 57, 247	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
249	246, 248	mpbid 210	. . . . . . . . 9 |- ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
250	95, 54	jca 532	. . . . . . . . . . 11 |- ( ph -> ( ph /\ J e. ( 0..^ N ) ) )
251		eleq1 2539	. . . . . . . . . . . . . 14 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
252	251	anbi2d 703	. . . . . . . . . . . . 13 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
253		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
254	253	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
255	254	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
256		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( S ` j ) = ( S ` J ) )
257	256	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
258	257	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
259	255, 258	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
260	254, 256	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
261	259, 260	eqeq12d 2489	. . . . . . . . . . . . 13 |- ( 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 ) ) ) )
262	252, 261	imbi12d 320	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) )
263	14	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k x. T ) = ( k x. ( B - A ) )
264	263	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . 21 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
265	264	eleq1i 2544	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
266	265	rexbii 2969	. . . . . . . . . . . . . . . . . . 19 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
267	266	rgenw 2828	. . . . . . . . . . . . . . . . . 18 |- 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 )
268		rabbi 3045	. . . . . . . . . . . . . . . . . 18 |- ( 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 } )
269	267, 268	mpbi 208	. . . . . . . . . . . . . . . . 17 |- { 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 }
270	269	uneq2i 3660	. . . . . . . . . . . . . . . 16 |- ( { 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 } )
271	270	fveq2i 5875	. . . . . . . . . . . . . . 15 |- ( # ` ( { 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 } ) )
272	271	oveq1i 6305	. . . . . . . . . . . . . 14 |- ( ( # ` ( { 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 )
273	36, 272	eqtri 2496	. . . . . . . . . . . . 13 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
274		isoeq5 6218	. . . . . . . . . . . . . . . . 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 } ) -> ( 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 } ) ) ) )
275	270, 274	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( 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 } ) ) )
276	275	ax-gen 1601	. . . . . . . . . . . . . . 15 |- A. f ( 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 } ) ) )
277		iotabi 5566	. . . . . . . . . . . . . . 15 |- ( A. f ( 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 } ) ) ) -> ( 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 } ) ) ) )
278	276, 277	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 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 } ) ) )
279	43, 278	eqtri 2496	. . . . . . . . . . . . 13 |- 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 } ) ) )
280		eqid 2467	. . . . . . . . . . . . 13 |- ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
281	15, 14, 16, 17, 18, 19, 26, 273, 279, 65, 78, 280	fourierdlem65 31795	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
282	262, 281	vtoclg 3176	. . . . . . . . . . 11 |- ( J e. ( 0..^ N ) -> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
283	54, 250, 282	sylc 60	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
284	283	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
285	249, 284	breqtrd 4477	. . . . . . . 8 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
286	88, 68	posdifd 10151	. . . . . . . 8 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
287	285, 286	mpbird 232	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
288		simpr 461	. . . . . . . . 9 |- ( ( ph /\ J e. ( 0..^ N ) ) -> J e. ( 0..^ N ) )
289	258, 255	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
290	256	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
291	290	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
292	290	oveq1d 6310	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
293	292	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
294	291, 293	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
295	289, 294	sseq12d 3538	. . . . . . . . . . 11 |- ( 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 ) ) ) ) )
296	252, 295	imbi12d 320	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
297		eqid 2467	. . . . . . . . . . 11 |- ( ( 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 ) ) )
298	14, 15, 16, 17, 18, 21, 25, 26, 31, 36, 43, 65, 78, 297, 174	fourierdlem79 31809	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) )
299	296, 298	vtoclg 3176	. . . . . . . . 9 |- ( 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 ) ) ) ) )
300	288, 299	mpcom 36	. . . . . . . 8 |- ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
301	95, 54, 300	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
302		eqid 2467	. . . . . . 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 ) ) ) ) )
303		eqid 2467	. . . . . . 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 ) ) ) )
304	179, 182, 193, 204, 238, 88, 68, 287, 301, 302, 303	fourierdlem32 31762	. . . . . 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 ) ) ) ) )
305		resabs1 5308	. . . . . . . 8 |- ( ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) -> ( ( 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 ) ) ) ) ) )
306	301, 305	syl 16	. . . . . . 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 ) ) ) ) ) )
307	306	oveq1d 6310	. . . . . 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 ) ) ) ) )
308	304, 307	eleqtrd 2557	. . . . 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 ) ) ) ) )
309	5, 7, 11, 71, 72, 91, 161, 308	limcperiod 31493	. . . 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 ) ) )
310	13	oveq2i 6306	. . . . . . 7 |- ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
311	310	a1i 11	. . . . . 6 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) + U ) = ( ( Z ` ( E ` ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
312	18, 21	iccssred 31426	. . . . . . . . . . . . 13 |- ( ph -> ( C [,] D ) C_ RR )
313	12	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> RR C_ CC )
314	312, 313	sstrd 3519	. . . . . . . . . . . 12 |- ( ph -> ( C [,] D ) C_ CC )
315	26, 47, 46	fourierdlem15 31745	. . . . . . . . . . . . 13 |- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
316	315, 83	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ph -> ( S ` J ) e. ( C [,] D ) )
317	314, 316	sseldd 3510	. . . . . . . . . . 11 |- ( ph -> ( S ` J ) e. CC )
318	120, 317	subcld 9942	. . . . . . . . . 10 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) e. CC )
319	88	recnd 9634	. . . . . . . . . 10 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) e. CC )
320	119, 318, 319	subsub23d 31374	. . . . . . . . 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 ) ) ) )
321	283, 320	mpbird 232	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
322	321	eqcomd 2475	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
323	322	oveq1d 6310	. . . . . 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 ) ) ) ) ) )
324	321, 319	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) e. CC )
325	324, 120, 119	addsub12d 9965	. . . . . . 7 |- ( ph -> ( ( ( E ` ( S ` ( J + 1 ) ) ) - ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` (