Theorem fourierdlem111 31841

Description: The fourier partial sum for F is the sum of two integrals, with the same integrand involving F and the Dirichlet Kernel D, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem111.a	|- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / pi ) )
fourierdlem111.b	|- B = ( n e. NN |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / pi ) )
fourierdlem111.s	|- S = ( 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 ) ) ) ) ) )
fourierdlem111.d	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
fourierdlem111.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem111.m	|- ( ph -> M e. NN )
fourierdlem111.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem111.x	|- ( ph -> X e. RR )
fourierdlem111.6	|- ( ph -> F : RR --> RR )
fourierdlem111.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem111.g	|- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
fourierdlem111.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem111.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem111.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
fourierdlem111.t	|- T = ( 2 x. pi )
fourierdlem111.o	|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi - X ) /\ ( p ` m ) = ( pi - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem111.14	|- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )

Assertion

Ref	Expression
fourierdlem111	|- ( ( ph /\ n e. NN ) -> ( S ` n ) = ( S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )

Distinct variable groups:   A, m, n   B, m   D, i, m, y   D, s, t, i, y   x, D, i, s, y   i, F, n, s, t, y   x, F, n   i, G, s, x   L, s, t   x, L   i, M, m, p   M, s, t, y   x, M   Q, i, p   Q, s, t, y   x, Q   R, s, t   x, R   T, s, x   i, W, m, p   W, s, x, y   i, X, m, n, y   X, p   X, s, t   x, X   ph, i, m, n, y   ph, s, t   ph, x

Allowed substitution hints:   ph( p)   A( x, y, t, i, s, p)   B( x, y, t, i, n, s, p)   D( n, p)   P( x, y, t, i, m, n, s, p)   Q( m, n)   R( y, i, m, n, p)   S( x, y, t, i, m, n, s, p)   T( y, t, i, m, n, p)   F( m, p)   G( y, t, m, n, p)   L( y, i, m, n, p)   M( n)   O( x, y, t, i, m, n, s, p)   W( t, n)

Proof of Theorem fourierdlem111

