Theorem fourierdlem104 31834

Description: The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem104.f	|- ( ph -> F : RR --> RR )
fourierdlem104.xre	|- ( ph -> X e. RR )
fourierdlem104.p	|- P = ( 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 ) ) ) } )
fourierdlem104.m	|- ( ph -> M e. NN )
fourierdlem104.v	|- ( ph -> V e. ( P ` M ) )
fourierdlem104.x	|- ( ph -> X e. ran V )
fourierdlem104.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem104.fbdioo	|- ( ( ph /\ i e. ( 0..^ M ) ) -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
fourierdlem104.fdvcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
fourierdlem104.fdvbd	|- ( ( ph /\ i e. ( 0..^ M ) ) -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
fourierdlem104.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
fourierdlem104.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
fourierdlem104.h	|- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem104.k	|- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem104.u	|- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem104.s	|- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
fourierdlem104.g	|- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem104.z	|- Z = ( m e. NN |-> S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
fourierdlem104.e	|- E = ( n e. NN |-> ( S. ( 0 (,) pi ) ( G ` s ) _d s / pi ) )
fourierdlem104.y	|- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
fourierdlem104.w	|- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
fourierdlem104.a	|- ( ph -> A e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) lim CC X ) )
fourierdlem104.b	|- ( ph -> B e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) lim CC X ) )
fourierdlem104.d	|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
fourierdlem104.o	|- O = ( U |` ( d [,] pi ) )
fourierdlem104.t	|- T = ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
fourierdlem104.n	|- N = ( ( # ` T ) - 1 )
fourierdlem104.j	|- J = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem104.q	|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem104.1	|- C = ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) )
fourierdlem104.ch	|- ( ch <-> ( ( ( ( ( ph /\ e e. RR+ ) /\ d e. ( 0 (,) pi ) ) /\ k e. NN ) /\ ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) /\ ( abs ` S. ( d (,) pi ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )

Assertion

Ref	Expression
fourierdlem104	|- ( ph -> Z ~~> ( Y / 2 ) )

Distinct variable groups:   A, s   B, s   C, i, t, w, z   D, i, m, s   n, E   i, F, k, l, s, t   m, F, k   w, F, z, k, s   e, G, k, s   i, G, t   i, H, s   k, J, l, s   f, J, k   i, J, t   m, J   w, J, z   K, s   L, l, s, t   k, M, l, s, i, t   m, M, p, i   i, N, k, l, s, t   e, N, l   f, N   m, N   w, N, z   e, O, l, s, k   t, O   Q, l, s   Q, f   Q, i, t   Q, p   R, l, s, t   S, s   T, f   U, d, k, s, l   U, n, k, s   i, V, k, s   V, p   t, V   W, s   i, X, k, l, s, t   m, X, p   w, X, z   i, Y, k, l, s, t   m, Y, n, i   w, Y, z   n, Z   e, d   i, d, ph, t, k, l, s   ph, e   ch, s   f, d, ph   w, d, z, ph   e, n, ph   ph, m

Allowed substitution hints:   ph( p)   ch( z, w, t, e, f, i, k, m, n, p, d, l)   A( z, w, t, e, f, i, k, m, n, p, d, l)   B( z, w, t, e, f, i, k, m, n, p, d, l)   C( e, f, k, m, n, s, p, d, l)   D( z, w, t, e, f, k, n, p, d, l)   P( z, w, t, e, f, i, k, m, n, s, p, d, l)   Q( z, w, e, k, m, n, d)   R( z, w, e, f, i, k, m, n, p, d)   S( z, w, t, e, f, i, k, m, n, p, d, l)   T( z, w, t, e, i, k, m, n, s, p, d, l)   U( z, w, t, e, f, i, m, p)   E( z, w, t, e, f, i, k, m, s, p, d, l)   F( e, f, n, p, d)   G( z, w, f, m, n, p, d, l)   H( z, w, t, e, f, k, m, n, p, d, l)   J( e, n, p, d)   K( z, w, t, e, f, i, k, m, n, p, d, l)   L( z, w, e, f, i, k, m, n, p, d)   M( z, w, e, f, n, d)   N( n, p, d)   O( z, w, f, i, m, n, p, d)   V( z, w, e, f, m, n, d, l)   W( z, w, t, e, f, i, k, m, n, p, d, l)   X( e, f, n, d)   Y( e, f, p, d)   Z( z, w, t, e, f, i, k, m, s, p, d, l)

Proof of Theorem fourierdlem104

Dummy variables .|| b r c u j y x h v a are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2467	. . 3 |- ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
2		1z 10906	. . . 4 |- 1 e. ZZ
3	2	a1i 11	. . 3 |- ( ph -> 1 e. ZZ )
4		nfv 1683	. . . . 5 |- F/ n ph
5		nfmpt1 4542	. . . . 5 |- F/_ n ( n e. NN |-> S. ( 0 (,) pi ) ( G ` s ) _d s )
6		nfmpt1 4542	. . . . 5 |- F/_ n ( n e. NN |-> pi )
7		fourierdlem104.e	. . . . . 6 |- E = ( n e. NN |-> ( S. ( 0 (,) pi ) ( G ` s ) _d s / pi ) )
8		nfmpt1 4542	. . . . . 6 |- F/_ n ( n e. NN |-> ( S. ( 0 (,) pi ) ( G ` s ) _d s / pi ) )
9	7, 8	nfcxfr 2627	. . . . 5 |- F/_ n E
10		nnuz 11129	. . . . 5 |- NN = ( ZZ>= ` 1 )
11		fourierdlem104.f	. . . . . . . . . 10 |- ( ph -> F : RR --> RR )
12		fourierdlem104.xre	. . . . . . . . . 10 |- ( ph -> X e. RR )
13		ioossre 11598	. . . . . . . . . . . . 13 |- ( X (,) +oo ) C_ RR
14	13	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( X (,) +oo ) C_ RR )
15	11, 14	fssresd 5758	. . . . . . . . . . 11 |- ( ph -> ( F |` ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
16		ioosscn 31414	. . . . . . . . . . . 12 |- ( X (,) +oo ) C_ CC
17	16	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( X (,) +oo ) C_ CC )
18		eqid 2467	. . . . . . . . . . . 12 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
19		pnfxr 11333	. . . . . . . . . . . . 13 |- +oo e. RR*
20	19	a1i 11	. . . . . . . . . . . 12 |- ( ph -> +oo e. RR* )
21	12	ltpnfd 31380	. . . . . . . . . . . 12 |- ( ph -> X < +oo )
22	18, 20, 12, 21	lptioo1cn 31511	. . . . . . . . . . 11 |- ( ph -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( X (,) +oo ) ) )
23		fourierdlem104.y	. . . . . . . . . . 11 |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
24	15, 17, 22, 23	limcrecl 31494	. . . . . . . . . 10 |- ( ph -> Y e. RR )
25		ioossre 11598	. . . . . . . . . . . . 13 |- ( -oo (,) X ) C_ RR
26	25	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( -oo (,) X ) C_ RR )
27	11, 26	fssresd 5758	. . . . . . . . . . 11 |- ( ph -> ( F |` ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
28		ioosscn 31414	. . . . . . . . . . . 12 |- ( -oo (,) X ) C_ CC
29	28	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( -oo (,) X ) C_ CC )
30		mnfxr 11335	. . . . . . . . . . . . 13 |- -oo e. RR*
31	30	a1i 11	. . . . . . . . . . . 12 |- ( ph -> -oo e. RR* )
32	12	mnfltd 31391	. . . . . . . . . . . 12 |- ( ph -> -oo < X )
33	18, 31, 12, 32	lptioo2cn 31510	. . . . . . . . . . 11 |- ( ph -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( -oo (,) X ) ) )
34		fourierdlem104.w	. . . . . . . . . . 11 |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
35	27, 29, 33, 34	limcrecl 31494	. . . . . . . . . 10 |- ( ph -> W e. RR )
36		fourierdlem104.h	. . . . . . . . . 10 |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
37		fourierdlem104.k	. . . . . . . . . 10 |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
38		fourierdlem104.u	. . . . . . . . . 10 |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
39		fourierdlem104.s	. . . . . . . . . 10 |- S = ( s e. ( -u pi [,] pi ) |-> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) )
40		fourierdlem104.g	. . . . . . . . . 10 |- G = ( s e. ( -u pi [,] pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
41		pire 22718	. . . . . . . . . . . . 13 |- pi e. RR
42	41	renegcli 9892	. . . . . . . . . . . 12 |- -u pi e. RR
43	42	a1i 11	. . . . . . . . . . 11 |- ( ph -> -u pi e. RR )
44	41	a1i 11	. . . . . . . . . . 11 |- ( ph -> pi e. RR )
45		negpilt0 31362	. . . . . . . . . . . . . 14 |- -u pi < 0
46		pipos 22720	. . . . . . . . . . . . . 14 |- 0 < pi
47		0re 9608	. . . . . . . . . . . . . . 15 |- 0 e. RR
48	42, 47, 41	lttri 9722	. . . . . . . . . . . . . 14 |- ( ( -u pi < 0 /\ 0 < pi ) -> -u pi < pi )
49	45, 46, 48	mp2an 672	. . . . . . . . . . . . 13 |- -u pi < pi
50	42, 41	ltlei 9718	. . . . . . . . . . . . 13 |- ( -u pi < pi -> -u pi <_ pi )
51	49, 50	ax-mp 5	. . . . . . . . . . . 12 |- -u pi <_ pi
52	51	a1i 11	. . . . . . . . . . 11 |- ( ph -> -u pi <_ pi )
53	11, 12, 24, 35, 36	fourierdlem9 31739	. . . . . . . . . . 11 |- ( ph -> H : ( -u pi [,] pi ) --> RR )
54		fourierdlem104.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
55		fourierdlem104.v	. . . . . . . . . . . . . . . . 17 |- ( ph -> V e. ( P ` M ) )
56		fourierdlem104.p	. . . . . . . . . . . . . . . . . . 19 |- P = ( 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 ) ) ) } )
57	56	fourierdlem2 31732	. . . . . . . . . . . . . . . . . 18 |- ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) /\ A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
58	54, 57	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) /\ A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
59	55, 58	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) /\ A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
60	59	simpld 459	. . . . . . . . . . . . . . 15 |- ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
61		elmapi 7452	. . . . . . . . . . . . . . 15 |- ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
62	60, 61	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> V : ( 0 ... M ) --> RR )
63	62	ffvelrnda 6032	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( V ` i ) e. RR )
64	12	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
65	63, 64	resubcld 9999	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) - X ) e. RR )
66		fourierdlem104.q	. . . . . . . . . . . 12 |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
67	65, 66	fmptd 6056	. . . . . . . . . . 11 |- ( ph -> Q : ( 0 ... M ) --> RR )
68	66	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) )
69		fveq2 5872	. . . . . . . . . . . . . . 15 |- ( i = 0 -> ( V ` i ) = ( V ` 0 ) )
70	69	oveq1d 6310	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
71	70	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i = 0 ) -> ( ( V ` i ) - X ) = ( ( V ` 0 ) - X ) )
72	54	nnnn0d 10864	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN0 )
73		nn0uz 11128	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
74	72, 73	syl6eleq 2565	. . . . . . . . . . . . . 14 |- ( ph -> M e. ( ZZ>= ` 0 ) )
75		eluzfz1 11705	. . . . . . . . . . . . . 14 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
76	74, 75	syl 16	. . . . . . . . . . . . 13 |- ( ph -> 0 e. ( 0 ... M ) )
77	62, 76	ffvelrnd 6033	. . . . . . . . . . . . . 14 |- ( ph -> ( V ` 0 ) e. RR )
78	77, 12	resubcld 9999	. . . . . . . . . . . . 13 |- ( ph -> ( ( V ` 0 ) - X ) e. RR )
79	68, 71, 76, 78	fvmptd 5962	. . . . . . . . . . . 12 |- ( ph -> ( Q ` 0 ) = ( ( V ` 0 ) - X ) )
80	59	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) /\ A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) )
81	80	simpld 459	. . . . . . . . . . . . . 14 |- ( ph -> ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) )
82	81	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> ( V ` 0 ) = ( -u pi + X ) )
83	82	oveq1d 6310	. . . . . . . . . . . 12 |- ( ph -> ( ( V ` 0 ) - X ) = ( ( -u pi + X ) - X ) )
84		ax-resscn 9561	. . . . . . . . . . . . . 14 |- RR C_ CC
85	84, 43	sseldi 3507	. . . . . . . . . . . . 13 |- ( ph -> -u pi e. CC )
86	12	recnd 9634	. . . . . . . . . . . . 13 |- ( ph -> X e. CC )
87	85, 86	pncand 9943	. . . . . . . . . . . 12 |- ( ph -> ( ( -u pi + X ) - X ) = -u pi )
88	79, 83, 87	3eqtrd 2512	. . . . . . . . . . 11 |- ( ph -> ( Q ` 0 ) = -u pi )
89		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) } ) = ( 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 ) ) ) } )
90	43, 44, 12, 56, 89, 54, 55, 66	fourierdlem14 31744	. . . . . . . . . . . . . . 15 |- ( ph -> Q e. ( ( 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 ) ) ) } ) ` M ) )
91	89	fourierdlem2 31732	. . . . . . . . . . . . . . . 16 |- ( M e. NN -> ( Q e. ( ( 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 ) ) ) } ) ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
92	54, 91	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( Q e. ( ( 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 ) ) ) } ) ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
93	90, 92	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
94	93	simprd 463	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
95	94	simpld 459	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) )
96	95	simprd 463	. . . . . . . . . . 11 |- ( ph -> ( Q ` M ) = pi )
97	94	simprd 463	. . . . . . . . . . . 12 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
98	97	r19.21bi 2836	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
99	11	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : RR --> RR )
100	89, 54, 90	fourierdlem15 31745	. . . . . . . . . . . . . 14 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
101	100	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
102		elfzofz 11823	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
103	102	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
104	101, 103	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( -u pi [,] pi ) )
105		fzofzp1 11889	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
106	105	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
107	101, 106	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( -u pi [,] pi ) )
108	12	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
109		fourierdlem104.x	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. ran V )
110		ffn 5737	. . . . . . . . . . . . . . . . . 18 |- ( V : ( 0 ... M ) --> RR -> V Fn ( 0 ... M ) )
111	60, 61, 110	3syl 20	. . . . . . . . . . . . . . . . 17 |- ( ph -> V Fn ( 0 ... M ) )
112		fvelrnb 5921	. . . . . . . . . . . . . . . . 17 |- ( V Fn ( 0 ... M ) -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
113	111, 112	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X e. ran V <-> E. i e. ( 0 ... M ) ( V ` i ) = X ) )
114	109, 113	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ph -> E. i e. ( 0 ... M ) ( V ` i ) = X )
115		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( ( V ` i ) = X -> ( ( V ` i ) - X ) = ( X - X ) )
116	115	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( ( V ` i ) - X ) = ( X - X ) )
117	86	subidd 9930	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( X - X ) = 0 )
118	117	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> ( X - X ) = 0 )
119	116, 118	eqtr2d 2509	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ ( V ` i ) = X ) -> 0 = ( ( V ` i ) - X ) )
120	119	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( V ` i ) = X -> 0 = ( ( V ` i ) - X ) ) )
121	120	reximdva 2942	. . . . . . . . . . . . . . 15 |- ( ph -> ( E. i e. ( 0 ... M ) ( V ` i ) = X -> E. i e. ( 0 ... M ) 0 = ( ( V ` i ) - X ) ) )
122	114, 121	mpd 15	. . . . . . . . . . . . . 14 |- ( ph -> E. i e. ( 0 ... M ) 0 = ( ( V ` i ) - X ) )
123	66	elrnmpt 5255	. . . . . . . . . . . . . . 15 |- ( 0 e. RR -> ( 0 e. ran Q <-> E. i e. ( 0 ... M ) 0 = ( ( V ` i ) - X ) ) )
124	47, 123	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 0 e. ran Q <-> E. i e. ( 0 ... M ) 0 = ( ( V ` i ) - X ) )
125	122, 124	sylibr 212	. . . . . . . . . . . . 13 |- ( ph -> 0 e. ran Q )
126	89, 54, 90, 125	fourierdlem12 31742	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> -. 0 e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
127		fourierdlem104.fcn	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
128	62	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> V : ( 0 ... M ) --> RR )
129	128, 103	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` i ) e. RR )
130	129, 108	resubcld 9999	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
131	66	fvmpt2 5964	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
132	103, 130, 131	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
133	132	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + X ) = ( ( ( V ` i ) - X ) + X ) )
134	84, 129	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` i ) e. CC )
135	86	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. CC )
136	134, 135	npcand 9946	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( V ` i ) - X ) + X ) = ( V ` i ) )
137	133, 136	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) + X ) = ( V ` i ) )
138		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = i -> ( V ` j ) = ( V ` i ) )
139	138	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = i -> ( ( V ` j ) - X ) = ( ( V ` i ) - X ) )
140	139	cbvmptv 4544	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
141	66, 140	eqtr4i 2499	. . . . . . . . . . . . . . . . . . . 20 |- Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
142	141	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
143		fveq2 5872	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
144	143	oveq1d 6310	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
145	144	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
146	128, 106	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
147	146, 108	resubcld 9999	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
148	142, 145, 106, 147	fvmptd 5962	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
149	148	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + X ) = ( ( ( V ` ( i + 1 ) ) - X ) + X ) )
150	84, 146	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` ( i + 1 ) ) e. CC )
151	150, 135	npcand 9946	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( V ` ( i + 1 ) ) - X ) + X ) = ( V ` ( i + 1 ) ) )
152	149, 151	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) + X ) = ( V ` ( i + 1 ) ) )
153	137, 152	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
154	153	reseq2d 5279	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) ) = ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) )
155	153	oveq1d 6310	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) -cn-> CC ) = ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
156	154, 155	eleq12d 2549	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) ) e. ( ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) -cn-> CC ) <-> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) ) )
157	127, 156	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) ) e. ( ( ( ( Q ` i ) + X ) (,) ( ( Q ` ( i + 1 ) ) + X ) ) -cn-> CC ) )
158	24	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Y e. RR )
159	35	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> W e. RR )
160	99, 104, 107, 108, 126, 157, 158, 159, 36	fourierdlem40 31770	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
161		fourierdlem104.r	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
162		eqid 2467	. . . . . . . . . . . 12 |- ( RR _D F ) = ( RR _D F )
163		fourierdlem104.fdvcn	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
164		cncff 21265	. . . . . . . . . . . . 13 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
165		id 22	. . . . . . . . . . . . . 14 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
166	84	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR -> RR C_ CC )
167		fss 5745	. . . . . . . . . . . . . 14 |- ( ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR /\ RR C_ CC ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
168	165, 166, 167	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
169	163, 164, 168	3syl 20	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
170		fourierdlem104.b	. . . . . . . . . . . 12 |- ( ph -> B e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) lim CC X ) )
171		eqid 2467	. . . . . . . . . . . 12 |- if ( ( V ` i ) = X , B , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) = if ( ( V ` i ) = X , B , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) )
172	12, 56, 11, 109, 23, 35, 36, 54, 55, 161, 66, 89, 162, 169, 170, 171	fourierdlem75 31805	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> if ( ( V ` i ) = X , B , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
173		fourierdlem104.l	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
174	163, 164	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
175		fourierdlem104.a	. . . . . . . . . . . 12 |- ( ph -> A e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) lim CC X ) )
176		eqid 2467	. . . . . . . . . . . 12 |- if ( ( V ` ( i + 1 ) ) = X , A , ( ( L - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) = if ( ( V ` ( i + 1 ) ) = X , A , ( ( L - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) )
177	12, 56, 11, 109, 24, 34, 36, 54, 55, 173, 66, 89, 162, 174, 175, 176	fourierdlem74 31804	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> if ( ( V ` ( i + 1 ) ) = X , A , ( ( L - if ( ( V ` ( i + 1 ) ) < X , W , Y ) ) / ( Q ` ( i + 1 ) ) ) ) e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
178		fveq2 5872	. . . . . . . . . . . . 13 |- ( j = i -> ( Q ` j ) = ( Q ` i ) )
179		oveq1 6302	. . . . . . . . . . . . . 14 |- ( j = i -> ( j + 1 ) = ( i + 1 ) )
180	179	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
181	178, 180	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = i -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
182	181	cbvmptv 4544	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) |-> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) = ( i e. ( 0..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
183	43, 44, 52, 53, 54, 67, 88, 96, 98, 160, 172, 177, 182	fourierdlem70 31800	. . . . . . . . . 10 |- ( ph -> E. x e. RR A. s e. ( -u pi [,] pi ) ( abs ` ( H ` s ) ) <_ x )
184	11	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> F : RR --> RR )
185	109	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> X e. ran V )
186	23	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
187	34	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
188		nnre 10555	. . . . . . . . . . . 12 |- ( n e. NN -> n e. RR )
189	188	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> n e. RR )
190	54	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> M e. NN )
191	55	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> V e. ( P ` M ) )
192	127	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
193	161	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
194	173	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
195	174	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ i e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
196	175	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> A e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) lim CC X ) )
197	170	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. NN ) -> B e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) lim CC X ) )
198	56, 184, 185, 186, 187, 36, 37, 38, 189, 39, 40, 190, 191, 192, 193, 194, 140, 89, 162, 195, 196, 197	fourierdlem88 31818	. . . . . . . . . 10 |- ( ( ph /\ n e. NN ) -> G e. L^1 )
199		eqid 2467	. . . . . . . . . 10 |- ( ( e / 3 ) / y ) = ( ( e / 3 ) / y )
200		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( t = s -> ( G ` t ) = ( G ` s ) )
201	200	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( t = s -> ( abs ` ( G ` t ) ) = ( abs ` ( G ` s ) ) )
202	201	breq1d 4463	. . . . . . . . . . . . . . . 16 |- ( t = s -> ( ( abs ` ( G ` t ) ) <_ y <-> ( abs ` ( G ` s ) ) <_ y ) )
203	202	cbvralv 3093	. . . . . . . . . . . . . . 15 |- ( A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y <-> A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y )
204	203	ralbii 2898	. . . . . . . . . . . . . 14 |- ( A. n e. NN A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y <-> A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y )
205	204	3anbi3i 1189	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y ) <-> ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y ) )
206	205	anbi1i 695	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y ) /\ u e. dom vol ) <-> ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y ) /\ u e. dom vol ) )
207	206	anbi1i 695	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y ) /\ u e. dom vol ) /\ ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ ( ( e / 3 ) / y ) ) ) <-> ( ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y ) /\ u e. dom vol ) /\ ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ ( ( e / 3 ) / y ) ) ) )
208	207	anbi1i 695	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. t e. ( -u pi [,] pi ) ( abs ` ( G ` t ) ) <_ y ) /\ u e. dom vol ) /\ ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ ( ( e / 3 ) / y ) ) ) /\ n e. NN ) <-> ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. RR+ /\ A. n e. NN A. s e. ( -u pi [,] pi ) ( abs ` ( G ` s ) ) <_ y ) /\ u e. dom vol ) /\ ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ ( ( e / 3 ) / y ) ) ) /\ n e. NN ) )
209	11, 12, 24, 35, 36, 37, 38, 39, 40, 183, 198, 199, 208	fourierdlem87 31817	. . . . . . . . 9 |- ( ( ph /\ e e. RR+ ) -> E. c e. RR+ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
210		iftrue 3951	. . . . . . . . . . . . . . . 16 |- ( c <_ ( pi / 2 ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) = c )
211	210	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) = c )
212		0xr 9652	. . . . . . . . . . . . . . . . 17 |- 0 e. RR*
213	212	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> 0 e. RR* )
214	41	rexri 9658	. . . . . . . . . . . . . . . . 17 |- pi e. RR*
215	214	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> pi e. RR* )
216		rpre 11238	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> c e. RR )
217	216	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> c e. RR )
218		rpgt0 11243	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> 0 < c )
219	218	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> 0 < c )
220	41	rehalfcli 10799	. . . . . . . . . . . . . . . . . . 19 |- ( pi / 2 ) e. RR
221	220	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> ( pi / 2 ) e. RR )
222	221	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> ( pi / 2 ) e. RR )
223	41	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> pi e. RR )
224		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> c <_ ( pi / 2 ) )
225		halfpos 10781	. . . . . . . . . . . . . . . . . . . 20 |- ( pi e. RR -> ( 0 < pi <-> ( pi / 2 ) < pi ) )
226	41, 225	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( 0 < pi <-> ( pi / 2 ) < pi )
227	46, 226	mpbi 208	. . . . . . . . . . . . . . . . . 18 |- ( pi / 2 ) < pi
228	227	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> ( pi / 2 ) < pi )
229	217, 222, 223, 224, 228	lelttrd 9751	. . . . . . . . . . . . . . . 16 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> c < pi )
230	213, 215, 217, 219, 229	eliood 31418	. . . . . . . . . . . . . . 15 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> c e. ( 0 (,) pi ) )
231	211, 230	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) )
232		iffalse 3954	. . . . . . . . . . . . . . . 16 |- ( -. c <_ ( pi / 2 ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) = ( pi / 2 ) )
233		2pos 10639	. . . . . . . . . . . . . . . . . . 19 |- 0 < 2
234		2re 10617	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
235	41, 234	divgt0i 10466	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 < pi /\ 0 < 2 ) -> 0 < ( pi / 2 ) )
236	46, 233, 235	mp2an 672	. . . . . . . . . . . . . . . . . 18 |- 0 < ( pi / 2 )
237		elioo2 11582	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 e. RR* /\ pi e. RR* ) -> ( ( pi / 2 ) e. ( 0 (,) pi ) <-> ( ( pi / 2 ) e. RR /\ 0 < ( pi / 2 ) /\ ( pi / 2 ) < pi ) ) )
238	212, 214, 237	mp2an 672	. . . . . . . . . . . . . . . . . 18 |- ( ( pi / 2 ) e. ( 0 (,) pi ) <-> ( ( pi / 2 ) e. RR /\ 0 < ( pi / 2 ) /\ ( pi / 2 ) < pi ) )
239	220, 236, 227, 238	mpbir3an 1178	. . . . . . . . . . . . . . . . 17 |- ( pi / 2 ) e. ( 0 (,) pi )
240	239	a1i 11	. . . . . . . . . . . . . . . 16 |- ( -. c <_ ( pi / 2 ) -> ( pi / 2 ) e. ( 0 (,) pi ) )
241	232, 240	eqeltrd 2555	. . . . . . . . . . . . . . 15 |- ( -. c <_ ( pi / 2 ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) )
242	241	adantl 466	. . . . . . . . . . . . . 14 |- ( ( c e. RR+ /\ -. c <_ ( pi / 2 ) ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) )
243	231, 242	pm2.61dan 789	. . . . . . . . . . . . 13 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) )
244	243	3ad2ant2 1018	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) )
245		ioombl 21843	. . . . . . . . . . . . . . . 16 |- ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) e. dom vol
246	245	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) e. dom vol )
247		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
248	246, 247	jca 532	. . . . . . . . . . . . . 14 |- ( ( c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) e. dom vol /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
249		ioossicc 11622	. . . . . . . . . . . . . . . . . 18 |- ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( 0 [,] if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( 0 [,] if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) )
251	42	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> -u pi e. RR )
252	41	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> pi e. RR )
253	42, 47	ltlei 9718	. . . . . . . . . . . . . . . . . . . 20 |- ( -u pi < 0 -> -u pi <_ 0 )
254	45, 253	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- -u pi <_ 0
255	254	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> -u pi <_ 0 )
256		elioore 11571	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( 0 (,) pi ) -> s e. RR )
257	256	ssriv 3513	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) pi ) C_ RR
258	257, 243	sseldi 3507	. . . . . . . . . . . . . . . . . . 19 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. RR )
259		min2 11402	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c e. RR /\ ( pi / 2 ) e. RR ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ ( pi / 2 ) )
260	216, 221, 259	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ ( pi / 2 ) )
261	227	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. RR+ -> ( pi / 2 ) < pi )
262	258, 221, 252, 260, 261	lelttrd 9751	. . . . . . . . . . . . . . . . . . 19 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) < pi )
263	258, 252, 262	ltled 9744	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ pi )
264		iccss 11604	. . . . . . . . . . . . . . . . . 18 |- ( ( ( -u pi e. RR /\ pi e. RR ) /\ ( -u pi <_ 0 /\ if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ pi ) ) -> ( 0 [,] if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) )
265	251, 252, 255, 263, 264	syl22anc 1229	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> ( 0 [,] if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) )
266	250, 265	sstrd 3519	. . . . . . . . . . . . . . . 16 |- ( c e. RR+ -> ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) )
267	47	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( c e. RR+ -> 0 e. RR )
268	219, 211	breqtrrd 4479	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c e. RR+ /\ c <_ ( pi / 2 ) ) -> 0 < if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
269	236, 232	syl5breqr 4489	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -. c <_ ( pi / 2 ) -> 0 < if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
270	269	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c e. RR+ /\ -. c <_ ( pi / 2 ) ) -> 0 < if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
271	268, 270	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. RR+ -> 0 < if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
272	267, 258, 271	ltled 9744	. . . . . . . . . . . . . . . . . . 19 |- ( c e. RR+ -> 0 <_ if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
273		volioo 31589	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 e. RR /\ if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. RR /\ 0 <_ if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) = ( if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) - 0 ) )
274	267, 258, 272, 273	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) = ( if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) - 0 ) )
275	84, 258	sseldi 3507	. . . . . . . . . . . . . . . . . . 19 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. CC )
276	275	subid1d 9931	. . . . . . . . . . . . . . . . . 18 |- ( c e. RR+ -> ( if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) - 0 ) = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
277	274, 276	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) )
278		min1 11401	. . . . . . . . . . . . . . . . . 18 |- ( ( c e. RR /\ ( pi / 2 ) e. RR ) -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ c )
279	216, 221, 278	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( c e. RR+ -> if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) <_ c )
280	277, 279	eqbrtrd 4473	. . . . . . . . . . . . . . . 16 |- ( c e. RR+ -> ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c )
281	266, 280	jca 532	. . . . . . . . . . . . . . 15 |- ( c e. RR+ -> ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) /\ ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) )
282	281	adantr 465	. . . . . . . . . . . . . 14 |- ( ( c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) /\ ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) )
283		sseq1 3530	. . . . . . . . . . . . . . . . 17 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( u C_ ( -u pi [,] pi ) <-> ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) ) )
284		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( vol ` u ) = ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) )
285	284	breq1d 4463	. . . . . . . . . . . . . . . . 17 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( ( vol ` u ) <_ c <-> ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) )
286	283, 285	anbi12d 710	. . . . . . . . . . . . . . . 16 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) <-> ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) /\ ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) ) )
287		itgeq1 22047	. . . . . . . . . . . . . . . . . . 19 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s = S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s )
288	287	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) = ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) )
289	288	breq1d 4463	. . . . . . . . . . . . . . . . 17 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
290	289	ralbidv 2906	. . . . . . . . . . . . . . . 16 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
291	286, 290	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( u = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) -> ( ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) <-> ( ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) /\ ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) -> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
292	291	rspcva 3217	. . . . . . . . . . . . . 14 |- ( ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) e. dom vol /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> ( ( ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) C_ ( -u pi [,] pi ) /\ ( vol ` ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ) <_ c ) -> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
293	248, 282, 292	sylc 60	. . . . . . . . . . . . 13 |- ( ( c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
294	293	3adant1 1014	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
295		oveq2 6303	. . . . . . . . . . . . . . . . 17 |- ( d = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) -> ( 0 (,) d ) = ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) )
296	295	itgeq1d 31597	. . . . . . . . . . . . . . . 16 |- ( d = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) -> S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s = S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s )
297	296	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( d = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) -> ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) = ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) )
298	297	breq1d 4463	. . . . . . . . . . . . . 14 |- ( d = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) -> ( ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
299	298	ralbidv 2906	. . . . . . . . . . . . 13 |- ( d = if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) -> ( A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) <-> A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
300	299	rspcev 3219	. . . . . . . . . . . 12 |- ( ( if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) e. ( 0 (,) pi ) /\ A. k e. NN ( abs ` S. ( 0 (,) if ( c <_ ( pi / 2 ) , c , ( pi / 2 ) ) ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) -> E. d e. ( 0 (,) pi ) A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
301	244, 294, 300	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ e e. RR+ ) /\ c e. RR+ /\ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) -> E. d e. ( 0 (,) pi ) A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
302	301	3exp 1195	. . . . . . . . . 10 |- ( ( ph /\ e e. RR+ ) -> ( c e. RR+ -> ( A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) -> E. d e. ( 0 (,) pi ) A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) ) )
303	302	rexlimdv 2957	. . . . . . . . 9 |- ( ( ph /\ e e. RR+ ) -> ( E. c e. RR+ A. u e. dom vol ( ( u C_ ( -u pi [,] pi ) /\ ( vol ` u ) <_ c ) -> A. k e. NN ( abs ` S. u ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) -> E. d e. ( 0 (,) pi ) A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) ) )
304	209, 303	mpd 15	. . . . . . . 8 |- ( ( ph /\ e e. RR+ ) -> E. d e. ( 0 (,) pi ) A. k e. NN ( abs ` S. ( 0 (,) d ) ( ( U ` s ) x. ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( e / 2 ) )
305	257	sseli 3505	. . . . . . . . . . . . . . . . . . 19 |- ( d e. ( 0 (,) pi ) -> d e. RR )
306	305	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d e. RR )
307	41	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi e. RR )
308	11, 12, 24, 35, 36, 37, 38	fourierdlem55 31785	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> U : ( -u pi [,] pi ) --> RR )
309	84	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> RR C_ CC )
310	308, 309	fssd 5746	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> U : ( -u pi [,] pi ) --> CC )
311	310	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> U : ( -u pi [,] pi ) --> CC )
312	42	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> -u pi e. RR )
313	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d e. ( 0 (,) pi ) -> -u pi e. RR )
314	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. ( 0 (,) pi ) -> 0 e. RR )
315	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. ( 0 (,) pi ) -> -u pi < 0 )
316		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 e. RR* /\ pi e. RR* /\ d e. ( 0 (,) pi ) ) -> 0 < d )
317	212, 214, 316	mp3an12 1314	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. ( 0 (,) pi ) -> 0 < d )
318	313, 314, 305, 315, 317	lttrd 9754	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d e. ( 0 (,) pi ) -> -u pi < d )
319	313, 305, 318	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d e. ( 0 (,) pi ) -> -u pi <_ d )
320	319	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> -u pi <_ d )
321	307	leidd 10131	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi <_ pi )
322		iccss 11604	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( -u pi e. RR /\ pi e. RR ) /\ ( -u pi <_ d /\ pi <_ pi ) ) -> ( d [,] pi ) C_ ( -u pi [,] pi ) )
323	312, 307, 320, 321, 322	syl22anc 1229	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d [,] pi ) C_ ( -u pi [,] pi ) )
324	311, 323	fssresd 5758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( U |` ( d [,] pi ) ) : ( d [,] pi ) --> CC )
325		fourierdlem104.o	. . . . . . . . . . . . . . . . . . . . 21 |- O = ( U |` ( d [,] pi ) )
326	325	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> O = ( U |` ( d [,] pi ) ) )
327	326	feq1d 5723	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( O : ( d [,] pi ) --> CC <-> ( U |` ( d [,] pi ) ) : ( d [,] pi ) --> CC ) )
328	324, 327	mpbird 232	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> O : ( d [,] pi ) --> CC )
329		fourierdlem104.n	. . . . . . . . . . . . . . . . . . . . . 22 |- N = ( ( # ` T ) - 1 )
330	41	elexi 3128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- pi e. _V
331	330	prid2 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- pi e. { d , pi }
332		elun1 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( pi e. { d , pi } -> pi e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) )
333	331, 332	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- pi e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
334		fourierdlem104.t	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- T = ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
335	334	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) = T
336	333, 335	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- pi e. T
337		ne0i 3796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( pi e. T -> T =/= (/) )
338	336, 337	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- T =/= (/)
339	338	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> T =/= (/) )
340		prfi 7807	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { d , pi } e. Fin
341	340	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> { d , pi } e. Fin )
342		fzfi 12062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 0 ... M ) e. Fin
343	66	rnmptfi 31348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 0 ... M ) e. Fin -> ran Q e. Fin )
344	342, 343	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ran Q e. Fin
345	344	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ran Q e. Fin )
346		infi 7755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ran Q e. Fin -> ( ran Q i^i ( d (,) pi ) ) e. Fin )
347	345, 346	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( ran Q i^i ( d (,) pi ) ) e. Fin )
348		unfi 7799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( { d , pi } e. Fin /\ ( ran Q i^i ( d (,) pi ) ) e. Fin ) -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) e. Fin )
349	341, 347, 348	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) e. Fin )
350	334, 349	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> T e. Fin )
351		hashnncl 12416	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( T e. Fin -> ( ( # ` T ) e. NN <-> T =/= (/) ) )
352	350, 351	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( # ` T ) e. NN <-> T =/= (/) ) )
353	339, 352	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( # ` T ) e. NN )
354		nnm1nn0 10849	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( # ` T ) e. NN -> ( ( # ` T ) - 1 ) e. NN0 )
355	353, 354	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( # ` T ) - 1 ) e. NN0 )
356	329, 355	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. NN0 )
357	356	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. NN0 )
358	47	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 e. RR )
359		1re 9607	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. RR
360	359	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 e. RR )
361	357	nn0red 10865	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. RR )
362		0lt1 10087	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 < 1
363	362	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 < 1 )
364		2m1e1 10662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( 2 - 1 ) = 1
365	364	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 = ( 2 - 1 )
366	365	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 = ( 2 - 1 ) )
367	234	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 e. RR )
368	353	nnred 10563	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( # ` T ) e. RR )
369	368	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` T ) e. RR )
370		iooltub 31435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 0 e. RR* /\ pi e. RR* /\ d e. ( 0 (,) pi ) ) -> d < pi )
371	212, 214, 370	mp3an12 1314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( d e. ( 0 (,) pi ) -> d < pi )
372	305, 371	ltned 9732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( d e. ( 0 (,) pi ) -> d =/= pi )
373	372	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d =/= pi )
374		hashprg 12440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( d e. RR /\ pi e. RR ) -> ( d =/= pi <-> ( # ` { d , pi } ) = 2 ) )
375	306, 307, 374	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d =/= pi <-> ( # ` { d , pi } ) = 2 ) )
376	373, 375	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` { d , pi } ) = 2 )
377	376	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 = ( # ` { d , pi } ) )
378	350	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> T e. Fin )
379		ssun1 3672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { d , pi } C_ ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
380	379, 335	sseqtri 3541	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- { d , pi } C_ T
381	380	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> { d , pi } C_ T )
382		hashssle 31397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( T e. Fin /\ { d , pi } C_ T ) -> ( # ` { d , pi } ) <_ ( # ` T ) )
383	378, 381, 382	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` { d , pi } ) <_ ( # ` T ) )
384	377, 383	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 <_ ( # ` T ) )
385	367, 369, 360, 384	lesub1dd 10180	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( 2 - 1 ) <_ ( ( # ` T ) - 1 ) )
386	366, 385	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 <_ ( ( # ` T ) - 1 ) )
387	329	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( # ` T ) - 1 ) = N
388	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ( # ` T ) - 1 ) = N )
389	386, 388	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 <_ N )
390	358, 360, 361, 363, 389	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 < N )
391	358, 390	gtned 9731	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N =/= 0 )
392	357, 391	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( N e. NN0 /\ N =/= 0 ) )
393		elnnne0 10821	. . . . . . . . . . . . . . . . . . 19 |- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
394	392, 393	sylibr 212	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. NN )
395		fourierdlem104.j	. . . . . . . . . . . . . . . . . . . . 21 |- J = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
396	306	leidd 10131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d <_ d )
397	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( d e. ( 0 (,) pi ) -> pi e. RR )
398	305, 397, 371	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( d e. ( 0 (,) pi ) -> d <_ pi )
399	398	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d <_ pi )
400	306, 307, 306, 396, 399	eliccd 31425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d e. ( d [,] pi ) )
401	306, 307, 307, 399, 321	eliccd 31425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi e. ( d [,] pi ) )
402	400, 401	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d e. ( d [,] pi ) /\ pi e. ( d [,] pi ) ) )
403		vex 3121	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- d e. _V
404	403, 330	prss 4187	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( d e. ( d [,] pi ) /\ pi e. ( d [,] pi ) ) <-> { d , pi } C_ ( d [,] pi ) )
405	402, 404	sylib 196	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> { d , pi } C_ ( d [,] pi ) )
406		inss2 3724	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ran Q i^i ( d (,) pi ) ) C_ ( d (,) pi )
407	406	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ran Q i^i ( d (,) pi ) ) C_ ( d (,) pi ) )
408		ioossicc 11622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( d (,) pi ) C_ ( d [,] pi )
409	408	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d (,) pi ) C_ ( d [,] pi ) )
410	407, 409	sstrd 3519	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ran Q i^i ( d (,) pi ) ) C_ ( d [,] pi ) )
411	405, 410	unssd 3685	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) C_ ( d [,] pi ) )
412	334, 411	syl5eqss 3553	. . . . . . . . . . . . . . .