Theorem fourierdlem112 31842

Description: Here abbreviations (local definitions) are introduced to prove the fourier 31849 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	. . . . . 6 |- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
2		fveq2 5872	. . . . . . . . 9 |- ( n = j -> ( A ` n ) = ( A ` j ) )
3		oveq1 6302	. . . . . . . . . 10 |- ( n = j -> ( n x. X ) = ( j x. X ) )
4	3	fveq2d 5876	. . . . . . . . 9 |- ( n = j -> ( cos ` ( n x. X ) ) = ( cos ` ( j x. X ) ) )
5	2, 4	oveq12d 6313	. . . . . . . 8 |- ( n = j -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) )
6		fveq2 5872	. . . . . . . . 9 |- ( n = j -> ( B ` n ) = ( B ` j ) )
7	3	fveq2d 5876	. . . . . . . . 9 |- ( n = j -> ( sin ` ( n x. X ) ) = ( sin ` ( j x. X ) ) )
8	6, 7	oveq12d 6313	. . . . . . . 8 |- ( n = j -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) )
9	5, 8	oveq12d 6313	. . . . . . 7 |- ( 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 4544	. . . . . 6 |- ( 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 2496	. . . . 5 |- S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
12		seqeq3 12092	. . . . 5 |- ( 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	ax-mp 5	. . . 4 |- seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) )
14	13	a1i 11	. . 3 |- ( ph -> seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) )
15		nnuz 11129	. . . . 5 |- NN = ( ZZ>= ` 1 )
16		1z 10906	. . . . . 6 |- 1 e. ZZ
17	16	a1i 11	. . . . 5 |- ( ph -> 1 e. ZZ )
18		nfv 1683	. . . . . . 7 |- F/ n ph
19		nfcv 2629	. . . . . . . 8 |- F/_ n NN
20		nfcv 2629	. . . . . . . . 9 |- F/_ n ( -u pi (,) 0 )
21		nfcv 2629	. . . . . . . . . 10 |- F/_ n ( F ` ( X + s ) )
22		nfcv 2629	. . . . . . . . . 10 |- F/_ n x.
23		nfcv 2629	. . . . . . . . . 10 |- F/_ n ( ( D ` m ) ` s )
24	21, 22, 23	nfov 6318	. . . . . . . . 9 |- F/_ n ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) )
25	20, 24	nfitg 22049	. . . . . . . 8 |- F/_ n S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
26	19, 25	nfmpt 4541	. . . . . . 7 |- F/_ n ( m e. NN |-> S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
27		nfcv 2629	. . . . . . . . 9 |- F/_ n ( 0 (,) pi )
28	27, 24	nfitg 22049	. . . . . . . 8 |- F/_ n S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
29	19, 28	nfmpt 4541	. . . . . . 7 |- F/_ n ( m e. NN |-> S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
30		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 ) ) ) ) ) )
31		fourierdlem112.a	. . . . . . . . . . . . 13 |- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
32		nfmpt1 4542	. . . . . . . . . . . . 13 |- F/_ n ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
33	31, 32	nfcxfr 2627	. . . . . . . . . . . 12 |- F/_ n A
34		nfcv 2629	. . . . . . . . . . . 12 |- F/_ n 0
35	33, 34	nffv 5879	. . . . . . . . . . 11 |- F/_ n ( A ` 0 )
36		nfcv 2629	. . . . . . . . . . 11 |- F/_ n /
37		nfcv 2629	. . . . . . . . . . 11 |- F/_ n 2
38	35, 36, 37	nfov 6318	. . . . . . . . . 10 |- F/_ n ( ( A ` 0 ) / 2 )
39		nfcv 2629	. . . . . . . . . 10 |- F/_ n +
40		nfcv 2629	. . . . . . . . . . 11 |- F/_ n ( 1 ... m )
41	40	nfsum1 13492	. . . . . . . . . 10 |- F/_ n sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
42	38, 39, 41	nfov 6318	. . . . . . . . 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 ) ) ) ) )
43	19, 42	nfmpt 4541	. . . . . . . 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 ) ) ) ) ) )
44	30, 43	nfcxfr 2627	. . . . . . 7 |- F/_ n Z
45		fourierdlem112.f	. . . . . . . 8 |- ( ph -> F : RR --> RR )
46		fourierdlem112.25	. . . . . . . 8 |- ( ph -> X e. RR )
47		eqid 2467	. . . . . . . 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 ) ) ) } )
48		ax-resscn 9561	. . . . . . . . . . . . . 14 |- RR C_ CC
49		pire 22718	. . . . . . . . . . . . . 14 |- pi e. RR
50	48, 49	sselii 3506	. . . . . . . . . . . . 13 |- pi e. CC
51		subneg 9880	. . . . . . . . . . . . 13 |- ( ( pi e. CC /\ pi e. CC ) -> ( pi - -u pi ) = ( pi + pi ) )
52	50, 50, 51	mp2an 672	. . . . . . . . . . . 12 |- ( pi - -u pi ) = ( pi + pi )
53	50	2timesi 10668	. . . . . . . . . . . . 13 |- ( 2 x. pi ) = ( pi + pi )
54	53	eqcomi 2480	. . . . . . . . . . . 12 |- ( pi + pi ) = ( 2 x. pi )
55		fourierdlem112.t	. . . . . . . . . . . . 13 |- T = ( 2 x. pi )
56	55	eqcomi 2480	. . . . . . . . . . . 12 |- ( 2 x. pi ) = T
57	52, 54, 56	3eqtrri 2501	. . . . . . . . . . 11 |- T = ( pi - -u pi )
58		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 ) ) ) } )
59		fourierdlem112.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
60		fourierdlem112.q	. . . . . . . . . . 11 |- ( ph -> Q e. ( P ` M ) )
61	49	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> pi e. RR )
62	61	renegcld 9998	. . . . . . . . . . . 12 |- ( ph -> -u pi e. RR )
63	62, 46	readdcld 9635	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR )
64	61, 46	readdcld 9635	. . . . . . . . . . 11 |- ( ph -> ( pi + X ) e. RR )
65		negpilt0 31362	. . . . . . . . . . . . . 14 |- -u pi < 0
66		pipos 22720	. . . . . . . . . . . . . 14 |- 0 < pi
67	49	renegcli 9892	. . . . . . . . . . . . . . 15 |- -u pi e. RR
68		0re 9608	. . . . . . . . . . . . . . 15 |- 0 e. RR
69	67, 68, 49	lttri 9722	. . . . . . . . . . . . . 14 |- ( ( -u pi < 0 /\ 0 < pi ) -> -u pi < pi )
70	65, 66, 69	mp2an 672	. . . . . . . . . . . . 13 |- -u pi < pi
71	70	a1i 11	. . . . . . . . . . . 12 |- ( ph -> -u pi < pi )
72	62, 61, 46, 71	ltadd1dd 10175	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
73		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
74	73	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
75	74	rexbidv 2978	. . . . . . . . . . . . 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 ) )
76	75	cbvrabv 3117	. . . . . . . . . . . 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 }
77	76	uneq2i 3660	. . . . . . . . . . 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 } )
78		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 )
79		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 } ) ) )
80	57, 58, 59, 60, 63, 64, 72, 47, 77, 78, 79	fourierdlem54 31784	. . . . . . . . . 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 } ) ) ) )
81	80	simpld 459	. . . . . . . . 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 ) ) )
82	81	simpld 459	. . . . . . . 8 |- ( ph -> N e. NN )
83	81	simprd 463	. . . . . . . 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 ) )
84		fourierdlem112.xran	. . . . . . . 8 |- ( ph -> X e. ran V )
85	45	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> F : RR --> RR )
86		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` i ) = ( p ` j ) )
87		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
88	87	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
89	86, 88	breq12d 4466	. . . . . . . . . . . . . . 15 |- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
90	89	cbvralv 3093	. . . . . . . . . . . . . 14 |- ( A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) )
91	90	anbi2i 694	. . . . . . . . . . . . 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 ) ) ) )
92	91	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 ) ) ) ) )
93	92	rabbiia 3107	. . . . . . . . . . 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 ) ) ) }
94	93	mpteq2i 4536	. . . . . . . . . 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 ) ) ) } )
95	58, 94	eqtri 2496	. . . . . . . . 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 ) ) ) } )
96	59	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> M e. NN )
97	60	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> Q e. ( P ` M ) )
98		fourierdlem112.fper	. . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
99	98	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
100		eleq1 2539	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
101	100	anbi2d 703	. . . . . . . . . . . 12 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
102		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
103	87	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
104	102, 103	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( i = j -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
105	104	reseq2d 5279	. . . . . . . . . . . . 13 |- ( i = j -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
106	104	oveq1d 6310	. . . . . . . . . . . . 13 |- ( i = j -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
107	105, 106	eleq12d 2549	. . . . . . . . . . . 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 ) ) )
108	101, 107	imbi12d 320	. . . . . . . . . . 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 ) ) ) )
109		fourierdlem112.fcn	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
110	108, 109	chvarv 1983	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
111	110	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
112	63	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
113	63	rexrd 9655	. . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR* )
114		pnfxr 11333	. . . . . . . . . . . 12 |- +oo e. RR*
115	114	a1i 11	. . . . . . . . . . 11 |- ( ph -> +oo e. RR* )
116	64	ltpnfd 31380	. . . . . . . . . . 11 |- ( ph -> ( pi + X ) < +oo )
117	113, 115, 64, 72, 116	eliood 31418	. . . . . . . . . 10 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
118	117	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
119		id 22	. . . . . . . . . . 11 |- ( i e. ( 0..^ N ) -> i e. ( 0..^ N ) )
120	78	oveq2i 6306	. . . . . . . . . . 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 ) )
121	119, 120	syl6eleq 2565	. . . . . . . . . 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 ) ) )
122	121	adantl 466	. . . . . . . . 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 ) ) )
123	78	oveq2i 6306	. . . . . . . . . . . 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 ) )
124		isoeq4 6217	. . . . . . . . . . . 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 } ) ) ) )
125	123, 124	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 } ) ) )
126	125	iotabii 5579	. . . . . . . . . 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 } ) ) )
127	79, 126	eqtri 2496	. . . . . . . . 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 } ) ) )
128	85, 95, 57, 96, 97, 99, 111, 112, 118, 122, 127	fourierdlem98 31828	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
129		fourierdlem112.fbd	. . . . . . . . . 10 |- ( ph -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
130	129	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
131		nfra1 2848	. . . . . . . . . . . 12 |- F/ t A. t e. RR ( abs ` ( F ` t ) ) <_ w
132		simpl 457	. . . . . . . . . . . . . 14 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> A. t e. RR ( abs ` ( F ` t ) ) <_ w )
133		elioore 11571	. . . . . . . . . . . . . . 15 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> t e. RR )
134	133	adantl 466	. . . . . . . . . . . . . 14 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. RR )
135		rspa 2834	. . . . . . . . . . . . . 14 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. RR ) -> ( abs ` ( F ` t ) ) <_ w )
136	132, 134, 135	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w )
137	136	ex 434	. . . . . . . . . . . 12 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( F ` t ) ) <_ w ) )
138	131, 137	ralrimi 2867	. . . . . . . . . . 11 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
139	138	reximi 2935	. . . . . . . . . 10 |- ( 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 )
140	139	a1i 11	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( 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 ) )
141	130, 140	mpd 15	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
142		ssid 3528	. . . . . . . . . . . . 13 |- RR C_ RR
143	142	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ RR )
144		dvfre 22222	. . . . . . . . . . . 12 |- ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
145	45, 143, 144	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
146	145	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
147		eqid 2467	. . . . . . . . . . . . . 14 |- ( RR _D F ) = ( RR _D F )
148	49	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ N ) ) -> pi e. RR )
149	67	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ N ) ) -> -u pi e. RR )
150	104	reseq2d 5279	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
151	150, 106	eleq12d 2549	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
152	101, 151	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
153		fourierdlem112.fdvcn	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
154	152, 153	chvarv 1983	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
155	154	adantlr 714	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
156		fourierdlem112.x	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. RR )
157	62, 156	readdcld 9635	. . . . . . . . . . . . . . 15 |- ( ph -> ( -u pi + X ) e. RR )
158	157	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
159	157	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ph -> ( -u pi + X ) e. RR* )
160	61, 156	readdcld 9635	. . . . . . . . . . . . . . . 16 |- ( ph -> ( pi + X ) e. RR )
161	62, 61, 156, 71	ltadd1dd 10175	. . . . . . . . . . . . . . . 16 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
162	160	ltpnfd 31380	. . . . . . . . . . . . . . . 16 |- ( ph -> ( pi + X ) < +oo )
163	159, 115, 160, 161, 162	eliood 31418	. . . . . . . . . . . . . . 15 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
164	163	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
165		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = h -> ( k x. T ) = ( h x. T ) )
166	165	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k = h -> ( y + ( k x. T ) ) = ( y + ( h x. T ) ) )
167	166	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = h -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
168	167	cbvrexv 3094	. . . . . . . . . . . . . . . . . . . . 21 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
169	168	rgenw 2828	. . . . . . . . . . . . . . . . . . . 20 |- 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 )
170		rabbi 3045	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 } )
171	169, 170	mpbi 208	. . . . . . . . . . . . . . . . . . 19 |- { 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 }
172	171	uneq2i 3660	. . . . . . . . . . . . . . . . . 18 |- ( { ( -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 } )
173		isoeq5 6218	. . . . . . . . . . . . . . . . . 18 |- ( ( { ( -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 } ) ) ) )
174	172, 173	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( 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 } ) ) )
175	174	ax-gen 1601	. . . . . . . . . . . . . . . 16 |- A. 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 } ) ) <-> 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 } ) ) )
176		iotabi 5566	. . . . . . . . . . . . . . . 16 |- ( A. 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 } ) ) <-> 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 } ) ) ) -> ( 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 } ) ) ) )
177	175, 176	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( 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 } ) ) )
178	127, 177	eqtri 2496	. . . . . . . . . . . . . 14 |- 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 } ) ) )
179		eleq1 2539	. . . . . . . . . . . . . . . 16 |- ( v = u -> ( v e. dom ( RR _D F ) <-> u e. dom ( RR _D F ) ) )
180		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( v = u -> ( ( RR _D F ) ` v ) = ( ( RR _D F ) ` u ) )
181		eqidd 2468	. . . . . . . . . . . . . . . 16 |- ( v = u -> 0 = 0 )
182	179, 180, 181	ifeq123d 31337	. . . . . . . . . . . . . . 15 |- ( 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 ) )
183	182	cbvmptv 4544	. . . . . . . . . . . . . 14 |- ( 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 ) )
184	85, 147, 95, 148, 149, 57, 96, 97, 99, 155, 158, 164, 122, 178, 183	fourierdlem97 31827	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
185		cncff 21265	. . . . . . . . . . . . 13 |- ( ( ( 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 )
186	184, 185	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
187		fdm 5741	. . . . . . . . . . . 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 ) ) ) )
188	186, 187	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
189		ssdmres 5301	. . . . . . . . . . 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 ) ) ) )
190	188, 189	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
191		fssres 5757	. . . . . . . . . 10 |- ( ( ( RR _D F ) : dom ( RR _D F ) --> RR /\ ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
192	146, 190, 191	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
193	48	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> RR C_ CC )
194		cncffvrn 21270	. . . . . . . . . 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 ) )
195	193, 184, 194	syl2anc 661	. . . . . . . . 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 ) )
196	192, 195	mpbird 232	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
197		fourierdlem112.fdvbd	. . . . . . . . . . 11 |- ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
198	197	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
199		nfv 1683	. . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0..^ N ) )
200		nfra1 2848	. . . . . . . . . . . . . 14 |- F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
201	199, 200	nfan 1875	. . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
202		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
203		fvres 5886	. . . . . . . . . . . . . . . . . 18 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
204	202, 203	syl 16	. . . . . . . . . . . . . . . . 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 ) )
205	204	fveq2d 5876	. . . . . . . . . . . . . . . 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 ) ) )
206	205	adantlr 714	. . . . . . . . . . . . . . 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 ) ) )
207		simplr 754	. . . . . . . . . . . . . . . 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 )
208	190	sselda 3509	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
209	208	adantlr 714	. . . . . . . . . . . . . . . 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 ) )
210		rspa 2834	. . . . . . . . . . . . . . . 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 )
211	207, 209, 210	syl2anc 661	. . . . . . . . . . . . . . 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 )
212	206, 211	eqbrtrd 4473	. . . . . . . . . . . . . 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 )
213	212	ex 434	. . . . . . . . . . . . 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 ) )
214	201, 213	ralrimi 2867	. . . . . . . . . . . 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 )
215	214	ex 434	. . . . . . . . . . 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 ) )
216	215	reximdv 2941	. . . . . . . . . 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 ) )
217	198, 216	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 )
218		nfra1 2848	. . . . . . . . . . . 12 |- F/ t A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z
219	203	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( RR _D F ) ` t ) = ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) )
220	219	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
221	220	adantl 466	. . . . . . . . . . . . . 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 ) ) )
222		rspa 2834	. . . . . . . . . . . . . 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 )
223	221, 222	eqbrtrd 4473	. . . . . . . . . . . . 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 )
224	223	ex 434	. . . . . . . . . . . 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 ) )
225	218, 224	ralrimi 2867	. . . . . . . . . . 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 )
226	225	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 ) )
227	226	reximdv 2941	. . . . . . . . 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 ) )
228	217, 227	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 )
229		nfv 1683	. . . . . . . . . . . 12 |- F/ i ( ph /\ j e. ( 0..^ M ) )
230		nfcv 2629	. . . . . . . . . . . . . 14 |- F/_ i j
231	230	nfcsb1 3455	. . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ C
232		nfcv 2629	. . . . . . . . . . . . 13 |- F/_ i ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) )
233	231, 232	nfel 2642	. . . . . . . . . . . 12 |- F/ i [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) )
234	229, 233	nfim 1867	. . . . . . . . . . 11 |- F/ i ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
235		csbeq1a 3449	. . . . . . . . . . . . 13 |- ( i = j -> C = [_ j / i ]_ C )
236	105, 102	oveq12d 6313	. . . . . . . . . . . . 13 |- ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
237	235, 236	eleq12d 2549	. . . . . . . . . . . 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 ) ) ) )
238	101, 237	imbi12d 320	. . . . . . . . . . 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 ) ) ) ) )
239		fourierdlem112.c	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
240	234, 238, 239	chvar 1982	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
241	240	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
242	85, 95, 57, 96, 97, 99, 111, 241, 112, 118, 122, 127	fourierdlem96 31826	. . . . . . . 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 ) ) )
243	230	nfcsb1 3455	. . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ U
244		nfcv 2629	. . . . . . . . . . . . 13 |- F/_ i ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) )
245	243, 244	nfel 2642	. . . . . . . . . . . 12 |- F/ i [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) )
246	229, 245	nfim 1867	. . . . . . . . . . 11 |- F/ i ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
247		csbeq1a 3449	. . . . . . . . . . . . 13 |- ( i = j -> U = [_ j / i ]_ U )
248	105, 103	oveq12d 6313	. . . . . . . . . . . . 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 ) ) ) )
249	247, 248	eleq12d 2549	. . . . . . . . . . . 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 ) ) ) ) )
250	101, 249	imbi12d 320	. . . . . . . . . . 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 ) ) ) ) ) )
251		fourierdlem112.u	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
252	246, 250, 251	chvar 1982	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
253	252	adantlr 714	. . . . . . . . 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 ) ) ) )
254	85, 95, 57, 96, 97, 99, 111, 253, 158, 164, 122, 127	fourierdlem99 31829	. . . . . . . 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 ) ) ) )
255		eqeq1 2471	. . . . . . . . . 10 |- ( g = s -> ( g = 0 <-> s = 0 ) )
256		eqidd 2468	. . . . . . . . . 10 |- ( g = s -> 0 = 0 )
257		oveq2 6303	. . . . . . . . . . . . 13 |- ( g = s -> ( X + g ) = ( X + s ) )
258	257	fveq2d 5876	. . . . . . . . . . . 12 |- ( g = s -> ( F ` ( X + g ) ) = ( F ` ( X + s ) ) )
259		breq2 4457	. . . . . . . . . . . . 13 |- ( g = s -> ( 0 < g <-> 0 < s ) )
260		eqidd 2468	. . . . . . . . . . . . 13 |- ( g = s -> R = R )
261		eqidd 2468	. . . . . . . . . . . . 13 |- ( g = s -> L = L )
262	259, 260, 261	ifeq123d 31337	. . . . . . . . . . . 12 |- ( g = s -> if ( 0 < g , R , L ) = if ( 0 < s , R , L ) )
263	258, 262	oveq12d 6313	. . . . . . . . . . 11 |- ( g = s -> ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) )
264		id 22	. . . . . . . . . . 11 |- ( g = s -> g = s )
265	263, 264	oveq12d 6313	. . . . . . . . . 10 |- ( g = s -> ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) )
266	255, 256, 265	ifeq123d 31337	. . . . . . . . 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 ) ) )
267	266	cbvmptv 4544	. . . . . . . 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 ) ) )
268		eqeq1 2471	. . . . . . . . . 10 |- ( o = s -> ( o = 0 <-> s = 0 ) )
269		eqidd 2468	. . . . . . . . . 10 |- ( o = s -> 1 = 1 )
270		id 22	. . . . . . . . . . 11 |- ( o = s -> o = s )
271		oveq1 6302	. . . . . . . . . . . . 13 |- ( o = s -> ( o / 2 ) = ( s / 2 ) )
272	271	fveq2d 5876	. . . . . . . . . . . 12 |- ( o = s -> ( sin ` ( o / 2 ) ) = ( sin ` ( s / 2 ) ) )
273	272	oveq2d 6311	. . . . . . . . . . 11 |- ( o = s -> ( 2 x. ( sin ` ( o / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
274	270, 273	oveq12d 6313	. . . . . . . . . 10 |- ( o = s -> ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
275	268, 269, 274	ifeq123d 31337	. . . . . . . . 9 |- ( o = s -> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
276	275	cbvmptv 4544	. . . . . . . 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 ) ) ) ) ) )
277		fveq2 5872	. . . . . . . . . 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 ) )
278		fveq2 5872	. . . . . . . . . 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 ) )
279	277, 278	oveq12d 6313	. . . . . . . . 9 |- ( r = s -> ( ( ( g e. ( -u pi [,] pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X