Dummy variables k j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2539	. . . . . 6 |- ( k = n -> ( k e. NN <-> n e. NN ) )
2	1	anbi2d 703	. . . . 5 |- ( k = n -> ( ( ph /\ k e. NN ) <-> ( ph /\ n e. NN ) ) )
3		fveq2 5872	. . . . . 6 |- ( k = n -> ( S ` k ) = ( S ` n ) )
4		fveq2 5872	. . . . . . . . . 10 |- ( k = n -> ( D ` k ) = ( D ` n ) )
5	4	fveq1d 5874	. . . . . . . . 9 |- ( k = n -> ( ( D ` k ) ` ( t - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
6	5	oveq2d 6311	. . . . . . . 8 |- ( k = n -> ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) = ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
7	6	adantr 465	. . . . . . 7 |- ( ( k = n /\ t e. ( -u pi (,) pi ) ) -> ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) = ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
8	7	itgeq2dv 22056	. . . . . 6 |- ( k = n -> S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
9	3, 8	eqeq12d 2489	. . . . 5 |- ( k = n -> ( ( S ` k ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t <-> ( S ` n ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t ) )
10	2, 9	imbi12d 320	. . . 4 |- ( k = n -> ( ( ( ph /\ k e. NN ) -> ( S ` k ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t ) <-> ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t ) ) )
11		fourierdlem111.6	. . . . . 6 |- ( ph -> F : RR --> RR )
12	11	adantr 465	. . . . 5 |- ( ( ph /\ k e. NN ) -> F : RR --> RR )
13		eqid 2467	. . . . 5 |- ( -u pi (,) pi ) = ( -u pi (,) pi )
14		elioore 11571	. . . . . . . . . 10 |- ( s e. ( -u pi (,) pi ) -> s e. RR )
15	14	ssriv 3513	. . . . . . . . 9 |- ( -u pi (,) pi ) C_ RR
16	15	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) C_ RR )
17	11, 16	feqresmpt 5928	. . . . . . 7 |- ( ph -> ( F |` ( -u pi (,) pi ) ) = ( x e. ( -u pi (,) pi ) |-> ( F ` x ) ) )
18		ioossicc 11622	. . . . . . . . 9 |- ( -u pi (,) pi ) C_ ( -u pi [,] pi )
19	18	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) C_ ( -u pi [,] pi ) )
20		ioombl 21843	. . . . . . . . 9 |- ( -u pi (,) pi ) e. dom vol
21	20	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) e. dom vol )
22	11	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> F : RR --> RR )
23		pire 22718	. . . . . . . . . . . . . . . . 17 |- pi e. RR
24	23	renegcli 9892	. . . . . . . . . . . . . . . 16 |- -u pi e. RR
25	24, 23	pm3.2i 455	. . . . . . . . . . . . . . 15 |- ( -u pi e. RR /\ pi e. RR )
26		elicc2 11601	. . . . . . . . . . . . . . 15 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( t e. ( -u pi [,] pi ) <-> ( t e. RR /\ -u pi <_ t /\ t <_ pi ) ) )
27	25, 26	ax-mp 5	. . . . . . . . . . . . . 14 |- ( t e. ( -u pi [,] pi ) <-> ( t e. RR /\ -u pi <_ t /\ t <_ pi ) )
28	27	biimpi 194	. . . . . . . . . . . . 13 |- ( t e. ( -u pi [,] pi ) -> ( t e. RR /\ -u pi <_ t /\ t <_ pi ) )
29	28	simp1d 1008	. . . . . . . . . . . 12 |- ( t e. ( -u pi [,] pi ) -> t e. RR )
30	29	ssriv 3513	. . . . . . . . . . 11 |- ( -u pi [,] pi ) C_ RR
31	30	a1i 11	. . . . . . . . . 10 |- ( ph -> ( -u pi [,] pi ) C_ RR )
32	31	sselda 3509	. . . . . . . . 9 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> x e. RR )
33	22, 32	ffvelrnd 6033	. . . . . . . 8 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> ( F ` x ) e. RR )
34	11, 31	feqresmpt 5928	. . . . . . . . . 10 |- ( ph -> ( F |` ( -u pi [,] pi ) ) = ( x e. ( -u pi [,] pi ) |-> ( F ` x ) ) )
35	34	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( x e. ( -u pi [,] pi ) |-> ( F ` x ) ) = ( F |` ( -u pi [,] pi ) ) )
36		fourierdlem111.p	. . . . . . . . . 10 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
37		fourierdlem111.m	. . . . . . . . . 10 |- ( ph -> M e. NN )
38		fourierdlem111.q	. . . . . . . . . 10 |- ( ph -> Q e. ( P ` M ) )
39		ax-resscn 9561	. . . . . . . . . . . . 13 |- RR C_ CC
40	39	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ CC )
41	11, 40	fssd 5746	. . . . . . . . . . 11 |- ( ph -> F : RR --> CC )
42		fssres 5757	. . . . . . . . . . 11 |- ( ( F : RR --> CC /\ ( -u pi [,] pi ) C_ RR ) -> ( F |` ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
43	41, 31, 42	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( F |` ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
44		ioossicc 11622	. . . . . . . . . . . . 13 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
45	24	rexri 9658	. . . . . . . . . . . . . . 15 |- -u pi e. RR*
46	45	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -u pi e. RR* )
47	23	rexri 9658	. . . . . . . . . . . . . . 15 |- pi e. RR*
48	47	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> pi e. RR* )
49	36, 37, 38	fourierdlem15 31745	. . . . . . . . . . . . . . 15 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
50	49	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
51		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
52	46, 48, 50, 51	fourierdlem8 31738	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
53	44, 52	syl5ss 3520	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
54		resabs1 5308	. . . . . . . . . . . 12 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
55	53, 54	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
56		fourierdlem111.fcn	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
57	55, 56	eqeltrd 2555	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
58		fourierdlem111.r	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
59	55	oveq1d 6310	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
60	59	eleq2d 2537	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( R e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) <-> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) ) )
61	58, 60	mpbird 232	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
62		fourierdlem111.l	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
63	55	oveq1d 6310	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
64	63	eleq2d 2537	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( L e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) <-> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) ) )
65	62, 64	mpbird 232	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
66	36, 37, 38, 43, 57, 61, 65	fourierdlem69 31799	. . . . . . . . 9 |- ( ph -> ( F |` ( -u pi [,] pi ) ) e. L^1 )
67	35, 66	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( x e. ( -u pi [,] pi ) |-> ( F ` x ) ) e. L^1 )
68	19, 21, 33, 67	iblss 22079	. . . . . . 7 |- ( ph -> ( x e. ( -u pi (,) pi ) |-> ( F ` x ) ) e. L^1 )
69	17, 68	eqeltrd 2555	. . . . . 6 |- ( ph -> ( F |` ( -u pi (,) pi ) ) e. L^1 )
70	69	adantr 465	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( F |` ( -u pi (,) pi ) ) e. L^1 )
71		fourierdlem111.a	. . . . 5 |- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / pi ) )
72		fourierdlem111.b	. . . . 5 |- B = ( n e. NN |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / pi ) )
73		fourierdlem111.x	. . . . . 6 |- ( ph -> X e. RR )
74	73	adantr 465	. . . . 5 |- ( ( ph /\ k e. NN ) -> X e. RR )
75		fourierdlem111.s	. . . . 5 |- S = ( 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 ) ) ) ) ) )
76		fourierdlem111.d	. . . . 5 |- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
77		simpr 461	. . . . 5 |- ( ( ph /\ k e. NN ) -> k e. NN )
78	12, 13, 70, 71, 72, 74, 75, 76, 77	fourierdlem83 31813	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S ` k ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t )
79	10, 78	chvarv 1983	. . 3 |- ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
80	24	a1i 11	. . . . 5 |- ( ( ph /\ n e. NN ) -> -u pi e. RR )
81	23	a1i 11	. . . . 5 |- ( ( ph /\ n e. NN ) -> pi e. RR )
82	41	adantr 465	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> F : RR --> CC )
83	29	adantl 466	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
84		ffvelrn 6030	. . . . . . . 8 |- ( ( F : RR --> CC /\ t e. RR ) -> ( F ` t ) e. CC )
85	82, 83, 84	syl2anc 661	. . . . . . 7 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
86	85	adantlr 714	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
87	76	dirkerf 31720	. . . . . . . . . 10 |- ( n e. NN -> ( D ` n ) : RR --> RR )
88	87	adantl 466	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> ( D ` n ) : RR --> RR )
89	88	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( D ` n ) : RR --> RR )
90	73	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> X e. RR )
91	83, 90	resubcld 9999	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
92	91	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
93		ffvelrn 6030	. . . . . . . 8 |- ( ( ( D ` n ) : RR --> RR /\ ( t - X ) e. RR ) -> ( ( D ` n ) ` ( t - X ) ) e. RR )
94	89, 92, 93	syl2anc 661	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. RR )
95	39, 94	sseldi 3507	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. CC )
96	86, 95	mulcld 9628	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) e. CC )
97	80, 81, 96	itgioo 22090	. . . 4 |- ( ( ph /\ n e. NN ) -> S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
98		fvres 5886	. . . . . . . 8 |- ( t e. ( -u pi [,] pi ) -> ( ( F |` ( -u pi [,] pi ) ) ` t ) = ( F ` t ) )
99	98	eqcomd 2475	. . . . . . 7 |- ( t e. ( -u pi [,] pi ) -> ( F ` t ) = ( ( F |` ( -u pi [,] pi ) ) ` t ) )
100	99	oveq1d 6310	. . . . . 6 |- ( t e. ( -u pi [,] pi ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
101	100	adantl 466	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
102	101	itgeq2dv 22056	. . . 4 |- ( ( ph /\ n e. NN ) -> S. ( -u pi [,] pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( -u pi [,] pi ) ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
103		nfcv 2629	. . . . . . . 8 |- F/_ m ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
104		nfcv 2629	. . . . . . . 8 |- F/_ n ( 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 ) ) ) ) ) )
105		simpl 457	. . . . . . . . . . . . 13 |- ( ( n = m /\ y e. RR ) -> n = m )
106	105	oveq2d 6311	. . . . . . . . . . . 12 |- ( ( n = m /\ y e. RR ) -> ( 2 x. n ) = ( 2 x. m ) )
107	106	oveq1d 6310	. . . . . . . . . . 11 |- ( ( n = m /\ y e. RR ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. m ) + 1 ) )
108	107	oveq1d 6310	. . . . . . . . . 10 |- ( ( n = m /\ y e. RR ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) )
109	105	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ( n = m /\ y e. RR ) -> ( n + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
110	109	oveq1d 6310	. . . . . . . . . . . 12 |- ( ( n = m /\ y e. RR ) -> ( ( n + ( 1 / 2 ) ) x. y ) = ( ( m + ( 1 / 2 ) ) x. y ) )
111	110	fveq2d 5876	. . . . . . . . . . 11 |- ( ( n = m /\ y e. RR ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) )
112	111	oveq1d 6310	. . . . . . . . . 10 |- ( ( n = m /\ y e. RR ) -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) )
113	108, 112	ifeq12d 3965	. . . . . . . . 9 |- ( ( n = m /\ y e. RR ) -> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = 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 ) ) ) ) ) )
114	113	mpteq2dva 4539	. . . . . . . 8 |- ( n = m -> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
115	103, 104, 114	cbvmpt 4543	. . . . . . 7 |- ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
116	76, 115	eqtri 2496	. . . . . 6 |- 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 ) ) ) ) ) ) )
117		nfcv 2629	. . . . . . 7 |- F/_ t ( ( ( F |` ( -u pi [,] pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) )
118		nfcv 2629	. . . . . . 7 |- F/_ s ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) )
119		fveq2 5872	. . . . . . . 8 |- ( s = t -> ( ( F |` ( -u pi [,] pi ) ) ` s ) = ( ( F |` ( -u pi [,] pi ) ) ` t ) )
120		oveq1 6302	. . . . . . . . 9 |- ( s = t -> ( s - X ) = ( t - X ) )
121	120	fveq2d 5876	. . . . . . . 8 |- ( s = t -> ( ( D ` n ) ` ( s - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
122	119, 121	oveq12d 6313	. . . . . . 7 |- ( s = t -> ( ( ( F |` ( -u pi [,] pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
123	117, 118, 122	cbvmpt 4543	. . . . . 6 |- ( s e. ( -u pi [,] pi ) |-> ( ( ( F |` ( -u pi [,] pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) ) ) = ( t e. ( -u pi [,] pi ) |-> ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
124	38	adantr 465	. . . . . 6 |- ( ( ph /\ n e. NN ) -> Q e. ( P ` M ) )
125	37	adantr 465	. . . . . 6 |- ( ( ph /\ n e. NN ) -> M e. NN )
126		simpr 461	. . . . . 6 |- ( ( ph /\ n e. NN ) -> n e. NN )
127	73	adantr 465	. . . . . 6 |- ( ( ph /\ n e. NN ) -> X e. RR )
128	43	adantr 465	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( F |` ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
129	57	adantlr 714	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
130	61	adantlr 714	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
131	65	adantlr 714	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> L e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
132	116, 36, 123, 124, 125, 126, 127, 128, 129, 130, 131	fourierdlem101 31831	. . . . 5 |- ( ( ph /\ n e. NN ) -> S. ( -u pi [,] pi ) ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
133		oveq2 6303	. . . . . . . . . 10 |- ( s = y -> ( X + s ) = ( X + y ) )
134	133	fveq2d 5876	. . . . . . . . 9 |- ( s = y -> ( F ` ( X + s ) ) = ( F ` ( X + y ) ) )
135		fveq2 5872	. . . . . . . . 9 |- ( s = y -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` y ) )
136	134, 135	oveq12d 6313	. . . . . . . 8 |- ( s = y -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) )
137		nfcv 2629	. . . . . . . 8 |- F/_ y ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) )
138		nfcv 2629	. . . . . . . 8 |- F/_ s ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) )
139	136, 137, 138	cbvitg 22050	. . . . . . 7 |- S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y
140	139	a1i 11	. . . . . 6 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
141	24	a1i 11	. . . . . . . . . . 11 |- ( ph -> -u pi e. RR )
142	141, 73	jca 532	. . . . . . . . . 10 |- ( ph -> ( -u pi e. RR /\ X e. RR ) )
143		resubcl 9895	. . . . . . . . . 10 |- ( ( -u pi e. RR /\ X e. RR ) -> ( -u pi - X ) e. RR )
144	142, 143	syl 16	. . . . . . . . 9 |- ( ph -> ( -u pi - X ) e. RR )
145	144	adantr 465	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( -u pi - X ) e. RR )
146	23	a1i 11	. . . . . . . . . . 11 |- ( ph -> pi e. RR )
147	146, 73	jca 532	. . . . . . . . . 10 |- ( ph -> ( pi e. RR /\ X e. RR ) )
148		resubcl 9895	. . . . . . . . . 10 |- ( ( pi e. RR /\ X e. RR ) -> ( pi - X ) e. RR )
149	147, 148	syl 16	. . . . . . . . 9 |- ( ph -> ( pi - X ) e. RR )
150	149	adantr 465	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( pi - X ) e. RR )
151	41	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> F : RR --> CC )
152	73	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> X e. RR )
153		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. ( ( -u pi - X ) [,] ( pi - X ) ) )
154	144	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) e. RR )
155	149	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( pi - X ) e. RR )
156		elicc2 11601	. . . . . . . . . . . . . . 15 |- ( ( ( -u pi - X ) e. RR /\ ( pi - X ) e. RR ) -> ( y e. ( ( -u pi - X ) [,] ( pi - X ) ) <-> ( y e. RR /\ ( -u pi - X ) <_ y /\ y <_ ( pi - X ) ) ) )
157	154, 155, 156	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( y e. ( ( -u pi - X ) [,] ( pi - X ) ) <-> ( y e. RR /\ ( -u pi - X ) <_ y /\ y <_ ( pi - X ) ) ) )
158	153, 157	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( y e. RR /\ ( -u pi - X ) <_ y /\ y <_ ( pi - X ) ) )
159	158	simp1d 1008	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. RR )
160	152, 159	readdcld 9635	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) e. RR )
161		ffvelrn 6030	. . . . . . . . . . 11 |- ( ( F : RR --> CC /\ ( X + y ) e. RR ) -> ( F ` ( X + y ) ) e. CC )
162	151, 160, 161	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
163	162	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
164	88	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( D ` n ) : RR --> RR )
165	159	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. RR )
166		ffvelrn 6030	. . . . . . . . . . 11 |- ( ( ( D ` n ) : RR --> RR /\ y e. RR ) -> ( ( D ` n ) ` y ) e. RR )
167	164, 165, 166	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( D ` n ) ` y ) e. RR )
168	39, 167	sseldi 3507	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( D ` n ) ` y ) e. CC )
169	163, 168	mulcld 9628	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) e. CC )
170	145, 150, 169	itgioo 22090	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
171	39, 73	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ph -> X e. CC )
172	39, 146	sseldi 3507	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> pi e. CC )
173	172	negcld 9929	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -u pi e. CC )
174	171, 173	pncan3d 9945	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( X + ( -u pi - X ) ) = -u pi )
175	174	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( ph -> -u pi = ( X + ( -u pi - X ) ) )
176	175	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi = ( X + ( -u pi - X ) ) )
177	158	simp2d 1009	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) <_ y )
178	154, 159, 152, 177	leadd2dd 10179	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + ( -u pi - X ) ) <_ ( X + y ) )
179	176, 178	eqbrtrd 4473	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi <_ ( X + y ) )
180	158	simp3d 1010	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y <_ ( pi - X ) )
181	159, 155, 152, 180	leadd2dd 10179	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) <_ ( X + ( pi - X ) ) )
182	171	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> X e. CC )
183	172	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> pi e. CC )
184	182, 183	pncan3d 9945	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + ( pi - X ) ) = pi )
185	181, 184	breqtrd 4477	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) <_ pi )
186	160, 179, 185	3jca 1176	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( X + y ) e. RR /\ -u pi <_ ( X + y ) /\ ( X + y ) <_ pi ) )
187	24	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi e. RR )
188	23	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> pi e. RR )
189		elicc2 11601	. . . . . . . . . . . . . 14 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( ( X + y ) e. ( -u pi [,] pi ) <-> ( ( X + y ) e. RR /\ -u pi <_ ( X + y ) /\ ( X + y ) <_ pi ) ) )
190	187, 188, 189	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( X + y ) e. ( -u pi [,] pi ) <-> ( ( X + y ) e. RR /\ -u pi <_ ( X + y ) /\ ( X + y ) <_ pi ) ) )
191	186, 190	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) e. ( -u pi [,] pi ) )
192		fvres 5886	. . . . . . . . . . . 12 |- ( ( X + y ) e. ( -u pi [,] pi ) -> ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
193	191, 192	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
194	193	eqcomd 2475	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) )
195	194	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) )
196	195	oveq1d 6310	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) )
197	196	itgeq2dv 22056	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
198	170, 197	eqtrd 2508	. . . . . 6 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
199	140, 198	eqtr2d 2509	. . . . 5 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
200	132, 199	eqtrd 2508	. . . 4 |- ( ( ph /\ n e. NN ) -> S. ( -u pi [,] pi ) ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
201	97, 102, 200	3eqtrd 2512	. . 3 |- ( ( ph /\ n e. NN ) -> S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
202		elioore 11571	. . . . . . . . 9 |- ( s e. ( ( -u pi - X ) (,) ( pi - X ) ) -> s e. RR )
203	202	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> s e. RR )
204	41	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> F : RR --> CC )
205	73	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> X e. RR )
206	202	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> s e. RR )
207	205, 206	readdcld 9635	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( X + s ) e. RR )
208	204, 207	ffvelrnd 6033	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
209	208	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
210	39	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> RR C_ CC )
211	88	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( D ` n ) : RR --> RR )
212	211, 203	ffvelrnd 6033	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( D ` n ) ` s ) e. RR )
213	210, 212	sseldd 3510	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( D ` n ) ` s ) e. CC )
214	209, 213	mulcld 9628	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
215		fourierdlem111.g	. . . . . . . . . 10 |- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
216		oveq2 6303	. . . . . . . . . . . . 13 |- ( x = s -> ( X + x ) = ( X + s ) )
217	216	fveq2d 5876	. . . . . . . . . . . 12 |- ( x = s -> ( F ` ( X + x ) ) = ( F ` ( X + s ) ) )
218		fveq2 5872	. . . . . . . . . . . 12 |- ( x = s -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` s ) )
219	217, 218	oveq12d 6313	. . . . . . . . . . 11 |- ( x = s -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
220	219	cbvmptv 4544	. . . . . . . . . 10 |- ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) ) = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
221	215, 220	eqtri 2496	. . . . . . . . 9 |- G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
222	221	fvmpt2 5964	. . . . . . . 8 |- ( ( s e. RR /\ ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
223	203, 214, 222	syl2anc 661	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
224	223	eqcomd 2475	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
225	224	itgeq2dv 22056	. . . . 5 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( G ` s ) _d s )
226		eqidd 2468	. . . . 5 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) (,) ( pi - X ) ) ( G ` s ) _d s )
227	41	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> F : RR --> CC )
228	73	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> X e. RR )
229		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. RR )
230	228, 229	readdcld 9635	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( X + x ) e. RR )
231	227, 230	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
232	231	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
233	39	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> RR C_ CC )
234	88	ffvelrnda 6032	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. RR )
235	233, 234	sseldd 3510	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. CC )
236	232, 235	mulcld 9628	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC )
237	236, 215	fmptd 6056	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> G : RR --> CC )
238	237	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> G : RR --> CC )
239	144	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) e. RR )
240	149	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( pi - X ) e. RR )
241		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. ( ( -u pi - X ) [,] ( pi - X ) ) )
242		eliccre 31427	. . . . . . . . . 10 |- ( ( ( -u pi - X ) e. RR /\ ( pi - X ) e. RR /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
243	239, 240, 241, 242	syl3anc 1228	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
244	243	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
245	238, 244	ffvelrnd 6033	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( G ` s ) e. CC )
246	145, 150, 245	itgioo 22090	. . . . . 6 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` s ) _d s )
247		fveq2 5872	. . . . . . . 8 |- ( s = x -> ( G ` s ) = ( G ` x ) )
248	247	cbvitgv 22051	. . . . . . 7 |- S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` x ) _d x
249	248	a1i 11	. . . . . 6 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` x ) _d x )
250	246, 249	eqtrd 2508	. . . . 5 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` x ) _d x )
251	225, 226, 250	3eqtrd 2512	. . . 4 |- ( ( ph /\ n e. NN ) -> S. ( ( -u pi - X ) (,) ( pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` x ) _d x )
252		eqid 2467	. . . . . . 7 |- ( ( pi - X ) - ( -u pi - X ) ) = ( ( pi - X ) - ( -u pi - X ) )
253	127	renegcld 9998	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> -u X e. RR )
254		fourierdlem111.o	. . . . . . 7 |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u pi - X ) /\ ( p ` m ) = ( pi - X ) ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
255	36	fourierdlem2 31732	. . . . . . . . . . . . . . . . . . . 20 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
256	37, 255	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
257	38, 256	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
258	257	simpld 459	. . . . . . . . . . . . . . . . 17 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
259		elmapi 7452	. . . . . . . . . . . . . . . . 17 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
260	258, 259	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> Q : ( 0 ... M ) --> RR )
261	260	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
262		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( 0 ... M ) )
263	261, 262	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
264	73	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
265	263, 264	resubcld 9999	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
266	265	ralrimiva 2881	. . . . . . . . . . . 12 |- ( ph -> A. i e. ( 0 ... M ) ( ( Q ` i ) - X ) e. RR )
267		fourierdlem111.14	. . . . . . . . . . . . 13 |- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
268	267	fmpt 6053	. . . . . . . . . . . 12 |- ( A. i e. ( 0 ... M ) ( ( Q ` i ) - X ) e. RR <-> W : ( 0 ... M ) --> RR )
269	266, 268	sylib 196	. . . . . . . . . . 11 |- ( ph -> W : ( 0 ... M ) --> RR )
270		reex 9595	. . . . . . . . . . . . . 14 |- RR e. _V
271		ovex 6320	. . . . . . . . . . . . . 14 |- ( 0 ... M ) e. _V
272	270, 271	pm3.2i 455	. . . . . . . . . . . . 13 |- ( RR e. _V /\ ( 0 ... M ) e. _V )
273	272	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( RR e. _V /\ ( 0 ... M ) e. _V ) )
274		elmapg 7445	. . . . . . . . . . . 12 |- ( ( RR e. _V /\ ( 0 ... M ) e. _V ) -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
275	273, 274	syl 16	. . . . . . . . . . 11 |- ( ph -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
276	269, 275	mpbird 232	. . . . . . . . . 10 |- ( ph -> W e. ( RR ^m ( 0 ... M ) ) )
277	267	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
278		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
279	278	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
280	257	simprd 463	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
281	280	simpld 459	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) )
282	281	simpld 459	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) = -u pi )
283	282	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = 0 ) -> ( Q ` 0 ) = -u pi )
284		eqidd 2468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = 0 ) -> -u pi = -u pi )
285	279, 283, 284	3eqtrd 2512	. . . . . . . . . . . . . 14 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = -u pi )
286	285	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( -u pi - X ) )
287		0z 10887	. . . . . . . . . . . . . . . . 17 |- 0 e. ZZ
288	287	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 e. ZZ )
289	37	nnzd 10977	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. ZZ )
290		0re 9608	. . . . . . . . . . . . . . . . . . 19 |- 0 e. RR
291	290	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN -> 0 e. RR )
292		nnre 10555	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN -> M e. RR )
293		nngt0 10577	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN -> 0 < M )
294	291, 292, 293	ltled 9744	. . . . . . . . . . . . . . . . 17 |- ( M e. NN -> 0 <_ M )
295	37, 294	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ M )
296	288, 289, 295	3jca 1176	. . . . . . . . . . . . . . 15 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 <_ M ) )
297		eluz2 11100	. . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 <_ M ) )
298	296, 297	sylibr 212	. . . . . . . . . . . . . 14 |- ( ph -> M e. ( ZZ>= ` 0 ) )
299		eluzfz1 11705	. . . . . . . . . . . . . 14 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
300	298, 299	syl 16	. . . . . . . . . . . . 13 |- ( ph -> 0 e. ( 0 ... M ) )
301	277, 286, 300, 144	fvmptd 5962	. . . . . . . . . . . 12 |- ( ph -> ( W ` 0 ) = ( -u pi - X ) )
302		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
303	302	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = M ) -> ( Q ` i ) = ( Q ` M ) )
304	281	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` M ) = pi )
305	304	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = M ) -> ( Q ` M ) = pi )
306	303, 305	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( ( ph /\ i = M ) -> ( Q ` i ) = pi )
307	306	oveq1d 6310	. . . . . . . . . . . . 13 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( pi - X ) )
308		eluzfz2 11706	. . . . . . . . . . . . . 14 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
309	298, 308	syl 16	. . . . . . . . . . . . 13 |- ( ph -> M e. ( 0 ... M ) )
310	277, 307, 309, 149	fvmptd 5962	. . . . . . . . . . . 12 |- ( ph -> ( W ` M ) = ( pi - X ) )
311	301, 310	jca 532	. . . . . . . . . . 11 |- ( ph -> ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) )
312	280	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
313	312	r19.21bi 2836	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
314	260	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
315		elfzofz 11823	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
316	315	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
317	314, 316	ffvelrnd 6033	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
318		fzofzp1 11889	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
319	318	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
320	314, 319	ffvelrnd 6033	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
321	73	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
322	317, 320, 321	ltsub1d 10173	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) ) )
323	313, 322	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
324	316, 265	syldan 470	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
325	267	fvmpt2 5964	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
326	316, 324, 325	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
327		fveq2 5872	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
328	327	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
329	328	cbvmptv 4544	. . . . . . . . . . . . . . . . 17 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
330	267, 329	eqtri 2496	. . . . . . . . . . . . . . . 16 |- W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
331	330	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
332		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
333	332	oveq1d 6310	. . . . . . . . . . . . . . . 16 |- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
334	333	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
335	320, 321	resubcld 9999	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
336	331, 334, 319, 335	fvmptd 5962	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
337	326, 336	breq12d 4466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( W ` i ) < ( W ` ( i + 1 ) ) <-> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) ) )
338	323, 337	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) < ( W ` ( i + 1 ) ) )
339	338	ralrimiva 2881	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) )
340	311, 339	jca 532	. . . . . . . . . 10 |- ( ph -> ( ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) /\ A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) )
341	276, 340	jca 532	. . . . . . . . 9 |- ( ph -> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) /\ A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) )
342	254	fourierdlem2 31732	. . . . . . . . . 10 |- ( M e. NN -> ( W e. ( O ` M ) <-> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) /\ A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) ) )
343	37, 342	syl 16	. . . . . . . . 9 |- ( ph -> ( W e. ( O ` M ) <-> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) /\ A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) ) )
344	341, 343	mpbird 232	. . . . . . . 8 |- ( ph -> W e. ( O ` M ) )
345	344	adantr 465	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> W e. ( O ` M ) )
346	172, 173, 171	nnncan2d 9977	. . . . . . . . . . . 12 |- ( ph -> ( ( pi - X ) - ( -u pi - X ) ) = ( pi - -u pi ) )
347	39, 23	sselii 3506	. . . . . . . . . . . . . 14 |- pi e. CC
348	347, 347	subnegi 9910	. . . . . . . . . . . . 13 |- ( pi - -u pi ) = ( pi + pi )
349	348	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( pi - -u pi ) = ( pi + pi ) )
350		fourierdlem111.t	. . . . . . . . . . . . . 14 |- T = ( 2 x. pi )
351	347	2timesi 10668	. . . . . . . . . . . . . . 15 |- ( 2 x. pi ) = ( pi + pi )
352	351, 348	eqtr4i 2499	. . . . . . . . . . . . . 14 |- ( 2 x. pi ) = ( pi - -u pi )
353	350, 352	eqtri 2496	. . . . . . . . . . . . 13 |- T = ( pi - -u pi )
354	353, 349	syl5req 2521	. . . . . . . . . . . 12 |- ( ph -> ( pi + pi ) = T )
355	346, 349, 354	3eqtrd 2512	. . . . . . . . . . 11 |- ( ph -> ( ( pi - X ) - ( -u pi - X ) ) = T )
356	355	oveq2d 6311	. . . . . . . . . 10 |- ( ph -> ( x + ( ( pi - X ) - ( -u pi - X ) ) ) = ( x + T ) )
357	356	fveq2d 5876	. . . . . . . . 9 |- ( ph -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` ( x + T ) ) )
358	357	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` ( x + T ) ) )
359		simpr 461	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR )
360	215	fvmpt2 5964	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
361	359, 236, 360	syl2anc 661	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
362	171	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> X e. CC )
363	39, 229	sseldi 3507	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> x e. CC )
364		2re 10617	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
365	364, 23	remulcli 9622	. . . . . . . . . . . . . . . . . . 19 |- ( 2 x. pi ) e. RR
366	350, 365	eqeltri 2551	. . . . . . . . . . . . . . . . . 18 |- T e. RR
367	366	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. RR )
368	39, 367	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. CC )
369	368	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> T e. CC )
370	362, 363, 369	addassd 9630	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( ( X + x ) + T ) = ( X + ( x + T ) ) )
371	370	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) = ( ( X + x ) + T ) )
372	371	fveq2d 5876	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) = ( F ` ( ( X + x ) + T ) ) )
373		simpl 457	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ph )
374	373, 230	jca 532	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( ph /\ ( X + x ) e. RR ) )
375		eleq1 2539	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( s e. RR <-> ( X + x ) e. RR ) )
376	375	anbi2d 703	. . . . . . . . . . . . . . 15 |- ( s = ( X + x ) -> ( ( ph /\ s e. RR ) <-> ( ph /\ ( X + x ) e. RR ) ) )
377		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( s = ( X + x ) -> ( s + T ) = ( ( X + x ) + T ) )
378	377	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( F ` ( s + T ) ) = ( F ` ( ( X + x ) + T ) ) )
379		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( F ` s ) = ( F ` ( X + x ) ) )
380	378, 379	eqeq12d 2489	. . . . . . . . . . . . . . 15 |- ( s = ( X + x ) -> ( ( F ` ( s + T ) ) = ( F ` s ) <-> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
381	376, 380	imbi12d 320	. . . . . . . . . . . . . 14 |- ( s = ( X + x ) -> ( ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) ) <-> ( ( ph /\ ( X + x ) e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) ) )
382		nfv 1683	. . . . . . . . . . . . . . 15 |- F/ x ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) )
383		eleq1 2539	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x e. RR <-> s e. RR ) )
384	383	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( ( ph /\ x e. RR ) <-> ( ph /\ s e. RR ) ) )
385		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( x = s -> ( x + T ) = ( s + T ) )
386	385	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( F ` ( x + T ) ) = ( F ` ( s + T ) ) )
387		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( F ` x ) = ( F ` s ) )
388	386, 387	eqeq12d 2489	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( s + T ) ) = ( F ` s ) ) )
389	384, 388	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( x = s -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) ) ) )
390		fourierdlem111.fper	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
391	382, 389, 390	chvar 1982	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) )
392	381, 391	vtoclg 3176	. . . . . . . . . . . . 13 |- ( ( X + x ) e. RR -> ( ( ph /\ ( X + x ) e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
393	230, 374, 392	sylc 60	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) )
394	372, 393	eqtr2d 2509	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
395	394	adantlr 714	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
396	76, 350	dirkerper 31719	. . . . . . . . . . . 12 |- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) = ( ( D ` n ) ` x ) )
397	396	eqcomd 2475	. . . . . . . . . . 11 |- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
398	397	adantll 713	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
399	395, 398	oveq12d 6313	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
400	221	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
401		oveq2 6303	. . . . . . . . . . . . . 14 |- ( s = ( x + T ) -> ( X + s ) = ( X + ( x + T ) ) )
402	401	fveq2d 5876	. . . . . . . . . . . . 13 |- ( s = ( x + T ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( x + T ) ) ) )
403		fveq2 5872	. . . . . . . . . . . . 13 |- ( s = ( x + T ) -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` ( x + T ) ) )
404	402, 403	oveq12d 6313	. . . . . . . . . . . 12 |- ( s = ( x + T ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
405	404	adantl 466	. . . . . . . . . . 11 |- ( ( ( ( ph /\ n e. NN ) /\ x e. RR ) /\ s = ( x + T ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
406	367	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> T e. RR )
407	359, 406	readdcld 9635	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x + T ) e. RR )
408	367	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> T e. RR )
409	229, 408	readdcld 9635	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
410	228, 409	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) e. RR )
411	227, 410	ffvelrnd 6033	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
412	411	adantlr 714	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
413	88	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( D ` n ) : RR --> RR )
414	413, 407	ffvelrnd 6033	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. RR )
415	233, 414	sseldd 3510	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. CC )
416	412, 415	mulcld 9628	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) e. CC )
417	400, 405, 407, 416	fvmptd 5962	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
418	417	eqcomd 2475	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) = ( G ` ( x + T ) ) )
419	361, 399, 418	3eqtrrd 2513	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( G ` x ) )
420	358, 419	eqtrd 2508	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` x ) )
421	221	reseq1i 5275	. . . . . . . . . 10 |- ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
422	421	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
423		ioossre 11598	. . . . . . . . . . 11 |- ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR
424		resmpt 5329	. . . . . . . . . . 11 |- ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR -> ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
425	423, 424	ax-mp 5	. . . . . . . . . 10 |- ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
426	425	a1i 11	<