Theorem fourierdlem91 31821

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem fourierdlem91

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem91.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		fourierdlem91.u	. . . . . . 7 |- U = ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) )
14		fourierdlem91.t	. . . . . . . . . . . . . . 15 |- T = ( B - A )
15		fourierdlem91.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		fourierdlem91.m	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
17		fourierdlem91.q	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( P ` M ) )
18		fourierdlem91.c	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR )
19		fourierdlem91.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		fourierdlem91.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		fourierdlem91.n	. . . . . . . . . . . . . . . 16 |- N = ( ( # ` H ) - 1 )
33		fourierdlem91.h	. . . . . . . . . . . . . . . . . 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		fourierdlem91.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		fourierdlem91.17	. . . . . . . . . 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		fourierdlem91.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		fourierdlem91.J	. . . . . . . . . . 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	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> T = ( B - A ) )
101	100	eqcomd 2475	. . . . . . . . . . . . . . . 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		fourierdlem91.6	. . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
158	157	idi 2	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
159	158	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
160	114, 116, 155, 156, 159	fperiodmul 31404	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + ( ( U / T ) x. T ) ) ) = ( F ` y ) )
161	112, 113, 160	3eqtrd 2512	. . . . . 6 |- ( ( ph /\ y e. RR ) -> ( F ` ( y + U ) ) = ( F ` y ) )
162	92, 94, 161	syl2anc 661	. . . . 5 |- ( ( ph /\ y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) -> ( F ` ( y + U ) ) = ( F ` y ) )
163	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 ) ) ) ) ) )
164	16, 163	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 ) ) ) ) ) )
165	17, 164	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 ) ) ) ) )
166	165	simpld 459	. . . . . . . . . 10 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
167		elmapi 7452	. . . . . . . . . 10 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
168	166, 167	syl 16	. . . . . . . . 9 |- ( ph -> Q : ( 0 ... M ) --> RR )
169	95, 168	syl 16	. . . . . . . 8 |- ( ph -> Q : ( 0 ... M ) --> RR )
170		elfzofz 11823	. . . . . . . . . . 11 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
171	170	ssriv 3513	. . . . . . . . . 10 |- ( 0..^ M ) C_ ( 0 ... M )
172	171	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ M ) C_ ( 0 ... M ) )
173	95, 16	syl 16	. . . . . . . . . . . 12 |- ( ph -> M e. NN )
174	95, 17	syl 16	. . . . . . . . . . . 12 |- ( ph -> Q e. ( P ` M ) )
175		fourierdlem91.i	. . . . . . . . . . . 12 |- I = ( x e. RR |-> sup ( { i e. ( 0..^ M ) | ( Q ` i ) <_ ( Z ` ( E ` x ) ) } , RR , < ) )
176	15, 173, 174, 14, 65, 78, 175	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 ) ) } ) ) )
177	176	simpld 459	. . . . . . . . . 10 |- ( ph -> I : RR --> ( 0..^ M ) )
178	177, 84	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
179	172, 178	sseldd 3510	. . . . . . . 8 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0 ... M ) )
180	169, 179	ffvelrnd 6033	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) e. RR )
181		fzofzp1 11889	. . . . . . . . 9 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
182	178, 181	syl 16	. . . . . . . 8 |- ( ph -> ( ( I ` ( S ` J ) ) + 1 ) e. ( 0 ... M ) )
183	169, 182	ffvelrnd 6033	. . . . . . 7 |- ( ph -> ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) e. RR )
184	165	simprd 463	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
185	184	simprd 463	. . . . . . . 8 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
186	15, 16, 17, 14, 65, 78, 175	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 ) ) } ) ) )
187	186	simpld 459	. . . . . . . . 9 |- ( ph -> I : RR --> ( 0..^ M ) )
188	187, 84	ffvelrnd 6033	. . . . . . . 8 |- ( ph -> ( I ` ( S ` J ) ) e. ( 0..^ M ) )
189		fveq2 5872	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` i ) = ( Q ` ( I ` ( S ` J ) ) ) )
190		oveq1 6302	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
191	190	fveq2d 5876	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
192	189, 191	breq12d 4466	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
193	192	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 ) ) )
194	185, 188, 193	syl2anc 661	. . . . . . 7 |- ( ph -> ( Q ` ( I ` ( S ` J ) ) ) < ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
195	95, 188	jca 532	. . . . . . . 8 |- ( ph -> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
196		eleq1 2539	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( i e. ( 0..^ M ) <-> ( I ` ( S ` J ) ) e. ( 0..^ M ) ) )
197	196	anbi2d 703	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) )
198	189, 191	oveq12d 6313	. . . . . . . . . . . 12 |- ( i = ( I ` ( S ` J ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
199	198	reseq2d 5279	. . . . . . . . . . 11 |- ( i = ( I ` ( S ` J ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
200	198	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 ) )
201	199, 200	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 ) ) )
202	197, 201	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 ) ) ) )
203		fourierdlem91.fcn	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
204	202, 203	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 ) ) )
205	188, 195, 204	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 ) )
206		nfcv 2629	. . . . . . . . 9 |- F/_ i ( I ` ( S ` J ) )
207		nfv 1683	. . . . . . . . . 10 |- F/ i ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) )
208		fourierdlem91.w	. . . . . . . . . . . . 13 |- W = ( i e. ( 0..^ M ) |-> L )
209		nfmpt1 4542	. . . . . . . . . . . . 13 |- F/_ i ( i e. ( 0..^ M ) |-> L )
210	208, 209	nfcxfr 2627	. . . . . . . . . . . 12 |- F/_ i W
211	210, 206	nffv 5879	. . . . . . . . . . 11 |- F/_ i ( W ` ( I ` ( S ` J ) ) )
212		nfcv 2629	. . . . . . . . . . 11 |- F/_ i ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
213	211, 212	nfel 2642	. . . . . . . . . 10 |- F/ i ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
214	207, 213	nfim 1867	. . . . . . . . 9 |- F/ i ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
215	197	biimpar 485	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
216	215	3adant2 1015	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ph /\ i e. ( 0..^ M ) ) )
217		simp2 997	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) )
218	216, 217	mpd 15	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
219		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( i = ( I ` ( S ` J ) ) -> ( W ` i ) = ( W ` ( I ` ( S ` J ) ) ) )
220	219	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( i = ( I ` ( S ` J ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
221	220	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = ( W ` i ) )
222	215	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> i e. ( 0..^ M ) )
223		fourierdlem91.l	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
224		elex 3127	. . . . . . . . . . . . . . . . 17 |- ( L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) -> L e. _V )
225	215, 223, 224	3syl 20	. . . . . . . . . . . . . . . 16 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> L e. _V )
226	208	fvmpt2 5964	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0..^ M ) /\ L e. _V ) -> ( W ` i ) = L )
227	222, 225, 226	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` i ) = L )
228	221, 227	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = L )
229	228	3adant2 1015	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) = L )
230	199, 191	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
231	230	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( i = ( I ` ( S ` J ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
232	231	3ad2ant1 1017	. . . . . . . . . . . . 13 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
233	229, 232	eleq12d 2549	. . . . . . . . . . . 12 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) <-> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) )
234	218, 233	mpbird 232	. . . . . . . . . . 11 |- ( ( i = ( I ` ( S ` J ) ) /\ ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) /\ ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
235	234	3exp 1195	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
236	223	a1ii 27	. . . . . . . . . 10 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) -> ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) ) )
237	235, 236	impbid 191	. . . . . . . . 9 |- ( i = ( I ` ( S ` J ) ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) <-> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ) )
238	206, 214, 237, 223	vtoclgf 3174	. . . . . . . 8 |- ( ( I ` ( S ` J ) ) e. ( 0..^ M ) -> ( ( ph /\ ( I ` ( S ` J ) ) e. ( 0..^ M ) ) -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) )
239	188, 195, 238	sylc 60	. . . . . . 7 |- ( ph -> ( W ` ( I ` ( S ` J ) ) ) e. ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) lim CC ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
240	50	simprd 463	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) )
241	240	simprd 463	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) )
242		fveq2 5872	. . . . . . . . . . . . 13 |- ( i = J -> ( S ` i ) = ( S ` J ) )
243		oveq1 6302	. . . . . . . . . . . . . 14 |- ( i = J -> ( i + 1 ) = ( J + 1 ) )
244	243	fveq2d 5876	. . . . . . . . . . . . 13 |- ( i = J -> ( S ` ( i + 1 ) ) = ( S ` ( J + 1 ) ) )
245	242, 244	breq12d 4466	. . . . . . . . . . . 12 |- ( i = J -> ( ( S ` i ) < ( S ` ( i + 1 ) ) <-> ( S ` J ) < ( S ` ( J + 1 ) ) ) )
246	245	rspccva 3218	. . . . . . . . . . 11 |- ( ( A. i e. ( 0..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) /\ J e. ( 0..^ N ) ) -> ( S ` J ) < ( S ` ( J + 1 ) ) )
247	241, 54, 246	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( S ` J ) < ( S ` ( J + 1 ) ) )
248		posdif 10057	. . . . . . . . . . 11 |- ( ( ( S ` J ) e. RR /\ ( S ` ( J + 1 ) ) e. RR ) -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
249	84, 57, 248	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( ( S ` J ) < ( S ` ( J + 1 ) ) <-> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
250	247, 249	mpbid 210	. . . . . . . . 9 |- ( ph -> 0 < ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
251		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ J e. ( 0..^ N ) ) -> J e. ( 0..^ N ) )
252		eleq1 2539	. . . . . . . . . . . . . . 15 |- ( j = J -> ( j e. ( 0..^ N ) <-> J e. ( 0..^ N ) ) )
253	252	anbi2d 703	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( ph /\ j e. ( 0..^ N ) ) <-> ( ph /\ J e. ( 0..^ N ) ) ) )
254		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( j + 1 ) = ( J + 1 ) )
255	254	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( S ` ( j + 1 ) ) = ( S ` ( J + 1 ) ) )
256	255	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( E ` ( S ` ( j + 1 ) ) ) = ( E ` ( S ` ( J + 1 ) ) ) )
257		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( j = J -> ( S ` j ) = ( S ` J ) )
258	257	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( j = J -> ( E ` ( S ` j ) ) = ( E ` ( S ` J ) ) )
259	258	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( j = J -> ( Z ` ( E ` ( S ` j ) ) ) = ( Z ` ( E ` ( S ` J ) ) ) )
260	256, 259	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
261	255, 257	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( j = J -> ( ( S ` ( j + 1 ) ) - ( S ` j ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
262	260, 261	eqeq12d 2489	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
263	253, 262	imbi12d 320	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) )
264	14	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k x. T ) = ( k x. ( B - A ) )
265	264	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
266	265	eleq1i 2544	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
267	266	rexbii 2969	. . . . . . . . . . . . . . . . . . . 20 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
268	267	rgenw 2828	. . . . . . . . . . . . . . . . . . 19 |- 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 )
269		rabbi 3045	. . . . . . . . . . . . . . . . . . 19 |- ( 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 } )
270	268, 269	mpbi 208	. . . . . . . . . . . . . . . . . 18 |- { 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 }
271	270	uneq2i 3660	. . . . . . . . . . . . . . . . 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 } )
272	271	fveq2i 5875	. . . . . . . . . . . . . . . 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 } ) )
273	272	oveq1i 6305	. . . . . . . . . . . . . . 15 |- ( ( # ` ( { 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 )
274	36, 273	eqtri 2496	. . . . . . . . . . . . . 14 |- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
275		isoeq5 6218	. . . . . . . . . . . . . . . . . 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 } ) ) ) )
276	271, 275	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 } ) ) )
277	276	ax-gen 1601	. . . . . . . . . . . . . . . 16 |- 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 } ) ) )
278		iotabi 5566	. . . . . . . . . . . . . . . 16 |- ( 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 } ) ) ) )
279	277, 278	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( 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 } ) ) )
280	43, 279	eqtri 2496	. . . . . . . . . . . . . 14 |- 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 } ) ) )
281		eqid 2467	. . . . . . . . . . . . . 14 |- ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) ) = ( ( S ` j ) + ( B - ( E ` ( S ` j ) ) ) )
282	15, 14, 16, 17, 18, 19, 26, 274, 280, 65, 78, 281	fourierdlem65 31795	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( j + 1 ) ) ) - ( Z ` ( E ` ( S ` j ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( S ` j ) ) )
283	263, 282	vtoclg 3176	. . . . . . . . . . . 12 |- ( J e. ( 0..^ N ) -> ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) ) )
284	251, 283	mpcom 36	. . . . . . . . . . 11 |- ( ( ph /\ J e. ( 0..^ N ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
285	95, 54, 284	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) = ( ( S ` ( J + 1 ) ) - ( S ` J ) ) )
286	285	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( ( S ` ( J + 1 ) ) - ( S ` J ) ) = ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
287	250, 286	breqtrd 4477	. . . . . . . 8 |- ( ph -> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) )
288	88, 68	posdifd 10151	. . . . . . . 8 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) <-> 0 < ( ( E ` ( S ` ( J + 1 ) ) ) - ( Z ` ( E ` ( S ` J ) ) ) ) ) )
289	287, 288	mpbird 232	. . . . . . 7 |- ( ph -> ( Z ` ( E ` ( S ` J ) ) ) < ( E ` ( S ` ( J + 1 ) ) ) )
290	259, 256	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = J -> ( ( Z ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) )
291	257	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( j = J -> ( I ` ( S ` j ) ) = ( I ` ( S ` J ) ) )
292	291	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j = J -> ( Q ` ( I ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` J ) ) ) )
293	291	oveq1d 6310	. . . . . . . . . . . . . 14 |- ( j = J -> ( ( I ` ( S ` j ) ) + 1 ) = ( ( I ` ( S ` J ) ) + 1 ) )
294	293	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j = J -> ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) )
295	292, 294	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = J -> ( ( Q ` ( I ` ( S ` j ) ) ) (,) ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) ) = ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
296	290, 295	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 ) ) ) ) )
297	253, 296	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 ) ) ) ) ) )
298	33, 31	eqtri 2496	. . . . . . . . . . 11 |- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
299		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 ) ) )
300	14, 15, 16, 17, 18, 21, 25, 26, 298, 32, 37, 65, 78, 299, 175	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 ) ) ) )
301	297, 300	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 ) ) ) ) )
302	251, 301	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 ) ) ) )
303	95, 54, 302	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) C_ ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) )
304		eqid 2467	. . . . . . 7 |- if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) = if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) )
305		eqid 2467	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) u. { ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) u. { ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) } ) )
306	180, 183, 194, 205, 239, 88, 68, 289, 303, 304, 305	fourierdlem33 31763	. . . . . 6 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
307		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 ) ) ) ) ) )
308	303, 307	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 ) ) ) ) ) )
309	308	oveq1d 6310	. . . . . 6 |- ( ph -> ( ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) = ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
310	306, 309	eleqtrd 2557	. . . . 5 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) ) lim CC ( E ` ( S ` ( J + 1 ) ) ) ) )
311	5, 7, 11, 71, 72, 91, 162, 310	limcperiod 31493	. . . 4 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J ) ) ) , ( ( F |` ( ( Q ` ( I ` ( S ` J ) ) ) (,) ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) ) ) ` ( E ` ( S ` ( J + 1 ) ) ) ) ) e. ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) )
312	13	oveq2i 6306	. . . . . . 7 |- ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) )
313	312	a1i 11	. . . . . 6 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) )
314	119, 120	pncan3d 9945	. . . . . 6 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + ( ( S ` ( J + 1 ) ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) = ( S ` ( J + 1 ) ) )
315	313, 314	eqtrd 2508	. . . . 5 |- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) + U ) = ( S ` ( J + 1 ) ) )
316	315	oveq2d 6311	. . . 4 |- ( ph -> ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( ( E ` ( S ` ( J + 1 ) ) ) + U ) ) = ( ( F |` { x e. CC | E. y e. ( ( Z ` ( E ` ( S ` J ) ) ) (,) ( E ` ( S ` ( J + 1 ) ) ) ) x = ( y + U ) } ) lim CC ( S ` ( J + 1 ) ) ) )
317	311, 316	eleqtrd 2557	. . 3 |- ( ph -> if ( ( E ` ( S ` ( J + 1 ) ) ) = ( Q ` ( ( I ` ( S ` J ) ) + 1 ) ) , ( W ` ( I ` ( S ` J