Theorem fourierdlem111 38081

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 2517	. . . . . 6 |- ( k = n -> ( k e. NN <-> n e. NN ) )
2	1	anbi2d 710	. . . . 5 |- ( k = n -> ( ( ph /\ k e. NN ) <-> ( ph /\ n e. NN ) ) )
3		fveq2 5865	. . . . . 6 |- ( k = n -> ( S ` k ) = ( S ` n ) )
4		fveq2 5865	. . . . . . . . . 10 |- ( k = n -> ( D ` k ) = ( D ` n ) )
5	4	fveq1d 5867	. . . . . . . . 9 |- ( k = n -> ( ( D ` k ) ` ( t - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
6	5	oveq2d 6306	. . . . . . . 8 |- ( k = n -> ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) = ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
7	6	adantr 467	. . . . . . 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 22739	. . . . . 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 2466	. . . . 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 322	. . . 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 467	. . . . 5 |- ( ( ph /\ k e. NN ) -> F : RR --> RR )
13		eqid 2451	. . . . 5 |- ( -u pi (,) pi ) = ( -u pi (,) pi )
14		ioossre 11696	. . . . . . . . 9 |- ( -u pi (,) pi ) C_ RR
15	14	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) C_ RR )
16	11, 15	feqresmpt 5919	. . . . . . 7 |- ( ph -> ( F |` ( -u pi (,) pi ) ) = ( x e. ( -u pi (,) pi ) |-> ( F ` x ) ) )
17		ioossicc 11720	. . . . . . . . 9 |- ( -u pi (,) pi ) C_ ( -u pi [,] pi )
18	17	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) C_ ( -u pi [,] pi ) )
19		ioombl 22518	. . . . . . . . 9 |- ( -u pi (,) pi ) e. dom vol
20	19	a1i 11	. . . . . . . 8 |- ( ph -> ( -u pi (,) pi ) e. dom vol )
21	11	adantr 467	. . . . . . . . 9 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> F : RR --> RR )
22		pire 23413	. . . . . . . . . . . . . . 15 |- pi e. RR
23	22	renegcli 9935	. . . . . . . . . . . . . 14 |- -u pi e. RR
24	23, 22	elicc2i 11700	. . . . . . . . . . . . 13 |- ( t e. ( -u pi [,] pi ) <-> ( t e. RR /\ -u pi <_ t /\ t <_ pi ) )
25	24	simp1bi 1023	. . . . . . . . . . . 12 |- ( t e. ( -u pi [,] pi ) -> t e. RR )
26	25	ssriv 3436	. . . . . . . . . . 11 |- ( -u pi [,] pi ) C_ RR
27	26	a1i 11	. . . . . . . . . 10 |- ( ph -> ( -u pi [,] pi ) C_ RR )
28	27	sselda 3432	. . . . . . . . 9 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> x e. RR )
29	21, 28	ffvelrnd 6023	. . . . . . . 8 |- ( ( ph /\ x e. ( -u pi [,] pi ) ) -> ( F ` x ) e. RR )
30	11, 27	feqresmpt 5919	. . . . . . . . 9 |- ( ph -> ( F |` ( -u pi [,] pi ) ) = ( x e. ( -u pi [,] pi ) |-> ( F ` x ) ) )
31		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 ) ) ) } )
32		fourierdlem111.m	. . . . . . . . . 10 |- ( ph -> M e. NN )
33		fourierdlem111.q	. . . . . . . . . 10 |- ( ph -> Q e. ( P ` M ) )
34		ax-resscn 9596	. . . . . . . . . . . . 13 |- RR C_ CC
35	34	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ CC )
36	11, 35	fssd 5738	. . . . . . . . . . 11 |- ( ph -> F : RR --> CC )
37	36, 27	fssresd 5750	. . . . . . . . . 10 |- ( ph -> ( F |` ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
38		ioossicc 11720	. . . . . . . . . . . . 13 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
39	23	rexri 9693	. . . . . . . . . . . . . . 15 |- -u pi e. RR*
40	39	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -u pi e. RR* )
41	22	rexri 9693	. . . . . . . . . . . . . . 15 |- pi e. RR*
42	41	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> pi e. RR* )
43	31, 32, 33	fourierdlem15 37984	. . . . . . . . . . . . . . 15 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
44	43	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
45		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
46	40, 42, 44, 45	fourierdlem8 37977	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
47	38, 46	syl5ss 3443	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
48	47	resabs1d 5134	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
49		fourierdlem111.fcn	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
50	48, 49	eqeltrd 2529	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
51		fourierdlem111.r	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
52	48	oveq1d 6305	. . . . . . . . . . 11 |- ( ( 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 ) ) )
53	51, 52	eleqtrrd 2532	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
54		fourierdlem111.l	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
55	48	oveq1d 6305	. . . . . . . . . . 11 |- ( ( 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 ) ) ) )
56	54, 55	eleqtrrd 2532	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
57	31, 32, 33, 37, 50, 53, 56	fourierdlem69 38039	. . . . . . . . 9 |- ( ph -> ( F |` ( -u pi [,] pi ) ) e. L^1 )
58	30, 57	eqeltrrd 2530	. . . . . . . 8 |- ( ph -> ( x e. ( -u pi [,] pi ) |-> ( F ` x ) ) e. L^1 )
59	18, 20, 29, 58	iblss 22762	. . . . . . 7 |- ( ph -> ( x e. ( -u pi (,) pi ) |-> ( F ` x ) ) e. L^1 )
60	16, 59	eqeltrd 2529	. . . . . 6 |- ( ph -> ( F |` ( -u pi (,) pi ) ) e. L^1 )
61	60	adantr 467	. . . . 5 |- ( ( ph /\ k e. NN ) -> ( F |` ( -u pi (,) pi ) ) e. L^1 )
62		fourierdlem111.a	. . . . 5 |- A = ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / pi ) )
63		fourierdlem111.b	. . . . 5 |- B = ( n e. NN |-> ( S. ( -u pi (,) pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / pi ) )
64		fourierdlem111.x	. . . . . 6 |- ( ph -> X e. RR )
65	64	adantr 467	. . . . 5 |- ( ( ph /\ k e. NN ) -> X e. RR )
66		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 ) ) ) ) ) )
67		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 ) ) ) ) ) ) )
68		simpr 463	. . . . 5 |- ( ( ph /\ k e. NN ) -> k e. NN )
69	12, 13, 61, 62, 63, 65, 66, 67, 68	fourierdlem83 38053	. . . 4 |- ( ( ph /\ k e. NN ) -> ( S ` k ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t )
70	10, 69	chvarv 2107	. . 3 |- ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u pi (,) pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
71	23	a1i 11	. . . . 5 |- ( ( ph /\ n e. NN ) -> -u pi e. RR )
72	22	a1i 11	. . . . 5 |- ( ( ph /\ n e. NN ) -> pi e. RR )
73	36	adantr 467	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> F : RR --> CC )
74	25	adantl 468	. . . . . . . 8 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> t e. RR )
75	73, 74	ffvelrnd 6023	. . . . . . 7 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
76	75	adantlr 721	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
77	67	dirkerf 37959	. . . . . . . . 9 |- ( n e. NN -> ( D ` n ) : RR --> RR )
78	77	ad2antlr 733	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( D ` n ) : RR --> RR )
79	64	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> X e. RR )
80	74, 79	resubcld 10047	. . . . . . . . 9 |- ( ( ph /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
81	80	adantlr 721	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( t - X ) e. RR )
82	78, 81	ffvelrnd 6023	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. RR )
83	82	recnd 9669	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. CC )
84	76, 83	mulcld 9663	. . . . 5 |- ( ( ( ph /\ n e. NN ) /\ t e. ( -u pi [,] pi ) ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) e. CC )
85	71, 72, 84	itgioo 22773	. . . 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 )
86		fvres 5879	. . . . . . . 8 |- ( t e. ( -u pi [,] pi ) -> ( ( F |` ( -u pi [,] pi ) ) ` t ) = ( F ` t ) )
87	86	eqcomd 2457	. . . . . . 7 |- ( t e. ( -u pi [,] pi ) -> ( F ` t ) = ( ( F |` ( -u pi [,] pi ) ) ` t ) )
88	87	oveq1d 6305	. . . . . 6 |- ( t e. ( -u pi [,] pi ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
89	88	adantl 468	. . . . 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 ) ) ) )
90	89	itgeq2dv 22739	. . . 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 )
91		simpl 459	. . . . . . . . . . . . 13 |- ( ( n = m /\ y e. RR ) -> n = m )
92	91	oveq2d 6306	. . . . . . . . . . . 12 |- ( ( n = m /\ y e. RR ) -> ( 2 x. n ) = ( 2 x. m ) )
93	92	oveq1d 6305	. . . . . . . . . . 11 |- ( ( n = m /\ y e. RR ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. m ) + 1 ) )
94	93	oveq1d 6305	. . . . . . . . . 10 |- ( ( n = m /\ y e. RR ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. pi ) ) )
95	91	oveq1d 6305	. . . . . . . . . . . . 13 |- ( ( n = m /\ y e. RR ) -> ( n + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
96	95	oveq1d 6305	. . . . . . . . . . . 12 |- ( ( n = m /\ y e. RR ) -> ( ( n + ( 1 / 2 ) ) x. y ) = ( ( m + ( 1 / 2 ) ) x. y ) )
97	96	fveq2d 5869	. . . . . . . . . . 11 |- ( ( n = m /\ y e. RR ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) )
98	97	oveq1d 6305	. . . . . . . . . 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 ) ) ) ) )
99	94, 98	ifeq12d 3901	. . . . . . . . 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 ) ) ) ) ) )
100	99	mpteq2dva 4489	. . . . . . . 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 ) ) ) ) ) ) )
101	100	cbvmptv 4495	. . . . . . 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 ) ) ) ) ) ) )
102	67, 101	eqtri 2473	. . . . . 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 ) ) ) ) ) ) )
103		fveq2 5865	. . . . . . . 8 |- ( s = t -> ( ( F |` ( -u pi [,] pi ) ) ` s ) = ( ( F |` ( -u pi [,] pi ) ) ` t ) )
104		oveq1 6297	. . . . . . . . 9 |- ( s = t -> ( s - X ) = ( t - X ) )
105	104	fveq2d 5869	. . . . . . . 8 |- ( s = t -> ( ( D ` n ) ` ( s - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
106	103, 105	oveq12d 6308	. . . . . . 7 |- ( s = t -> ( ( ( F |` ( -u pi [,] pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) ) = ( ( ( F |` ( -u pi [,] pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
107	106	cbvmptv 4495	. . . . . 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 ) ) ) )
108	33	adantr 467	. . . . . 6 |- ( ( ph /\ n e. NN ) -> Q e. ( P ` M ) )
109	32	adantr 467	. . . . . 6 |- ( ( ph /\ n e. NN ) -> M e. NN )
110		simpr 463	. . . . . 6 |- ( ( ph /\ n e. NN ) -> n e. NN )
111	64	adantr 467	. . . . . 6 |- ( ( ph /\ n e. NN ) -> X e. RR )
112	37	adantr 467	. . . . . 6 |- ( ( ph /\ n e. NN ) -> ( F |` ( -u pi [,] pi ) ) : ( -u pi [,] pi ) --> CC )
113	50	adantlr 721	. . . . . 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 ) )
114	53	adantlr 721	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( -u pi [,] pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
115	56	adantlr 721	. . . . . 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 ) ) ) )
116	102, 31, 107, 108, 109, 110, 111, 112, 113, 114, 115	fourierdlem101 38071	. . . . 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 )
117		oveq2 6298	. . . . . . . . . 10 |- ( s = y -> ( X + s ) = ( X + y ) )
118	117	fveq2d 5869	. . . . . . . . 9 |- ( s = y -> ( F ` ( X + s ) ) = ( F ` ( X + y ) ) )
119		fveq2 5865	. . . . . . . . 9 |- ( s = y -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` y ) )
120	118, 119	oveq12d 6308	. . . . . . . 8 |- ( s = y -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) )
121	120	cbvitgv 22734	. . . . . . 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
122	121	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 )
123	23	a1i 11	. . . . . . . . 9 |- ( ph -> -u pi e. RR )
124	123, 64	resubcld 10047	. . . . . . . 8 |- ( ph -> ( -u pi - X ) e. RR )
125	124	adantr 467	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( -u pi - X ) e. RR )
126	22	a1i 11	. . . . . . . . 9 |- ( ph -> pi e. RR )
127	126, 64	resubcld 10047	. . . . . . . 8 |- ( ph -> ( pi - X ) e. RR )
128	127	adantr 467	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( pi - X ) e. RR )
129	36	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> F : RR --> CC )
130	64	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> X e. RR )
131		simpr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. ( ( -u pi - X ) [,] ( pi - X ) ) )
132	124	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) e. RR )
133	127	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( pi - X ) e. RR )
134		elicc2 11699	. . . . . . . . . . . . . 14 |- ( ( ( -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 ) ) ) )
135	132, 133, 134	syl2anc 667	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
136	131, 135	mpbid 214	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( y e. RR /\ ( -u pi - X ) <_ y /\ y <_ ( pi - X ) ) )
137	136	simp1d 1020	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. RR )
138	130, 137	readdcld 9670	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) e. RR )
139	129, 138	ffvelrnd 6023	. . . . . . . . 9 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
140	139	adantlr 721	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
141	77	ad2antlr 733	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( D ` n ) : RR --> RR )
142	137	adantlr 721	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y e. RR )
143	141, 142	ffvelrnd 6023	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( D ` n ) ` y ) e. RR )
144	143	recnd 9669	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( D ` n ) ` y ) e. CC )
145	140, 144	mulcld 9663	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) e. CC )
146	125, 128, 145	itgioo 22773	. . . . . 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 ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
147	23	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi e. RR )
148	22	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> pi e. RR )
149	64	recnd 9669	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. CC )
150	126	recnd 9669	. . . . . . . . . . . . . . . . 17 |- ( ph -> pi e. CC )
151	150	negcld 9973	. . . . . . . . . . . . . . . 16 |- ( ph -> -u pi e. CC )
152	149, 151	pncan3d 9989	. . . . . . . . . . . . . . 15 |- ( ph -> ( X + ( -u pi - X ) ) = -u pi )
153	152	eqcomd 2457	. . . . . . . . . . . . . 14 |- ( ph -> -u pi = ( X + ( -u pi - X ) ) )
154	153	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi = ( X + ( -u pi - X ) ) )
155	136	simp2d 1021	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) <_ y )
156	132, 137, 130, 155	leadd2dd 10228	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + ( -u pi - X ) ) <_ ( X + y ) )
157	154, 156	eqbrtrd 4423	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> -u pi <_ ( X + y ) )
158	136	simp3d 1022	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> y <_ ( pi - X ) )
159	137, 133, 130, 158	leadd2dd 10228	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) <_ ( X + ( pi - X ) ) )
160	149	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> X e. CC )
161	150	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> pi e. CC )
162	160, 161	pncan3d 9989	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + ( pi - X ) ) = pi )
163	159, 162	breqtrd 4427	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) <_ pi )
164	147, 148, 138, 157, 163	eliccd 37601	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( X + y ) e. ( -u pi [,] pi ) )
165		fvres 5879	. . . . . . . . . . 11 |- ( ( X + y ) e. ( -u pi [,] pi ) -> ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
166	164, 165	syl 17	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
167	166	eqcomd 2457	. . . . . . . . 9 |- ( ( ph /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) )
168	167	adantlr 721	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u pi [,] pi ) ) ` ( X + y ) ) )
169	168	oveq1d 6305	. . . . . . 7 |- ( ( ( 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 ) ) )
170	169	itgeq2dv 22739	. . . . . 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 )
171	122, 146, 170	3eqtrrd 2490	. . . . 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 )
172	116, 171	eqtrd 2485	. . . 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 )
173	85, 90, 172	3eqtrd 2489	. . 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 )
174		elioore 11666	. . . . . . . . 9 |- ( s e. ( ( -u pi - X ) (,) ( pi - X ) ) -> s e. RR )
175	174	adantl 468	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> s e. RR )
176	36	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> F : RR --> CC )
177	64	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> X e. RR )
178	174	adantl 468	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> s e. RR )
179	177, 178	readdcld 9670	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( X + s ) e. RR )
180	176, 179	ffvelrnd 6023	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
181	180	adantlr 721	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
182	77	ad2antlr 733	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( D ` n ) : RR --> RR )
183	182, 175	ffvelrnd 6023	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( D ` n ) ` s ) e. RR )
184	183	recnd 9669	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( D ` n ) ` s ) e. CC )
185	181, 184	mulcld 9663	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
186		fourierdlem111.g	. . . . . . . . . 10 |- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
187		oveq2 6298	. . . . . . . . . . . . 13 |- ( x = s -> ( X + x ) = ( X + s ) )
188	187	fveq2d 5869	. . . . . . . . . . . 12 |- ( x = s -> ( F ` ( X + x ) ) = ( F ` ( X + s ) ) )
189		fveq2 5865	. . . . . . . . . . . 12 |- ( x = s -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` s ) )
190	188, 189	oveq12d 6308	. . . . . . . . . . 11 |- ( x = s -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
191	190	cbvmptv 4495	. . . . . . . . . 10 |- ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) ) = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
192	186, 191	eqtri 2473	. . . . . . . . 9 |- G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
193	192	fvmpt2 5957	. . . . . . . 8 |- ( ( s e. RR /\ ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
194	175, 185, 193	syl2anc 667	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
195	194	eqcomd 2457	. . . . . 6 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) (,) ( pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
196	195	itgeq2dv 22739	. . . . 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 )
197	36	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> F : RR --> CC )
198	64	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> X e. RR )
199		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. RR )
200	198, 199	readdcld 9670	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( X + x ) e. RR )
201	197, 200	ffvelrnd 6023	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
202	201	adantlr 721	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
203	77	adantl 468	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. NN ) -> ( D ` n ) : RR --> RR )
204	203	ffvelrnda 6022	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. RR )
205	204	recnd 9669	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. CC )
206	202, 205	mulcld 9663	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC )
207	206, 186	fmptd 6046	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> G : RR --> CC )
208	207	adantr 467	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> G : RR --> CC )
209	124	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( -u pi - X ) e. RR )
210	127	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( pi - X ) e. RR )
211		simpr 463	. . . . . . . . . 10 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. ( ( -u pi - X ) [,] ( pi - X ) ) )
212		eliccre 37603	. . . . . . . . . 10 |- ( ( ( -u pi - X ) e. RR /\ ( pi - X ) e. RR /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
213	209, 210, 211, 212	syl3anc 1268	. . . . . . . . 9 |- ( ( ph /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
214	213	adantlr 721	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> s e. RR )
215	208, 214	ffvelrnd 6023	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u pi - X ) [,] ( pi - X ) ) ) -> ( G ` s ) e. CC )
216	125, 128, 215	itgioo 22773	. . . . . 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 )
217		fveq2 5865	. . . . . . 7 |- ( s = x -> ( G ` s ) = ( G ` x ) )
218	217	cbvitgv 22734	. . . . . 6 |- S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` s ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( G ` x ) _d x
219	216, 218	syl6eq 2501	. . . . 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 )
220	196, 219	eqtrd 2485	. . . 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 )
221		eqid 2451	. . . . . . 7 |- ( ( pi - X ) - ( -u pi - X ) ) = ( ( pi - X ) - ( -u pi - X ) )
222	111	renegcld 10046	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> -u X e. RR )
223		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 ) ) ) } )
224	31	fourierdlem2 37971	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) ) )
225	32, 224	syl 17	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) ) )
226	33, 225	mpbid 214	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
227	226	simpld 461	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
228		elmapi 7493	. . . . . . . . . . . . . . 15 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
229	227, 228	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> Q : ( 0 ... M ) --> RR )
230	229	fnvinran 37335	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
231	64	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
232	230, 231	resubcld 10047	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
233		fourierdlem111.14	. . . . . . . . . . . 12 |- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
234	232, 233	fmptd 6046	. . . . . . . . . . 11 |- ( ph -> W : ( 0 ... M ) --> RR )
235		reex 9630	. . . . . . . . . . . . 13 |- RR e. _V
236		ovex 6318	. . . . . . . . . . . . 13 |- ( 0 ... M ) e. _V
237	235, 236	pm3.2i 457	. . . . . . . . . . . 12 |- ( RR e. _V /\ ( 0 ... M ) e. _V )
238		elmapg 7485	. . . . . . . . . . . 12 |- ( ( RR e. _V /\ ( 0 ... M ) e. _V ) -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
239	237, 238	mp1i 13	. . . . . . . . . . 11 |- ( ph -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
240	234, 239	mpbird 236	. . . . . . . . . 10 |- ( ph -> W e. ( RR ^m ( 0 ... M ) ) )
241	233	a1i 11	. . . . . . . . . . . 12 |- ( ph -> W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
242		fveq2 5865	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
243	226	simprd 465	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
244	243	simpld 461	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) )
245	244	simpld 461	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` 0 ) = -u pi )
246	242, 245	sylan9eqr 2507	. . . . . . . . . . . . 13 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = -u pi )
247	246	oveq1d 6305	. . . . . . . . . . . 12 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( -u pi - X ) )
248		0zd 10949	. . . . . . . . . . . . . 14 |- ( ph -> 0 e. ZZ )
249	32	nnzd 11039	. . . . . . . . . . . . . 14 |- ( ph -> M e. ZZ )
250		0red 9644	. . . . . . . . . . . . . . . 16 |- ( M e. NN -> 0 e. RR )
251		nnre 10616	. . . . . . . . . . . . . . . 16 |- ( M e. NN -> M e. RR )
252		nngt0 10638	. . . . . . . . . . . . . . . 16 |- ( M e. NN -> 0 < M )
253	250, 251, 252	ltled 9783	. . . . . . . . . . . . . . 15 |- ( M e. NN -> 0 <_ M )
254	32, 253	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ M )
255		eluz2 11165	. . . . . . . . . . . . . 14 |- ( M e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 <_ M ) )
256	248, 249, 254, 255	syl3anbrc 1192	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 0 ) )
257		eluzfz1 11806	. . . . . . . . . . . . 13 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
258	256, 257	syl 17	. . . . . . . . . . . 12 |- ( ph -> 0 e. ( 0 ... M ) )
259	241, 247, 258, 124	fvmptd 5954	. . . . . . . . . . 11 |- ( ph -> ( W ` 0 ) = ( -u pi - X ) )
260		fveq2 5865	. . . . . . . . . . . . . 14 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
261	244	simprd 465	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` M ) = pi )
262	260, 261	sylan9eqr 2507	. . . . . . . . . . . . 13 |- ( ( ph /\ i = M ) -> ( Q ` i ) = pi )
263	262	oveq1d 6305	. . . . . . . . . . . 12 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( pi - X ) )
264		eluzfz2 11807	. . . . . . . . . . . . 13 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
265	256, 264	syl 17	. . . . . . . . . . . 12 |- ( ph -> M e. ( 0 ... M ) )
266	241, 263, 265, 127	fvmptd 5954	. . . . . . . . . . 11 |- ( ph -> ( W ` M ) = ( pi - X ) )
267	259, 266	jca 535	. . . . . . . . . 10 |- ( ph -> ( ( W ` 0 ) = ( -u pi - X ) /\ ( W ` M ) = ( pi - X ) ) )
268	229	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
269		elfzofz 11935	. . . . . . . . . . . . . . 15 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
270	269	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
271	268, 270	ffvelrnd 6023	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
272		fzofzp1 12008	. . . . . . . . . . . . . . 15 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
273	272	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
274	268, 273	ffvelrnd 6023	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
275	64	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
276	243	simprd 465	. . . . . . . . . . . . . 14 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
277	276	r19.21bi 2757	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
278	271, 274, 275, 277	ltsub1dd 10225	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
279	270, 232	syldan 473	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
280	233	fvmpt2 5957	. . . . . . . . . . . . 13 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
281	270, 279, 280	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
282		fveq2 5865	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
283	282	oveq1d 6305	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
284	283	cbvmptv 4495	. . . . . . . . . . . . . . 15 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
285	233, 284	eqtri 2473	. . . . . . . . . . . . . 14 |- W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
286	285	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
287		fveq2 5865	. . . . . . . . . . . . . . 15 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
288	287	oveq1d 6305	. . . . . . . . . . . . . 14 |- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
289	288	adantl 468	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
290	274, 275	resubcld 10047	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
291	286, 289, 273, 290	fvmptd 5954	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
292	278, 281, 291	3brtr4d 4433	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) < ( W ` ( i + 1 ) ) )
293	292	ralrimiva 2802	. . . . . . . . . 10 |- ( ph -> A. i e. ( 0..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) )
294	240, 267, 293	jca32 538	. . . . . . . . 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 ) ) ) ) )
295	223	fourierdlem2 37971	. . . . . . . . . 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 ) ) ) ) ) )
296	32, 295	syl 17	. . . . . . . . 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 ) ) ) ) ) )
297	294, 296	mpbird 236	. . . . . . . 8 |- ( ph -> W e. ( O ` M ) )
298	297	adantr 467	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> W e. ( O ` M ) )
299	150, 151, 149	nnncan2d 10021	. . . . . . . . . . . 12 |- ( ph -> ( ( pi - X ) - ( -u pi - X ) ) = ( pi - -u pi ) )
300		picn 23414	. . . . . . . . . . . . . 14 |- pi e. CC
301	300	2timesi 10730	. . . . . . . . . . . . 13 |- ( 2 x. pi ) = ( pi + pi )
302		fourierdlem111.t	. . . . . . . . . . . . 13 |- T = ( 2 x. pi )
303	300, 300	subnegi 9953	. . . . . . . . . . . . 13 |- ( pi - -u pi ) = ( pi + pi )
304	301, 302, 303	3eqtr4i 2483	. . . . . . . . . . . 12 |- T = ( pi - -u pi )
305	299, 304	syl6eqr 2503	. . . . . . . . . . 11 |- ( ph -> ( ( pi - X ) - ( -u pi - X ) ) = T )
306	305	oveq2d 6306	. . . . . . . . . 10 |- ( ph -> ( x + ( ( pi - X ) - ( -u pi - X ) ) ) = ( x + T ) )
307	306	fveq2d 5869	. . . . . . . . 9 |- ( ph -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` ( x + T ) ) )
308	307	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` ( x + T ) ) )
309		simpr 463	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR )
310	186	fvmpt2 5957	. . . . . . . . . 10 |- ( ( x e. RR /\ ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
311	309, 206, 310	syl2anc 667	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
312	149	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> X e. CC )
313	199	recnd 9669	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> x e. CC )
314		2re 10679	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
315	314, 22	remulcli 9657	. . . . . . . . . . . . . . . . . . 19 |- ( 2 x. pi ) e. RR
316	302, 315	eqeltri 2525	. . . . . . . . . . . . . . . . . 18 |- T e. RR
317	316	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. RR )
318	317	recnd 9669	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. CC )
319	318	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> T e. CC )
320	312, 313, 319	addassd 9665	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( ( X + x ) + T ) = ( X + ( x + T ) ) )
321	320	eqcomd 2457	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) = ( ( X + x ) + T ) )
322	321	fveq2d 5869	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) = ( F ` ( ( X + x ) + T ) ) )
323		simpl 459	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ph )
324	323, 200	jca 535	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( ph /\ ( X + x ) e. RR ) )
325		eleq1 2517	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( s e. RR <-> ( X + x ) e. RR ) )
326	325	anbi2d 710	. . . . . . . . . . . . . . 15 |- ( s = ( X + x ) -> ( ( ph /\ s e. RR ) <-> ( ph /\ ( X + x ) e. RR ) ) )
327		oveq1 6297	. . . . . . . . . . . . . . . . 17 |- ( s = ( X + x ) -> ( s + T ) = ( ( X + x ) + T ) )
328	327	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( F ` ( s + T ) ) = ( F ` ( ( X + x ) + T ) ) )
329		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( s = ( X + x ) -> ( F ` s ) = ( F ` ( X + x ) ) )
330	328, 329	eqeq12d 2466	. . . . . . . . . . . . . . 15 |- ( s = ( X + x ) -> ( ( F ` ( s + T ) ) = ( F ` s ) <-> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
331	326, 330	imbi12d 322	. . . . . . . . . . . . . 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 ) ) ) ) )
332		eleq1 2517	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x e. RR <-> s e. RR ) )
333	332	anbi2d 710	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( ( ph /\ x e. RR ) <-> ( ph /\ s e. RR ) ) )
334		oveq1 6297	. . . . . . . . . . . . . . . . . 18 |- ( x = s -> ( x + T ) = ( s + T ) )
335	334	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( F ` ( x + T ) ) = ( F ` ( s + T ) ) )
336		fveq2 5865	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( F ` x ) = ( F ` s ) )
337	335, 336	eqeq12d 2466	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( s + T ) ) = ( F ` s ) ) )
338	333, 337	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( x = s -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) ) ) )
339		fourierdlem111.fper	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
340	338, 339	chvarv 2107	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) )
341	331, 340	vtoclg 3107	. . . . . . . . . . . . 13 |- ( ( X + x ) e. RR -> ( ( ph /\ ( X + x ) e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
342	200, 324, 341	sylc 62	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) )
343	322, 342	eqtr2d 2486	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
344	343	adantlr 721	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
345	67, 302	dirkerper 37958	. . . . . . . . . . . 12 |- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) = ( ( D ` n ) ` x ) )
346	345	eqcomd 2457	. . . . . . . . . . 11 |- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
347	346	adantll 720	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
348	344, 347	oveq12d 6308	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
349	192	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
350		oveq2 6298	. . . . . . . . . . . . . 14 |- ( s = ( x + T ) -> ( X + s ) = ( X + ( x + T ) ) )
351	350	fveq2d 5869	. . . . . . . . . . . . 13 |- ( s = ( x + T ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( x + T ) ) ) )
352		fveq2 5865	. . . . . . . . . . . . 13 |- ( s = ( x + T ) -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` ( x + T ) ) )
353	351, 352	oveq12d 6308	. . . . . . . . . . . 12 |- ( s = ( x + T ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
354	353	adantl 468	. . . . . . . . . . 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 ) ) ) )
355	316	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> T e. RR )
356	309, 355	readdcld 9670	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x + T ) e. RR )
357	316	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. RR ) -> T e. RR )
358	199, 357	readdcld 9670	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
359	198, 358	readdcld 9670	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) e. RR )
360	197, 359	ffvelrnd 6023	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
361	360	adantlr 721	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
362	77	ad2antlr 733	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( D ` n ) : RR --> RR )
363	362, 356	ffvelrnd 6023	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. RR )
364	363	recnd 9669	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. CC )
365	361, 364	mulcld 9663	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) e. CC )
366	349, 354, 356, 365	fvmptd 5954	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
367	366	eqcomd 2457	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) = ( G ` ( x + T ) ) )
368	311, 348, 367	3eqtrrd 2490	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( G ` x ) )
369	308, 368	eqtrd 2485	. . . . . . 7 |- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( pi - X ) - ( -u pi - X ) ) ) ) = ( G ` x ) )
370	192	reseq1i 5101	. . . . . . . . . 10 |- ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
371	370	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 ) ) ) ) )
372		ioossre 11696	. . . . . . . . . 10 |- ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR
373		resmpt 5154	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) )
374	372, 373	ax-mp 5	. . . . . . . . 9 |- ( ( 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 ) ) )
375	371, 374	syl6eq 2501	. . . . . . . 8 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
376	271	rexrd 9690	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
377	376	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
378	274	rexrd 9690	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
379	378	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
380	64	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
381		elioore 11666	. . . . . . . . . . . . . . . 16 |- ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -> s e. RR )
382	381	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> s e. RR )
383	380, 382	readdcld 9670	. . . . . . . . . . . . . 14 |- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
384	383	adantlr 721	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
385		eleq1 2517	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) <-> s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
386	385	anbi2d 710	. . . . . . . . . . . . . . 15 |- ( x = s -> ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) <-> ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ) )
387	187	breq2d 4414	. . . . . . . . . . . . . . 15 |- ( x = s -> ( ( Q ` i ) < ( X + x ) <-> ( Q ` i ) < ( X + s ) ) )
388	386, 387	imbi12d 322	. . . . . . . . . . . . . 14 |- ( x = s -> ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + x ) ) <-> ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + s ) ) ) )
389	149	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. CC )
390	281, 279	eqeltrd 2529	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) e. RR )
391	390	recnd 9669	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) e. CC )
392	389, 391	addcomd 9835	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( W ` i ) ) = ( ( W ` i ) + X ) )
393	281	oveq1d 6305	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( W ` i ) + X ) = ( ( ( Q ` i ) - X ) + X ) )
394	271	recnd 9669	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
395	394, 389	npcand 9990	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) - X ) + X ) = ( Q ` i ) )
396	392, 393, 395	3eqtrrd 2490	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( X + ( W ` i ) ) )
397	396	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( W ` i ) ) )
398	390	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR )
399		elioore 11666	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -> x e. RR )
400	399	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x e. RR )
401	64	ad2antrr 732	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
402	390	rexrd 9690	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` i ) e. RR* )
403	402	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR* )
404	291, 290	eqeltrd 2529	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` ( i + 1 ) ) e. RR )
405	404	rexrd 9690	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( W ` ( i + 1 ) ) e. RR* )
406	405	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR* )
407		simpr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
408		ioogtlb 37592	. . . . . . . . . . . . . . . . 17 |- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < x )
409	403, 406, 407, 408	syl3anc 1268	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < x )
410	398, 400, 401, 409	ltadd2dd 9794	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + ( W ` i ) ) < ( X + x ) )
411	397, 410	eqbrtrd 4423	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + x ) )
412	388, 411	chvarv 2107	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + s ) )
413	187	breq1d 4412	. . . . . . . . . . . . . . 15 |- ( x = s -> ( ( X + x ) < ( Q ` ( i + 1 ) ) <-> ( X + s ) < ( Q ` ( i + 1 ) ) ) )
414	386, 413	imbi12d 322	. . . . . . . . . . . . . 14 |- ( x = s -> ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) < ( Q ` ( i + 1 ) ) ) ) )
415	404	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR )
416		iooltub 37610	. . . . . . . . . . . . . . . . 17 |- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x < ( W ` ( i + 1 ) ) )
417	403, 406, 407, 416	syl3anc 1268	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x < ( W ` ( i + 1 ) ) )
418	400, 415, 401, 417	ltadd2dd 9794	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) < ( X + ( W ` ( i + 1