Theorem fourierdlem104 38186

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 2471	. . 3 |- ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
2		1zzd 10992	. . 3 |- ( ph -> 1 e. ZZ )
3		nfv 1769	. . . . 5 |- F/ n ph
4		nfmpt1 4485	. . . . 5 |- F/_ n ( n e. NN |-> S. ( 0 (,) pi ) ( G ` s ) _d s )
5		nfmpt1 4485	. . . . 5 |- F/_ n ( n e. NN |-> pi )
6		fourierdlem104.e	. . . . . 6 |- E = ( n e. NN |-> ( S. ( 0 (,) pi ) ( G ` s ) _d s / pi ) )
7		nfmpt1 4485	. . . . . 6 |- F/_ n ( n e. NN |-> ( S. ( 0 (,) pi ) ( G ` s ) _d s / pi ) )
8	6, 7	nfcxfr 2610	. . . . 5 |- F/_ n E
9		nnuz 11218	. . . . 5 |- NN = ( ZZ>= ` 1 )
10		elioore 11691	. . . . . . . . . . . . . . . 16 |- ( d e. ( 0 (,) pi ) -> d e. RR )
11	10	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d e. RR )
12		pire 23492	. . . . . . . . . . . . . . . 16 |- pi e. RR
13	12	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi e. RR )
14		fourierdlem104.f	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> F : RR --> RR )
15		fourierdlem104.xre	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> X e. RR )
16		ioossre 11721	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( X (,) +oo ) C_ RR
17	16	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( X (,) +oo ) C_ RR )
18	14, 17	fssresd 5762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( F |` ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
19		ioosscn 37687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( X (,) +oo ) C_ CC
20	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( X (,) +oo ) C_ CC )
21		eqid 2471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
22		pnfxr 11435	. . . . . . . . . . . . . . . . . . . . . . 23 |- +oo e. RR*
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> +oo e. RR* )
24	15	ltpnfd 11446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> X < +oo )
25	21, 23, 15, 24	lptioo1cn 37824	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( X (,) +oo ) ) )
26		fourierdlem104.y	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) lim CC X ) )
27	18, 20, 25, 26	limcrecl 37806	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> Y e. RR )
28		ioossre 11721	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -oo (,) X ) C_ RR
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( -oo (,) X ) C_ RR )
30	14, 29	fssresd 5762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( F |` ( -oo (,) X ) ) : ( -oo (,) X ) --> RR )
31		ioosscn 37687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( -oo (,) X ) C_ CC
32	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( -oo (,) X ) C_ CC )
33		mnfxr 11437	. . . . . . . . . . . . . . . . . . . . . . 23 |- -oo e. RR*
34	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -oo e. RR* )
35	15	mnfltd 11449	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -oo < X )
36	21, 34, 15, 35	lptioo2cn 37823	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` ( -oo (,) X ) ) )
37		fourierdlem104.w	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> W e. ( ( F |` ( -oo (,) X ) ) lim CC X ) )
38	30, 32, 36, 37	limcrecl 37806	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> W e. RR )
39		fourierdlem104.h	. . . . . . . . . . . . . . . . . . . 20 |- H = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
40		fourierdlem104.k	. . . . . . . . . . . . . . . . . . . 20 |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
41		fourierdlem104.u	. . . . . . . . . . . . . . . . . . . 20 |- U = ( s e. ( -u pi [,] pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
42	14, 15, 27, 38, 39, 40, 41	fourierdlem55 38137	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> U : ( -u pi [,] pi ) --> RR )
43		ax-resscn 9614	. . . . . . . . . . . . . . . . . . . 20 |- RR C_ CC
44	43	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> RR C_ CC )
45	42, 44	fssd 5750	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U : ( -u pi [,] pi ) --> CC )
46	45	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> U : ( -u pi [,] pi ) --> CC )
47	12	renegcli 9955	. . . . . . . . . . . . . . . . . . 19 |- -u pi e. RR
48	47	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> -u pi e. RR )
49	47	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( d e. ( 0 (,) pi ) -> -u pi e. RR )
50		0red 9662	. . . . . . . . . . . . . . . . . . . . 21 |- ( d e. ( 0 (,) pi ) -> 0 e. RR )
51		negpilt0 37580	. . . . . . . . . . . . . . . . . . . . . 22 |- -u pi < 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( d e. ( 0 (,) pi ) -> -u pi < 0 )
53		0xr 9705	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR*
54	12	rexri 9711	. . . . . . . . . . . . . . . . . . . . . 22 |- pi e. RR*
55		ioogtlb 37688	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 0 e. RR* /\ pi e. RR* /\ d e. ( 0 (,) pi ) ) -> 0 < d )
56	53, 54, 55	mp3an12 1380	. . . . . . . . . . . . . . . . . . . . 21 |- ( d e. ( 0 (,) pi ) -> 0 < d )
57	49, 50, 10, 52, 56	lttrd 9813	. . . . . . . . . . . . . . . . . . . 20 |- ( d e. ( 0 (,) pi ) -> -u pi < d )
58	49, 10, 57	ltled 9800	. . . . . . . . . . . . . . . . . . 19 |- ( d e. ( 0 (,) pi ) -> -u pi <_ d )
59	58	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> -u pi <_ d )
60	13	leidd 10201	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi <_ pi )
61		iccss 11727	. . . . . . . . . . . . . . . . . 18 |- ( ( ( -u pi e. RR /\ pi e. RR ) /\ ( -u pi <_ d /\ pi <_ pi ) ) -> ( d [,] pi ) C_ ( -u pi [,] pi ) )
62	48, 13, 59, 60, 61	syl22anc 1293	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d [,] pi ) C_ ( -u pi [,] pi ) )
63	46, 62	fssresd 5762	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( U |` ( d [,] pi ) ) : ( d [,] pi ) --> CC )
64		fourierdlem104.o	. . . . . . . . . . . . . . . . . 18 |- O = ( U |` ( d [,] pi ) )
65	64	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> O = ( U |` ( d [,] pi ) ) )
66	65	feq1d 5724	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( O : ( d [,] pi ) --> CC <-> ( U |` ( d [,] pi ) ) : ( d [,] pi ) --> CC ) )
67	63, 66	mpbird 240	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> O : ( d [,] pi ) --> CC )
68		fourierdlem104.n	. . . . . . . . . . . . . . . . . 18 |- N = ( ( # ` T ) - 1 )
69	12	elexi 3041	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- pi e. _V
70	69	prid2 4072	. . . . . . . . . . . . . . . . . . . . . . . 24 |- pi e. { d , pi }
71		elun1 3592	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( pi e. { d , pi } -> pi e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) )
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 |- pi e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
73		fourierdlem104.t	. . . . . . . . . . . . . . . . . . . . . . 23 |- T = ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
74	72, 73	eleqtrri 2548	. . . . . . . . . . . . . . . . . . . . . 22 |- pi e. T
75	74	ne0ii 3729	. . . . . . . . . . . . . . . . . . . . 21 |- T =/= (/)
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> T =/= (/) )
77		prfi 7864	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { d , pi } e. Fin
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> { d , pi } e. Fin )
79		fzfi 12223	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 ... M ) e. Fin
80		fourierdlem104.q	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
81	80	rnmptfi 37508	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 0 ... M ) e. Fin -> ran Q e. Fin )
82	79, 81	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ran Q e. Fin
83		infi 7813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ran Q e. Fin -> ( ran Q i^i ( d (,) pi ) ) e. Fin )
84	82, 83	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ran Q i^i ( d (,) pi ) ) e. Fin )
85		unfi 7856	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( { d , pi } e. Fin /\ ( ran Q i^i ( d (,) pi ) ) e. Fin ) -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) e. Fin )
86	78, 84, 85	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) e. Fin )
87	73, 86	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T e. Fin )
88		hashnncl 12585	. . . . . . . . . . . . . . . . . . . . 21 |- ( T e. Fin -> ( ( # ` T ) e. NN <-> T =/= (/) ) )
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( # ` T ) e. NN <-> T =/= (/) ) )
90	76, 89	mpbird 240	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( # ` T ) e. NN )
91		nnm1nn0 10935	. . . . . . . . . . . . . . . . . . 19 |- ( ( # ` T ) e. NN -> ( ( # ` T ) - 1 ) e. NN0 )
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( # ` T ) - 1 ) e. NN0 )
93	68, 92	syl5eqel 2553	. . . . . . . . . . . . . . . . 17 |- ( ph -> N e. NN0 )
94	93	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. NN0 )
95		0red 9662	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 e. RR )
96		1red 9676	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 e. RR )
97	94	nn0red 10950	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. RR )
98		0lt1 10157	. . . . . . . . . . . . . . . . . . 19 |- 0 < 1
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 < 1 )
100		2re 10701	. . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 e. RR )
102	90	nnred 10646	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( # ` T ) e. RR )
103	102	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` T ) e. RR )
104		iooltub 37706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 0 e. RR* /\ pi e. RR* /\ d e. ( 0 (,) pi ) ) -> d < pi )
105	53, 54, 104	mp3an12 1380	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( d e. ( 0 (,) pi ) -> d < pi )
106	10, 105	ltned 9788	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. ( 0 (,) pi ) -> d =/= pi )
107	106	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d =/= pi )
108		hashprg 12610	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( d e. RR /\ pi e. RR ) -> ( d =/= pi <-> ( # ` { d , pi } ) = 2 ) )
109	11, 12, 108	sylancl 675	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d =/= pi <-> ( # ` { d , pi } ) = 2 ) )
110	107, 109	mpbid 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` { d , pi } ) = 2 )
111	110	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 = ( # ` { d , pi } ) )
112	87	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> T e. Fin )
113		ssun1 3588	. . . . . . . . . . . . . . . . . . . . . . 23 |- { d , pi } C_ ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
114	113, 73	sseqtr4i 3451	. . . . . . . . . . . . . . . . . . . . . 22 |- { d , pi } C_ T
115		hashssle 37603	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T e. Fin /\ { d , pi } C_ T ) -> ( # ` { d , pi } ) <_ ( # ` T ) )
116	112, 114, 115	sylancl 675	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( # ` { d , pi } ) <_ ( # ` T ) )
117	111, 116	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 2 <_ ( # ` T ) )
118	101, 103, 96, 117	lesub1dd 10250	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( 2 - 1 ) <_ ( ( # ` T ) - 1 ) )
119		1e2m1 10747	. . . . . . . . . . . . . . . . . . 19 |- 1 = ( 2 - 1 )
120	118, 119, 68	3brtr4g 4428	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 1 <_ N )
121	95, 96, 97, 99, 120	ltletrd 9812	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> 0 < N )
122	121	gt0ne0d 10199	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N =/= 0 )
123		elnnne0 10907	. . . . . . . . . . . . . . . 16 |- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
124	94, 122, 123	sylanbrc 677	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> N e. NN )
125		fourierdlem104.j	. . . . . . . . . . . . . . . . 17 |- J = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
126	11	leidd 10201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d <_ d )
127	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( d e. ( 0 (,) pi ) -> pi e. RR )
128	10, 127, 105	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d e. ( 0 (,) pi ) -> d <_ pi )
129	128	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d <_ pi )
130	11, 13, 11, 126, 129	eliccd 37697	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d e. ( d [,] pi ) )
131	11, 13, 13, 129, 60	eliccd 37697	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi e. ( d [,] pi ) )
132	130, 131	jca 541	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d e. ( d [,] pi ) /\ pi e. ( d [,] pi ) ) )
133		vex 3034	. . . . . . . . . . . . . . . . . . . . 21 |- d e. _V
134	133, 69	prss 4117	. . . . . . . . . . . . . . . . . . . 20 |- ( ( d e. ( d [,] pi ) /\ pi e. ( d [,] pi ) ) <-> { d , pi } C_ ( d [,] pi ) )
135	132, 134	sylib 201	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> { d , pi } C_ ( d [,] pi ) )
136		inss2 3644	. . . . . . . . . . . . . . . . . . . . 21 |- ( ran Q i^i ( d (,) pi ) ) C_ ( d (,) pi )
137	136	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ran Q i^i ( d (,) pi ) ) C_ ( d (,) pi ) )
138		ioossicc 11745	. . . . . . . . . . . . . . . . . . . 20 |- ( d (,) pi ) C_ ( d [,] pi )
139	137, 138	syl6ss 3430	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ran Q i^i ( d (,) pi ) ) C_ ( d [,] pi ) )
140	135, 139	unssd 3601	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) C_ ( d [,] pi ) )
141	73, 140	syl5eqss 3462	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> T C_ ( d [,] pi ) )
142	133	prid1 4071	. . . . . . . . . . . . . . . . . . . 20 |- d e. { d , pi }
143		elun1 3592	. . . . . . . . . . . . . . . . . . . 20 |- ( d e. { d , pi } -> d e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) )
144	142, 143	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- d e. ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) )
145	144, 73	eleqtrri 2548	. . . . . . . . . . . . . . . . . 18 |- d e. T
146	145	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d e. T )
147	74	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> pi e. T )
148	112, 68, 125, 11, 13, 141, 146, 147	fourierdlem52 38134	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ( J : ( 0 ... N ) --> ( d [,] pi ) /\ ( J ` 0 ) = d ) /\ ( J ` N ) = pi ) )
149	148	simplld 769	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> J : ( 0 ... N ) --> ( d [,] pi ) )
150	148	simplrd 771	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( J ` 0 ) = d )
151	148	simprd 470	. . . . . . . . . . . . . . 15 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( J ` N ) = pi )
152		elfzoelz 11947	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ( 0..^ N ) -> k e. ZZ )
153	152	zred 11063	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0..^ N ) -> k e. RR )
154	153	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> k e. RR )
155	154	ltp1d 10559	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> k < ( k + 1 ) )
156	10, 127	jca 541	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d e. ( 0 (,) pi ) -> ( d e. RR /\ pi e. RR ) )
157	133, 69	prss 4117	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. RR /\ pi e. RR ) <-> { d , pi } C_ RR )
158	156, 157	sylib 201	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d e. ( 0 (,) pi ) -> { d , pi } C_ RR )
159	158	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> { d , pi } C_ RR )
160		ioossre 11721	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( d (,) pi ) C_ RR
161	136, 160	sstri 3427	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ran Q i^i ( d (,) pi ) ) C_ RR
162	161	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( ran Q i^i ( d (,) pi ) ) C_ RR )
163	159, 162	unssd 3601	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( { d , pi } u. ( ran Q i^i ( d (,) pi ) ) ) C_ RR )
164	73, 163	syl5eqss 3462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> T C_ RR )
165	112, 164, 125, 68	fourierdlem36 38118	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> J Isom < , < ( ( 0 ... N ) , T ) )
166	165	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> J Isom < , < ( ( 0 ... N ) , T ) )
167		elfzofz 11962	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0..^ N ) -> k e. ( 0 ... N ) )
168	167	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> k e. ( 0 ... N ) )
169		fzofzp1 12037	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0..^ N ) -> ( k + 1 ) e. ( 0 ... N ) )
170	169	adantl 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( k + 1 ) e. ( 0 ... N ) )
171		isorel 6235	. . . . . . . . . . . . . . . . 17 |- ( ( J Isom < , < ( ( 0 ... N ) , T ) /\ ( k e. ( 0 ... N ) /\ ( k + 1 ) e. ( 0 ... N ) ) ) -> ( k < ( k + 1 ) <-> ( J ` k ) < ( J ` ( k + 1 ) ) ) )
172	166, 168, 170, 171	syl12anc 1290	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( k < ( k + 1 ) <-> ( J ` k ) < ( J ` ( k + 1 ) ) ) )
173	155, 172	mpbid 215	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` k ) < ( J ` ( k + 1 ) ) )
174	42	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> U : ( -u pi [,] pi ) --> RR )
175	174, 62	feqresmpt 5933	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( U |` ( d [,] pi ) ) = ( s e. ( d [,] pi ) |-> ( U ` s ) ) )
176	62	sselda 3418	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> s e. ( -u pi [,] pi ) )
177	14, 15, 27, 38, 39	fourierdlem9 38090	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> H : ( -u pi [,] pi ) --> RR )
178	177	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> H : ( -u pi [,] pi ) --> RR )
179	178, 176	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( H ` s ) e. RR )
180	40	fourierdlem43 38126	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- K : ( -u pi [,] pi ) --> RR
181	180	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> K : ( -u pi [,] pi ) --> RR )
182	181, 176	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( K ` s ) e. RR )
183	179, 182	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( H ` s ) x. ( K ` s ) ) e. RR )
184	41	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( s e. ( -u pi [,] pi ) /\ ( ( H ` s ) x. ( K ` s ) ) e. RR ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
185	176, 183, 184	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
186		0red 9662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 0 e. RR )
187	10	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> d e. RR )
188	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> pi e. RR )
189		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s e. ( d [,] pi ) )
190		eliccre 37699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. RR /\ pi e. RR /\ s e. ( d [,] pi ) ) -> s e. RR )
191	187, 188, 189, 190	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s e. RR )
192	56	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 0 < d )
193	187	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> d e. RR* )
194	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> pi e. RR* )
195		iccgelb 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( d e. RR* /\ pi e. RR* /\ s e. ( d [,] pi ) ) -> d <_ s )
196	193, 194, 189, 195	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> d <_ s )
197	186, 187, 191, 192, 196	ltletrd 9812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 0 < s )
198	197	gt0ne0d 10199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s =/= 0 )
199	198	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> s =/= 0 )
200	199	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> -. s = 0 )
201	200	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) )
202	197	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> 0 < s )
203	202	iftrued 3880	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> if ( 0 < s , Y , W ) = Y )
204	203	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) = ( ( F ` ( X + s ) ) - Y ) )
205	204	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
206	201, 205	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
207	14	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> F : RR --> RR )
208	15	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> X e. RR )
209		iccssre 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( -u pi [,] pi ) C_ RR )
210	47, 12, 209	mp2an 686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( -u pi [,] pi ) C_ RR
211	210, 176	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> s e. RR )
212	208, 211	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( X + s ) e. RR )
213	207, 212	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( F ` ( X + s ) ) e. RR )
214	27	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> Y e. RR )
215	213, 214	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( F ` ( X + s ) ) - Y ) e. RR )
216	215, 211, 199	redivcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( ( F ` ( X + s ) ) - Y ) / s ) e. RR )
217	206, 216	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. RR )
218	39	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s e. ( -u pi [,] pi ) /\ if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) e. RR ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
219	176, 217, 218	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( H ` s ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
220	219, 201, 205	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( H ` s ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
221	188	renegcld 10067	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> -u pi e. RR )
222	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> -u pi < 0 )
223	221, 186, 191, 222, 197	lttrd 9813	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> -u pi < s )
224	221, 191, 223	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> -u pi <_ s )
225		iccleub 11715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d e. RR* /\ pi e. RR* /\ s e. ( d [,] pi ) ) -> s <_ pi )
226	193, 194, 189, 225	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s <_ pi )
227	221, 188, 191, 224, 226	eliccd 37697	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s e. ( -u pi [,] pi ) )
228	198	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> -. s = 0 )
229	228	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
230	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 2 e. RR )
231	191	rehalfcld 10882	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( s / 2 ) e. RR )
232	231	resincld 14274	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( sin ` ( s / 2 ) ) e. RR )
233	230, 232	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
234		2cnd 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 2 e. CC )
235	191	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> s e. CC )
236	235	halfcld 10880	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( s / 2 ) e. CC )
237	236	sincld 14261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( sin ` ( s / 2 ) ) e. CC )
238		2ne0 10724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 2 =/= 0
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> 2 =/= 0 )
240		fourierdlem44 38127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( s e. ( -u pi [,] pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
241	227, 198, 240	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
242	234, 237, 239, 241	mulne0d 10286	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
243	191, 233, 242	redivcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
244	229, 243	eqeltrd 2549	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. RR )
245	40	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s e. ( -u pi [,] pi ) /\ if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. RR ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
246	227, 244, 245	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( d e. ( 0 (,) pi ) /\ s e. ( d [,] pi ) ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
247	246	adantll 728	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
248	220, 247	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( H ` s ) x. ( K ` s ) ) = ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
249	200	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
250	249	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
251	185, 248, 250	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( U ` s ) = ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
252	251	mpteq2dva 4482	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( s e. ( d [,] pi ) |-> ( U ` s ) ) = ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
253	65, 175, 252	3eqtrd 2509	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> O = ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
254	253	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> O = ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
255	254	reseq1d 5110	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) = ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) )
256	14	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> F : RR --> RR )
257	15	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> X e. RR )
258		fourierdlem104.p	. . . . . . . . . . . . . . . . . 18 |- 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 ) ) ) } )
259		fourierdlem104.m	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> M e. NN )
260	259	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> M e. NN )
261		fourierdlem104.v	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> V e. ( P ` M ) )
262	261	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> V e. ( P ` M ) )
263		fourierdlem104.fcn	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
264	263	adantlr 729	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
265		fourierdlem104.r	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
266	265	adantlr 729	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
267		fourierdlem104.l	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
268	267	adantlr 729	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
269	105	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> d < pi )
270	50, 10	ltnled 9799	. . . . . . . . . . . . . . . . . . . . . 22 |- ( d e. ( 0 (,) pi ) -> ( 0 < d <-> -. d <_ 0 ) )
271	56, 270	mpbid 215	. . . . . . . . . . . . . . . . . . . . 21 |- ( d e. ( 0 (,) pi ) -> -. d <_ 0 )
272	271	intn3an2d 1408	. . . . . . . . . . . . . . . . . . . 20 |- ( d e. ( 0 (,) pi ) -> -. ( 0 e. RR /\ d <_ 0 /\ 0 <_ pi ) )
273		elicc2 11724	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( d e. RR /\ pi e. RR ) -> ( 0 e. ( d [,] pi ) <-> ( 0 e. RR /\ d <_ 0 /\ 0 <_ pi ) ) )
274	10, 12, 273	sylancl 675	. . . . . . . . . . . . . . . . . . . 20 |- ( d e. ( 0 (,) pi ) -> ( 0 e. ( d [,] pi ) <-> ( 0 e. RR /\ d <_ 0 /\ 0 <_ pi ) ) )
275	272, 274	mtbird 308	. . . . . . . . . . . . . . . . . . 19 |- ( d e. ( 0 (,) pi ) -> -. 0 e. ( d [,] pi ) )
276	275	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> -. 0 e. ( d [,] pi ) )
277	27	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> Y e. RR )
278		eqid 2471	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
279		eqid 2471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( if ( ( J ` ( k + 1 ) ) = ( Q ` ( ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) + 1 ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ L , ( F ` ( X + ( J ` ( k + 1 ) ) ) ) ) - Y ) / ( J ` ( k + 1 ) ) ) x. ( ( J ` ( k + 1 ) ) / ( 2 x. ( sin ` ( ( J ` ( k + 1 ) ) / 2 ) ) ) ) ) = ( ( ( if ( ( J ` ( k + 1 ) ) = ( Q ` ( ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) + 1 ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ L , ( F ` ( X + ( J ` ( k + 1 ) ) ) ) ) - Y ) / ( J ` ( k + 1 ) ) ) x. ( ( J ` ( k + 1 ) ) / ( 2 x. ( sin ` ( ( J ` ( k + 1 ) ) / 2 ) ) ) ) )
280		eqid 2471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( if ( ( J ` k ) = ( Q ` ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ R , ( F ` ( X + ( J ` k ) ) ) ) - Y ) / ( J ` k ) ) x. ( ( J ` k ) / ( 2 x. ( sin ` ( ( J ` k ) / 2 ) ) ) ) ) = ( ( ( if ( ( J ` k ) = ( Q ` ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ R , ( F ` ( X + ( J ` k ) ) ) ) - Y ) / ( J ` k ) ) x. ( ( J ` k ) / ( 2 x. ( sin ` ( ( J ` k ) / 2 ) ) ) ) )
281		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( l = i -> ( Q ` l ) = ( Q ` i ) )
282		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l = i -> ( l + 1 ) = ( i + 1 ) )
283	282	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( l = i -> ( Q ` ( l + 1 ) ) = ( Q ` ( i + 1 ) ) )
284	281, 283	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20 |- ( l = i -> ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
285	284	sseq2d 3446	. . . . . . . . . . . . . . . . . . 19 |- ( l = i -> ( ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) <-> ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
286	285	cbvriotav 6281	. . . . . . . . . . . . . . . . . 18 |- ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) = ( iota_ i e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
287	256, 257, 258, 260, 262, 264, 266, 268, 11, 13, 269, 62, 276, 277, 278, 80, 73, 68, 125, 279, 280, 286	fourierdlem86 38168	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( ( ( if ( ( J ` ( k + 1 ) ) = ( Q ` ( ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) + 1 ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ L , ( F ` ( X + ( J ` ( k + 1 ) ) ) ) ) - Y ) / ( J ` ( k + 1 ) ) ) x. ( ( J ` ( k + 1 ) ) / ( 2 x. ( sin ` ( ( J ` ( k + 1 ) ) / 2 ) ) ) ) ) e. ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` ( k + 1 ) ) ) /\ ( ( ( if ( ( J ` k ) = ( Q ` ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ R , ( F ` ( X + ( J ` k ) ) ) ) - Y ) / ( J ` k ) ) x. ( ( J ` k ) / ( 2 x. ( sin ` ( ( J ` k ) / 2 ) ) ) ) ) e. ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` k ) ) ) /\ ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) e. ( ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) -cn-> CC ) ) )
288	287	simprd 470	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) e. ( ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) -cn-> CC ) )
289	255, 288	eqeltrd 2549	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) e. ( ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) -cn-> CC ) )
290	287	simplld 769	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( if ( ( J ` ( k + 1 ) ) = ( Q ` ( ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) + 1 ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ L , ( F ` ( X + ( J ` ( k + 1 ) ) ) ) ) - Y ) / ( J ` ( k + 1 ) ) ) x. ( ( J ` ( k + 1 ) ) / ( 2 x. ( sin ` ( ( J ` ( k + 1 ) ) / 2 ) ) ) ) ) e. ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` ( k + 1 ) ) ) )
291	254	eqcomd 2477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = O )
292	291	reseq1d 5110	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) = ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) )
293	292	oveq1d 6323	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` ( k + 1 ) ) ) = ( ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` ( k + 1 ) ) ) )
294	290, 293	eleqtrd 2551	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( if ( ( J ` ( k + 1 ) ) = ( Q ` ( ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) + 1 ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ L , ( F ` ( X + ( J ` ( k + 1 ) ) ) ) ) - Y ) / ( J ` ( k + 1 ) ) ) x. ( ( J ` ( k + 1 ) ) / ( 2 x. ( sin ` ( ( J ` ( k + 1 ) ) / 2 ) ) ) ) ) e. ( ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` ( k + 1 ) ) ) )
295	287	simplrd 771	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( if ( ( J ` k ) = ( Q ` ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ R , ( F ` ( X + ( J ` k ) ) ) ) - Y ) / ( J ` k ) ) x. ( ( J ` k ) / ( 2 x. ( sin ` ( ( J ` k ) / 2 ) ) ) ) ) e. ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` k ) ) )
296	292	oveq1d 6323	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( s e. ( d [,] pi ) |-> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` k ) ) = ( ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` k ) ) )
297	295, 296	eleqtrd 2551	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( ( if ( ( J ` k ) = ( Q ` ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) ) , [_ ( iota_ l e. ( 0..^ M ) ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( ( Q ` l ) (,) ( Q ` ( l + 1 ) ) ) ) / i ]_ R , ( F ` ( X + ( J ` k ) ) ) ) - Y ) / ( J ` k ) ) x. ( ( J ` k ) / ( 2 x. ( sin ` ( ( J ` k ) / 2 ) ) ) ) ) e. ( ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) lim CC ( J ` k ) ) )
298		eqid 2471	. . . . . . . . . . . . . . 15 |- ( RR _D O ) = ( RR _D O )
299	67	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> O : ( d [,] pi ) --> CC )
300	11	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> d e. RR )
301	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> pi e. RR )
302		elioore 11691	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) -> s e. RR )
303	302	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s e. RR )
304	62, 210	syl6ss 3430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ d e. ( 0 (,) pi ) ) -> ( d [,] pi ) C_ RR )
305	304	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( d [,] pi ) C_ RR )
306	149	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> J : ( 0 ... N ) --> ( d [,] pi ) )
307	306, 168	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` k ) e. ( d [,] pi ) )
308	305, 307	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` k ) e. RR )
309	308	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` k ) e. RR )
310	11	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> d e. RR )
311	310	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> d e. RR* )
312	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> pi e. RR* )
313		iccgelb 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. RR* /\ pi e. RR* /\ ( J ` k ) e. ( d [,] pi ) ) -> d <_ ( J ` k ) )
314	311, 312, 307, 313	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> d <_ ( J ` k ) )
315	314	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> d <_ ( J ` k ) )
316	309	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` k ) e. RR* )
317	306, 170	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` ( k + 1 ) ) e. ( d [,] pi ) )
318	305, 317	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` ( k + 1 ) ) e. RR )
319	318	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` ( k + 1 ) ) e. RR* )
320	319	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` ( k + 1 ) ) e. RR* )
321		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) )
322		ioogtlb 37688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( J ` k ) e. RR* /\ ( J ` ( k + 1 ) ) e. RR* /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` k ) < s )
323	316, 320, 321, 322	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` k ) < s )
324	300, 309, 303, 315, 323	lelttrd 9810	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> d < s )
325	300, 303, 324	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> d <_ s )
326	318	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` ( k + 1 ) ) e. RR )
327		iooltub 37706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( J ` k ) e. RR* /\ ( J ` ( k + 1 ) ) e. RR* /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s < ( J ` ( k + 1 ) ) )
328	316, 320, 321, 327	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s < ( J ` ( k + 1 ) ) )
329		iccleub 11715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. RR* /\ pi e. RR* /\ ( J ` ( k + 1 ) ) e. ( d [,] pi ) ) -> ( J ` ( k + 1 ) ) <_ pi )
330	311, 312, 317, 329	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( J ` ( k + 1 ) ) <_ pi )
331	330	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( J ` ( k + 1 ) ) <_ pi )
332	303, 326, 301, 328, 331	ltletrd 9812	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s < pi )
333	303, 301, 332	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s <_ pi )
334	300, 301, 303, 325, 333	eliccd 37697	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s e. ( d [,] pi ) )
335	334	ralrimiva 2809	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> A. s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) s e. ( d [,] pi ) )
336		dfss3 3408	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( d [,] pi ) <-> A. s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) s e. ( d [,] pi ) )
337	335, 336	sylibr 217	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) C_ ( d [,] pi ) )
338	299, 337	feqresmpt 5933	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) -> ( O |` ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) = ( s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( O ` s ) ) )
339		simplll 776	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ph )
340		simpllr 777	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> d e. ( 0 (,) pi ) )
341	64	fveq1i 5880	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( O ` s ) = ( ( U |` ( d [,] pi ) ) ` s )
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( O ` s ) = ( ( U |` ( d [,] pi ) ) ` s ) )
343		fvres 5893	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( d [,] pi ) -> ( ( U |` ( d [,] pi ) ) ` s ) = ( U ` s ) )
344	343	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( U |` ( d [,] pi ) ) ` s ) = ( U ` s ) )
345	247, 249	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( K ` s ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
346	220, 345	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( H ` s ) x. ( K ` s ) ) = ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
347	215	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( F ` ( X + s ) ) - Y ) e. CC )
348	235	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> s e. CC )
349		2cnd 10704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> 2 e. CC )
350	348	halfcld 10880	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( s / 2 ) e. CC )
351	350	sincld 14261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( sin ` ( s / 2 ) ) e. CC )
352	349, 351	mulcld 9681	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
353	242	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
354	347, 348, 352, 199, 353	dmdcan2d 10435	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
355	185, 346, 354	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( U ` s ) = ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
356	342, 344, 355	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ s e. ( d [,] pi ) ) -> ( O ` s ) = ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
357	339, 340, 334, 356	syl21anc 1291	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( O ` s ) = ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
358	339, 340, 334, 354	syl21anc 1291	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
359	358	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ d e. ( 0 (,) pi ) ) /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - Y ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( ( F ` ( X + s ) ) - Y ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
360		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( t e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( ( ( F ` ( X + t ) ) - Y ) / t ) ) = ( t e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( ( ( F ` ( X + t ) ) - Y ) / t ) ) )
361		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( t = s -> ( X + t ) = ( X + s ) )
362	361	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( t = s -> ( F ` ( X + t ) ) = ( F ` ( X + s ) ) )
363	362	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t = s -> ( ( F ` ( X + t ) ) - Y ) = ( ( F ` ( X + s ) ) - Y ) )
364		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t = s -> t = s )
365	363, 364	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( t = s -> ( ( ( F ` ( X + t ) ) - Y ) / t ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
366	365	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) /\ t = s ) -> ( ( ( F ` ( X + t ) ) - Y ) / t ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
367		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) )
368		ovex 6336	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( F ` ( X + s ) ) - Y ) / s ) e. _V
369	368	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - Y ) / s ) e. _V )
370	360, 366, 367, 369	fvmptd 5969	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( ( t e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( ( ( F ` ( X + t ) ) - Y ) / t ) ) ` s ) = ( ( ( F ` ( X + s ) ) - Y ) / s ) )
371		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) -> ( t e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( t / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) = ( t e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) |-> ( t / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) )
372		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( t = s -> ( t / 2 ) = ( s / 2 ) )
373	372	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( t = s -> ( sin ` ( t / 2 ) ) = ( sin ` ( s / 2 ) ) )
374	373	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t = s -> ( 2 x. ( sin ` ( t / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
375	364, 374	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( t = s -> ( t / ( 2 x. ( sin ` ( t / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
376	375	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ k e. ( 0..^ N ) ) /\ s e. ( ( J ` k ) (,) ( J ` ( k + 1 ) ) ) ) /\ t = s ) -> ( t / ( 2 x. ( sin ` ( t /