Theorem fourierdlem112 38194

Description: Here abbreviations (local definitions) are introduced to prove the fourier 38201 theorem. ( Z ` m ) is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem112.f	|- ( ph -> F : RR --> RR )
fourierdlem112.d	|- D = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
fourierdlem112.p	|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem112.m	|- ( ph -> M e. NN )
fourierdlem112.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem112.n	|- N = ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
fourierdlem112.v	|- V = ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
fourierdlem112.x	|- ( ph -> X e. RR )
fourierdlem112.xran	|- ( ph -> X e. ran V )
fourierdlem112.t	|- T = ( 2 x. pi )
fourierdlem112.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem112.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem112.c	|- ( ( ph /\ i e. ( 0..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem112.u	|- ( ( ph /\ i e. ( 0..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
fourierdlem112.fdvcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem112.e	|- ( ph -> E e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) lim CC X ) )
fourierdlem112.i	|- ( ph -> I e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) lim CC X ) )
fourierdlem112.l	|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
fourierdlem112.r	|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
fourierdlem112.a	|- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
fourierdlem112.b	|- B = ( n e. NN |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / pi ) )
fourierdlem112.z	|- Z = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
fourierdlem112.23	|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
fourierdlem112.fbd	|- ( ph -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
fourierdlem112.fdvbd	|- ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
fourierdlem112.25	|- ( ph -> X e. RR )

Assertion

Ref	Expression
fourierdlem112	|- ( ph -> ( seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) /\ ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) ) )

Distinct variable groups:   A, k, m, n   B, k, m, n   t, C, m   x, C, m   D, i, k, m, n, x, y   i, F, t, z   y, F, t, k, m   z, k, m   n, F   w, F, i, t, z   x, F   i, L, t, z, k, m   n, L   w, L   f, M, i, t, y, m   n, M, x   M, p, i, n, y   i, N, t, w, z   f, N, y, m   n, N, p   x, N, f   Q, f, i, t, y, k, m   Q, n, x   Q, p, k   R, i, t, z, k, m   R, n   w, R   T, f, t, y, i, k, m   T, n, x   T, p   t, U, m   x, U   i, V, t, w, z   f, V, k, m   n, V, p   x, V   i, X, t, z   f, X, y, k, m   n, X, p   w, X   x, X   m, Z   ph, i, t, w, z   ph, f, k, m, y   ph, n   w, m   ph, x

Allowed substitution hints:   ph( p)   A( x, y, z, w, t, f, i, p)   B( x, y, z, w, t, f, i, p)   C( y, z, w, f, i, k, n, p)   D( z, w, t, f, p)   P( x, y, z, w, t, f, i, k, m, n, p)   Q( z, w)   R( x, y, f, p)   S( x, y, z, w, t, f, i, k, m, n, p)   T( z, w)   U( y, z, w, f, i, k, n, p)   E( x, y, z, w, t, f, i, k, m, n, p)   F( f, p)   I( x, y, z, w, t, f, i, k, m, n, p)   L( x, y, f, p)   M( z, w, k)   N( k)   V( y)   Z( x, y, z, w, t, f, i, k, n, p)

Proof of Theorem fourierdlem112

Dummy variables j l a s b e g c u q r v h d o are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem112.23	. . . . 5 |- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
2		fveq2 5879	. . . . . . . 8 |- ( n = j -> ( A ` n ) = ( A ` j ) )
3		oveq1 6315	. . . . . . . . 9 |- ( n = j -> ( n x. X ) = ( j x. X ) )
4	3	fveq2d 5883	. . . . . . . 8 |- ( n = j -> ( cos ` ( n x. X ) ) = ( cos ` ( j x. X ) ) )
5	2, 4	oveq12d 6326	. . . . . . 7 |- ( n = j -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) )
6		fveq2 5879	. . . . . . . 8 |- ( n = j -> ( B ` n ) = ( B ` j ) )
7	3	fveq2d 5883	. . . . . . . 8 |- ( n = j -> ( sin ` ( n x. X ) ) = ( sin ` ( j x. X ) ) )
8	6, 7	oveq12d 6326	. . . . . . 7 |- ( n = j -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) )
9	5, 8	oveq12d 6326	. . . . . 6 |- ( n = j -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
10	9	cbvmptv 4488	. . . . 5 |- ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
11	1, 10	eqtri 2493	. . . 4 |- S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
12		seqeq3 12256	. . . 4 |- ( S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) -> seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) )
13	11, 12	mp1i 13	. . 3 |- ( ph -> seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) )
14		nnuz 11218	. . . . 5 |- NN = ( ZZ>= ` 1 )
15		1zzd 10992	. . . . 5 |- ( ph -> 1 e. ZZ )
16		nfv 1769	. . . . . . 7 |- F/ n ph
17		nfcv 2612	. . . . . . . 8 |- F/_ n NN
18		nfcv 2612	. . . . . . . . 9 |- F/_ n ( -u pi (,) 0 )
19		nfcv 2612	. . . . . . . . . 10 |- F/_ n ( F ` ( X + s ) )
20		nfcv 2612	. . . . . . . . . 10 |- F/_ n x.
21		nfcv 2612	. . . . . . . . . 10 |- F/_ n ( ( D ` m ) ` s )
22	19, 20, 21	nfov 6334	. . . . . . . . 9 |- F/_ n ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) )
23	18, 22	nfitg 22811	. . . . . . . 8 |- F/_ n S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
24	17, 23	nfmpt 4484	. . . . . . 7 |- F/_ n ( m e. NN |-> S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
25		nfcv 2612	. . . . . . . . 9 |- F/_ n ( 0 (,) pi )
26	25, 22	nfitg 22811	. . . . . . . 8 |- F/_ n S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
27	17, 26	nfmpt 4484	. . . . . . 7 |- F/_ n ( m e. NN |-> S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
28		fourierdlem112.z	. . . . . . . 8 |- Z = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
29		fourierdlem112.a	. . . . . . . . . . . . 13 |- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
30		nfmpt1 4485	. . . . . . . . . . . . 13 |- F/_ n ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
31	29, 30	nfcxfr 2610	. . . . . . . . . . . 12 |- F/_ n A
32		nfcv 2612	. . . . . . . . . . . 12 |- F/_ n 0
33	31, 32	nffv 5886	. . . . . . . . . . 11 |- F/_ n ( A ` 0 )
34		nfcv 2612	. . . . . . . . . . 11 |- F/_ n /
35		nfcv 2612	. . . . . . . . . . 11 |- F/_ n 2
36	33, 34, 35	nfov 6334	. . . . . . . . . 10 |- F/_ n ( ( A ` 0 ) / 2 )
37		nfcv 2612	. . . . . . . . . 10 |- F/_ n +
38		nfcv 2612	. . . . . . . . . . 11 |- F/_ n ( 1 ... m )
39	38	nfsum1 13833	. . . . . . . . . 10 |- F/_ n sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
40	36, 37, 39	nfov 6334	. . . . . . . . 9 |- F/_ n ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
41	17, 40	nfmpt 4484	. . . . . . . 8 |- F/_ n ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
42	28, 41	nfcxfr 2610	. . . . . . 7 |- F/_ n Z
43		fourierdlem112.f	. . . . . . . 8 |- ( ph -> F : RR --> RR )
44		fourierdlem112.25	. . . . . . . 8 |- ( ph -> X e. RR )
45		eqid 2471	. . . . . . . 8 |- ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` n ) = ( pi + X ) ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` n ) = ( pi + X ) ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
46		picn 23493	. . . . . . . . . . . . 13 |- pi e. CC
47	46	2timesi 10753	. . . . . . . . . . . 12 |- ( 2 x. pi ) = ( pi + pi )
48		fourierdlem112.t	. . . . . . . . . . . 12 |- T = ( 2 x. pi )
49	46, 46	subnegi 9973	. . . . . . . . . . . 12 |- ( pi - -u pi ) = ( pi + pi )
50	47, 48, 49	3eqtr4i 2503	. . . . . . . . . . 11 |- T = ( pi - -u pi )
51		fourierdlem112.p	. . . . . . . . . . 11 |- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
52		fourierdlem112.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
53		fourierdlem112.q	. . . . . . . . . . 11 |- ( ph -> Q e. ( P ` M ) )
54		pire 23492	. . . . . . . . . . . . . 14 |- pi e. RR
55	54	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> pi e. RR )
56	55	renegcld 10067	. . . . . . . . . . . 12 |- ( ph -> -u pi e. RR )
57	56, 44	readdcld 9688	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR )
58	55, 44	readdcld 9688	. . . . . . . . . . 11 |- ( ph -> ( pi + X ) e. RR )
59		negpilt0 37580	. . . . . . . . . . . . . 14 |- -u pi < 0
60		pipos 23494	. . . . . . . . . . . . . 14 |- 0 < pi
61	54	renegcli 9955	. . . . . . . . . . . . . . 15 |- -u pi e. RR
62		0re 9661	. . . . . . . . . . . . . . 15 |- 0 e. RR
63	61, 62, 54	lttri 9778	. . . . . . . . . . . . . 14 |- ( ( -u pi < 0 /\ 0 < pi ) -> -u pi < pi )
64	59, 60, 63	mp2an 686	. . . . . . . . . . . . 13 |- -u pi < pi
65	64	a1i 11	. . . . . . . . . . . 12 |- ( ph -> -u pi < pi )
66	56, 55, 44, 65	ltadd1dd 10245	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
67		oveq1 6315	. . . . . . . . . . . . . . 15 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
68	67	eleq1d 2533	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
69	68	rexbidv 2892	. . . . . . . . . . . . 13 |- ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
70	69	cbvrabv 3030	. . . . . . . . . . . 12 |- { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { x e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
71	70	uneq2i 3576	. . . . . . . . . . 11 |- ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { x e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
72		fourierdlem112.n	. . . . . . . . . . 11 |- N = ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
73		fourierdlem112.v	. . . . . . . . . . 11 |- V = ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
74	50, 51, 52, 53, 57, 58, 66, 45, 71, 72, 73	fourierdlem54 38136	. . . . . . . . . 10 |- ( ph -> ( ( N e. NN /\ V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` n ) = ( pi + X ) ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) ) /\ V Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
75	74	simpld 466	. . . . . . . . 9 |- ( ph -> ( N e. NN /\ V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` n ) = ( pi + X ) ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) ) )
76	75	simpld 466	. . . . . . . 8 |- ( ph -> N e. NN )
77	75	simprd 470	. . . . . . . 8 |- ( ph -> V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u pi + X ) /\ ( p ` n ) = ( pi + X ) ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) )
78		fourierdlem112.xran	. . . . . . . 8 |- ( ph -> X e. ran V )
79	43	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> F : RR --> RR )
80		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` i ) = ( p ` j ) )
81		oveq1 6315	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
82	81	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
83	80, 82	breq12d 4408	. . . . . . . . . . . . . . 15 |- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
84	83	cbvralv 3005	. . . . . . . . . . . . . 14 |- ( A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) )
85	84	anbi2i 708	. . . . . . . . . . . . 13 |- ( ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
86	85	a1i 11	. . . . . . . . . . . 12 |- ( p e. ( RR ^m ( 0 ... n ) ) -> ( ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) ) )
87	86	rabbiia 3019	. . . . . . . . . . 11 |- { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) }
88	87	mpteq2i 4479	. . . . . . . . . 10 |- ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
89	51, 88	eqtri 2493	. . . . . . . . 9 |- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` n ) = pi ) /\ A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
90	52	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> M e. NN )
91	53	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> Q e. ( P ` M ) )
92		fourierdlem112.fper	. . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
93	92	adantlr 729	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
94		eleq1 2537	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
95	94	anbi2d 718	. . . . . . . . . . . 12 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
96		fveq2 5879	. . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
97	81	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
98	96, 97	oveq12d 6326	. . . . . . . . . . . . . 14 |- ( i = j -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
99	98	reseq2d 5111	. . . . . . . . . . . . 13 |- ( i = j -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
100	98	oveq1d 6323	. . . . . . . . . . . . 13 |- ( i = j -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
101	99, 100	eleq12d 2543	. . . . . . . . . . . 12 |- ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) )
102	95, 101	imbi12d 327	. . . . . . . . . . 11 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
103		fourierdlem112.fcn	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
104	102, 103	chvarv 2120	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
105	104	adantlr 729	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
106	57	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
107	57	rexrd 9708	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR* )
108		pnfxr 11435	. . . . . . . . . . . 12 |- +oo e. RR*
109	108	a1i 11	. . . . . . . . . . 11 |- ( ph -> +oo e. RR* )
110	58	ltpnfd 11446	. . . . . . . . . . 11 |- ( ph -> ( pi + X ) < +oo )
111	107, 109, 58, 66, 110	eliood 37691	. . . . . . . . . 10 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
112	111	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
113		id 22	. . . . . . . . . . 11 |- ( i e. ( 0..^ N ) -> i e. ( 0..^ N ) )
114	72	oveq2i 6319	. . . . . . . . . . 11 |- ( 0..^ N ) = ( 0..^ ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) )
115	113, 114	syl6eleq 2559	. . . . . . . . . 10 |- ( i e. ( 0..^ N ) -> i e. ( 0..^ ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
116	115	adantl 473	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> i e. ( 0..^ ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
117	72	oveq2i 6319	. . . . . . . . . . . 12 |- ( 0 ... N ) = ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) )
118		isoeq4 6231	. . . . . . . . . . . 12 |- ( ( 0 ... N ) = ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) -> ( f Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
119	117, 118	ax-mp 5	. . . . . . . . . . 11 |- ( f Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
120	119	iotabii 5575	. . . . . . . . . 10 |- ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
121	73, 120	eqtri 2493	. . . . . . . . 9 |- V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
122	79, 89, 50, 90, 91, 93, 105, 106, 112, 116, 121	fourierdlem98 38180	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
123		fourierdlem112.fbd	. . . . . . . . . 10 |- ( ph -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
124	123	adantr 472	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
125		nfra1 2785	. . . . . . . . . . 11 |- F/ t A. t e. RR ( abs ` ( F ` t ) ) <_ w
126		elioore 11691	. . . . . . . . . . . . 13 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> t e. RR )
127		rspa 2774	. . . . . . . . . . . . 13 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. RR ) -> ( abs ` ( F ` t ) ) <_ w )
128	126, 127	sylan2 482	. . . . . . . . . . . 12 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w )
129	128	ex 441	. . . . . . . . . . 11 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( F ` t ) ) <_ w ) )
130	125, 129	ralrimi 2800	. . . . . . . . . 10 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
131	130	reximi 2852	. . . . . . . . 9 |- ( E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
132	124, 131	syl 17	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
133		ssid 3437	. . . . . . . . . . . 12 |- RR C_ RR
134		dvfre 22984	. . . . . . . . . . . 12 |- ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
135	43, 133, 134	sylancl 675	. . . . . . . . . . 11 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
136	135	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
137		eqid 2471	. . . . . . . . . . . . 13 |- ( RR _D F ) = ( RR _D F )
138	54	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> pi e. RR )
139	61	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> -u pi e. RR )
140	98	reseq2d 5111	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
141	140, 100	eleq12d 2543	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) )
142	95, 141	imbi12d 327	. . . . . . . . . . . . . . 15 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
143		fourierdlem112.fdvcn	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
144	142, 143	chvarv 2120	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
145	144	adantlr 729	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
146		fourierdlem112.x	. . . . . . . . . . . . . . 15 |- ( ph -> X e. RR )
147	56, 146	readdcld 9688	. . . . . . . . . . . . . 14 |- ( ph -> ( -u pi + X ) e. RR )
148	147	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
149	147	rexrd 9708	. . . . . . . . . . . . . . 15 |- ( ph -> ( -u pi + X ) e. RR* )
150	55, 146	readdcld 9688	. . . . . . . . . . . . . . 15 |- ( ph -> ( pi + X ) e. RR )
151	56, 55, 146, 65	ltadd1dd 10245	. . . . . . . . . . . . . . 15 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
152	150	ltpnfd 11446	. . . . . . . . . . . . . . 15 |- ( ph -> ( pi + X ) < +oo )
153	149, 109, 150, 151, 152	eliood 37691	. . . . . . . . . . . . . 14 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
154	153	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
155		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = h -> ( k x. T ) = ( h x. T ) )
156	155	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = h -> ( y + ( k x. T ) ) = ( y + ( h x. T ) ) )
157	156	eleq1d 2533	. . . . . . . . . . . . . . . . . . . 20 |- ( k = h -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
158	157	cbvrexv 3006	. . . . . . . . . . . . . . . . . . 19 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
159	158	rgenw 2768	. . . . . . . . . . . . . . . . . 18 |- A. y e. ( ( -u pi + X ) [,] ( pi + X ) ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
160		rabbi 2955	. . . . . . . . . . . . . . . . . 18 |- ( A. y e. ( ( -u pi + X ) [,] ( pi + X ) ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) <-> { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
161	159, 160	mpbi 213	. . . . . . . . . . . . . . . . 17 |- { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q }
162	161	uneq2i 3576	. . . . . . . . . . . . . . . 16 |- ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
163		isoeq5 6232	. . . . . . . . . . . . . . . 16 |- ( ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) )
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
165	164	iotabii 5575	. . . . . . . . . . . . . 14 |- ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
166	121, 165	eqtri 2493	. . . . . . . . . . . . 13 |- V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u pi + X ) , ( pi + X ) } u. { y e. ( ( -u pi + X ) [,] ( pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
167		eleq1 2537	. . . . . . . . . . . . . . 15 |- ( v = u -> ( v e. dom ( RR _D F ) <-> u e. dom ( RR _D F ) ) )
168		fveq2 5879	. . . . . . . . . . . . . . 15 |- ( v = u -> ( ( RR _D F ) ` v ) = ( ( RR _D F ) ` u ) )
169	167, 168	ifbieq1d 3895	. . . . . . . . . . . . . 14 |- ( v = u -> if ( v e. dom ( RR _D F ) , ( ( RR _D F ) ` v ) , 0 ) = if ( u e. dom ( RR _D F ) , ( ( RR _D F ) ` u ) , 0 ) )
170	169	cbvmptv 4488	. . . . . . . . . . . . 13 |- ( v e. RR |-> if ( v e. dom ( RR _D F ) , ( ( RR _D F ) ` v ) , 0 ) ) = ( u e. RR |-> if ( u e. dom ( RR _D F ) , ( ( RR _D F ) ` u ) , 0 ) )
171	79, 137, 89, 138, 139, 50, 90, 91, 93, 145, 148, 154, 116, 166, 170	fourierdlem97 38179	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
172		cncff 22003	. . . . . . . . . . . 12 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
173		fdm 5745	. . . . . . . . . . . 12 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC -> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
174	171, 172, 173	3syl 18	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
175		ssdmres 5132	. . . . . . . . . . 11 |- ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
176	174, 175	sylibr 217	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
177	136, 176	fssresd 5762	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
178		ax-resscn 9614	. . . . . . . . . . 11 |- RR C_ CC
179	178	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> RR C_ CC )
180		cncffvrn 22008	. . . . . . . . . 10 |- ( ( RR C_ CC /\ ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) <-> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR ) )
181	179, 171, 180	syl2anc 673	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) <-> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR ) )
182	177, 181	mpbird 240	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
183		fourierdlem112.fdvbd	. . . . . . . . . . 11 |- ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
184	183	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
185		nfv 1769	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0..^ N ) )
186		nfra1 2785	. . . . . . . . . . . . . 14 |- F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
187	185, 186	nfan 2031	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
188		fvres 5893	. . . . . . . . . . . . . . . . . 18 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
189	188	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
190	189	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
191	190	adantlr 729	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
192		simplr 770	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
193	176	sselda 3418	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
194	193	adantlr 729	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
195		rspa 2774	. . . . . . . . . . . . . . . 16 |- ( ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z /\ t e. dom ( RR _D F ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
196	192, 194, 195	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
197	191, 196	eqbrtrd 4416	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
198	197	ex 441	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
199	187, 198	ralrimi 2800	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
200	199	ex 441	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
201	200	reximdv 2857	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
202	184, 201	mpd 15	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
203		nfra1 2785	. . . . . . . . . . . 12 |- F/ t A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z
204	188	eqcomd 2477	. . . . . . . . . . . . . . . 16 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( RR _D F ) ` t ) = ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) )
205	204	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
206	205	adantl 473	. . . . . . . . . . . . . 14 |- ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
207		rspa 2774	. . . . . . . . . . . . . 14 |- ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
208	206, 207	eqbrtrd 4416	. . . . . . . . . . . . 13 |- ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
209	208	ex 441	. . . . . . . . . . . 12 |- ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
210	203, 209	ralrimi 2800	. . . . . . . . . . 11 |- ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
211	210	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
212	211	reximdv 2857	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
213	202, 212	mpd 15	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
214		nfv 1769	. . . . . . . . . . . 12 |- F/ i ( ph /\ j e. ( 0..^ M ) )
215		nfcsb1v 3365	. . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ C
216	215	nfel1 2626	. . . . . . . . . . . 12 |- F/ i [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) )
217	214, 216	nfim 2023	. . . . . . . . . . 11 |- F/ i ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
218		csbeq1a 3358	. . . . . . . . . . . . 13 |- ( i = j -> C = [_ j / i ]_ C )
219	99, 96	oveq12d 6326	. . . . . . . . . . . . 13 |- ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
220	218, 219	eleq12d 2543	. . . . . . . . . . . 12 |- ( i = j -> ( C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) <-> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) ) )
221	95, 220	imbi12d 327	. . . . . . . . . . 11 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) ) ) )
222		fourierdlem112.c	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
223	217, 221, 222	chvar 2119	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
224	223	adantlr 729	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
225	79, 89, 50, 90, 91, 93, 105, 224, 106, 112, 116, 121	fourierdlem96 38178	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> if ( ( ( d e. ( -u pi (,] pi ) |-> if ( d = pi , -u pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { f e. ( 0..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u pi (,] pi ) |-> if ( d = pi , -u pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( ( j e. ( 0..^ M ) |-> [_ j / i ]_ C ) ` ( ( y e. RR |-> sup ( { f e. ( 0..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u pi (,] pi ) |-> if ( d = pi , -u pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( d e. ( -u pi (,] pi ) |-> if ( d = pi , -u pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
226		nfcsb1v 3365	. . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ U
227	226	nfel1 2626	. . . . . . . . . . . 12 |- F/ i [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) )
228	214, 227	nfim 2023	. . . . . . . . . . 11 |- F/ i ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
229		csbeq1a 3358	. . . . . . . . . . . . 13 |- ( i = j -> U = [_ j / i ]_ U )
230	99, 97	oveq12d 6326	. . . . . . . . . . . . 13 |- ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
231	229, 230	eleq12d 2543	. . . . . . . . . . . 12 |- ( i = j -> ( U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) <-> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) ) )
232	95, 231	imbi12d 327	. . . . . . . . . . 11 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) ) ) )
233		fourierdlem112.u	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
234	228, 232, 233	chvar 2119	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
235	234	adantlr 729	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
236	79, 89, 50, 90, 91, 93, 105, 235, 148, 154, 116, 121	fourierdlem99 38181	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> if ( ( ( e e. RR |-> ( e + ( ( |_ ` ( ( pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) = ( Q ` ( ( ( y e. RR |-> sup ( { h e. ( 0..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u pi (,] pi ) |-> if ( g = pi , -u pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) + 1 ) ) , ( ( j e. ( 0..^ M ) |-> [_ j / i ]_ U ) ` ( ( y e. RR |-> sup ( { h e. ( 0..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u pi (,] pi ) |-> if ( g = pi , -u pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
237		eqeq1 2475	. . . . . . . . . 10 |- ( g = s -> ( g = 0 <-> s = 0 ) )
238		oveq2 6316	. . . . . . . . . . . . 13 |- ( g = s -> ( X + g ) = ( X + s ) )
239	238	fveq2d 5883	. . . . . . . . . . . 12 |- ( g = s -> ( F ` ( X + g ) ) = ( F ` ( X + s ) ) )
240		breq2 4399	. . . . . . . . . . . . 13 |- ( g = s -> ( 0 < g <-> 0 < s ) )
241	240	ifbid 3894	. . . . . . . . . . . 12 |- ( g = s -> if ( 0 < g , R , L ) = if ( 0 < s , R , L ) )
242	239, 241	oveq12d 6326	. . . . . . . . . . 11 |- ( g = s -> ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) )
243		id 22	. . . . . . . . . . 11 |- ( g = s -> g = s )
244	242, 243	oveq12d 6326	. . . . . . . . . 10 |- ( g = s -> ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) )
245	237, 244	ifbieq2d 3897	. . . . . . . . 9 |- ( g = s -> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) ) )
246	245	cbvmptv 4488	. . . . . . . 8 |- ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) ) )
247		eqeq1 2475	. . . . . . . . . 10 |- ( o = s -> ( o = 0 <-> s = 0 ) )
248		id 22	. . . . . . . . . . 11 |- ( o = s -> o = s )
249		oveq1 6315	. . . . . . . . . . . . 13 |- ( o = s -> ( o / 2 ) = ( s / 2 ) )
250	249	fveq2d 5883	. . . . . . . . . . . 12 |- ( o = s -> ( sin ` ( o / 2 ) ) = ( sin ` ( s / 2 ) ) )
251	250	oveq2d 6324	. . . . . . . . . . 11 |- ( o = s -> ( 2 x. ( sin ` ( o / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
252	248, 251	oveq12d 6326	. . . . . . . . . 10 |- ( o = s -> ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
253	247, 252	ifbieq2d 3897	. . . . . . . . 9 |- ( o = s -> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
254	253	cbvmptv 4488	. . . . . . . 8 |- ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
255		fveq2 5879	. . . . . . . . . 10 |- ( r = s -> ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) = ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) )
256		fveq2 5879	. . . . . . . . . 10 |- ( r = s -> ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) = ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) )
257	255, 256	oveq12d 6326	. . . . . . . . 9 |- ( r = s -> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) = ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) ) )
258	257	cbvmptv 4488	. . . . . . . 8 |- ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) = ( s e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) ) )
259		oveq2 6316	. . . . . . . . . 10 |- ( d = s -> ( ( k + ( 1 / 2 ) ) x. d ) = ( ( k + ( 1 / 2 ) ) x. s ) )
260	259	fveq2d 5883	. . . . . . . . 9 |- ( d = s -> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
261	260	cbvmptv 4488	. . . . . . . 8 |- ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
262		fveq2 5879	. . . . . . . . . 10 |- ( z = s -> ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) = ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) )
263		fveq2 5879	. . . . . . . . . 10 |- ( z = s -> ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) = ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) )
264	262, 263	oveq12d 6326	. . . . . . . . 9 |- ( z = s -> ( ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) = ( ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) ) )
265	264	cbvmptv 4488	. . . . . . . 8 |- ( z e. ( -u pi [,] pi ) |-> ( ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) = ( s e. ( -u pi [,] pi ) |-> ( ( ( r e. ( -u pi [,] pi ) |-> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u pi [,] pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( ( d e. ( -u pi [,] pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) ) )
266		fveq2 5879	. . . . . . . . . . . . 13 |- ( m = n -> ( D ` m ) = ( D ` n ) )
267	266	fveq1d 5881	. . . . . . . . . . . 12 |- ( m = n -> ( ( D ` m ) ` s ) = ( ( D ` n ) ` s ) )
268	267