Theorem fourierdlem76 31806

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem76.f	|- ( ph -> F : RR --> RR )
fourierdlem76.xre	|- ( ph -> X e. RR )
fourierdlem76.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 ) ) ) } )
fourierdlem76.m	|- ( ph -> M e. NN )
fourierdlem76.v	|- ( ph -> V e. ( P ` M ) )
fourierdlem76.fcn	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem76.r	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` i ) ) )
fourierdlem76.l	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
fourierdlem76.a	|- ( ph -> A e. RR )
fourierdlem76.b	|- ( ph -> B e. RR )
fourierdlem76.altb	|- ( ph -> A < B )
fourierdlem76.ab	|- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )
fourierdlem76.n0	|- ( ph -> -. 0 e. ( A [,] B ) )
fourierdlem76.c	|- ( ph -> C e. RR )
fourierdlem76.o	|- O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem76.q	|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem76.t	|- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
fourierdlem76.n	|- N = ( ( # ` T ) - 1 )
fourierdlem76.s	|- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem76.d	|- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )
fourierdlem76.e	|- E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
fourierdlem76.ch	|- ( ch <-> ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )

Assertion

Ref

Expression

fourierdlem76

|- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )

Distinct variable groups:   A, s   B, s   C, s   F, s   L, s   i, M, j   m, M, p, i   f, N   Q, s   R, s   S, f   S, s   T, f   i, V, j, s   V, p   i, X, j, s   m, X, p   ch, s   ph, f   ph, i, j, s

Allowed substitution hints:   ph( m, p)   ch( f, i, j, m, p)   A( f, i, j, m, p)   B( f, i, j, m, p)   C( f, i, j, m, p)   D( f, i, j, m, s, p)   P( f, i, j, m, s, p)   Q( f, i, j, m, p)   R( f, i, j, m, p)   S( i, j, m, p)   T( i, j, m, s, p)   E( f, i, j, m, s, p)   F( f, i, j, m, p)   L( f, i, j, m, p)   M( f, s)   N( i, j, m, s, p)   O( f, i, j, m, s, p)   V( f, m)   X( f)

Proof of Theorem fourierdlem76

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem76.ch	. . . 4 |- ( ch <-> ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
2	1	biimpri 206	. . 3 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ch )
3		eqid 2467	. . . . 5 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
4		eqid 2467	. . . . 5 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
5		eqid 2467	. . . . 5 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
6	1	biimpi 194	. . . . . . . . . . 11 |- ( ch -> ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
7		simplll 757	. . . . . . . . . . 11 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
8	6, 7	syl 16	. . . . . . . . . 10 |- ( ch -> ph )
9	8	adantr 465	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ph )
10		ioossicc 11622	. . . . . . . . . . 11 |- ( A (,) B ) C_ ( A [,] B )
11	10	a1i 11	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( A (,) B ) C_ ( A [,] B ) )
12		fourierdlem76.a	. . . . . . . . . . . . . 14 |- ( ph -> A e. RR )
13	12	rexrd 9655	. . . . . . . . . . . . 13 |- ( ph -> A e. RR* )
14	8, 13	syl 16	. . . . . . . . . . . 12 |- ( ch -> A e. RR* )
15	14	adantr 465	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A e. RR* )
16		fourierdlem76.b	. . . . . . . . . . . . . 14 |- ( ph -> B e. RR )
17	16	rexrd 9655	. . . . . . . . . . . . 13 |- ( ph -> B e. RR* )
18	8, 17	syl 16	. . . . . . . . . . . 12 |- ( ch -> B e. RR* )
19	18	adantr 465	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> B e. RR* )
20		ioossre 11598	. . . . . . . . . . . . 13 |- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR
21	20	sseli 3505	. . . . . . . . . . . 12 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> s e. RR )
22	21	adantl 466	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. RR )
23	8, 12	syl 16	. . . . . . . . . . . . 13 |- ( ch -> A e. RR )
24	23	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A e. RR )
25		fourierdlem76.t	. . . . . . . . . . . . . . . . . . 19 |- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
26		prfi 7807	. . . . . . . . . . . . . . . . . . . . 21 |- { A , B } e. Fin
27	26	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { A , B } e. Fin )
28		fzfid 12063	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( 0 ... M ) e. Fin )
29		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . . 23 |- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
30	29	rnmptfi 31348	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 0 ... M ) e. Fin -> ran Q e. Fin )
31	28, 30	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ran Q e. Fin )
32		infi 7755	. . . . . . . . . . . . . . . . . . . . 21 |- ( ran Q e. Fin -> ( ran Q i^i ( A (,) B ) ) e. Fin )
33	31, 32	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ran Q i^i ( A (,) B ) ) e. Fin )
34		unfi 7799	. . . . . . . . . . . . . . . . . . . 20 |- ( ( { A , B } e. Fin /\ ( ran Q i^i ( A (,) B ) ) e. Fin ) -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
35	27, 33, 34	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
36	25, 35	syl5eqel 2559	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T e. Fin )
37	12, 16	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( A e. RR /\ B e. RR ) )
38		prssg 4188	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. RR /\ B e. RR ) -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
39	12, 16, 38	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
40	37, 39	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { A , B } C_ RR )
41		inss2 3724	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ran Q i^i ( A (,) B ) ) C_ ( A (,) B )
42		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A (,) B ) C_ RR
43	41, 42	sstri 3518	. . . . . . . . . . . . . . . . . . . . 21 |- ( ran Q i^i ( A (,) B ) ) C_ RR
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ran Q i^i ( A (,) B ) ) C_ RR )
45	40, 44	unssd 3685	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ RR )
46	25, 45	syl5eqss 3553	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T C_ RR )
47		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 |- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
48		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 |- N = ( ( # ` T ) - 1 )
49	36, 46, 47, 48	fourierdlem36 31766	. . . . . . . . . . . . . . . . 17 |- ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
50	8, 49	syl 16	. . . . . . . . . . . . . . . 16 |- ( ch -> S Isom < , < ( ( 0 ... N ) , T ) )
51		isof1o 6220	. . . . . . . . . . . . . . . 16 |- ( S Isom < , < ( ( 0 ... N ) , T ) -> S : ( 0 ... N ) -1-1-onto-> T )
52		f1of 5822	. . . . . . . . . . . . . . . 16 |- ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) --> T )
53	50, 51, 52	3syl 20	. . . . . . . . . . . . . . 15 |- ( ch -> S : ( 0 ... N ) --> T )
54	8, 46	syl 16	. . . . . . . . . . . . . . 15 |- ( ch -> T C_ RR )
55	53, 54	fssd 5746	. . . . . . . . . . . . . 14 |- ( ch -> S : ( 0 ... N ) --> RR )
56	55	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> S : ( 0 ... N ) --> RR )
57		simpllr 758	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> j e. ( 0..^ N ) )
58	6, 57	syl 16	. . . . . . . . . . . . . . 15 |- ( ch -> j e. ( 0..^ N ) )
59		elfzofz 11823	. . . . . . . . . . . . . . 15 |- ( j e. ( 0..^ N ) -> j e. ( 0 ... N ) )
60	58, 59	syl 16	. . . . . . . . . . . . . 14 |- ( ch -> j e. ( 0 ... N ) )
61	60	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> j e. ( 0 ... N ) )
62	56, 61	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) e. RR )
63	49, 51, 52	3syl 20	. . . . . . . . . . . . . . . . . 18 |- ( ph -> S : ( 0 ... N ) --> T )
64		frn 5743	. . . . . . . . . . . . . . . . . 18 |- ( S : ( 0 ... N ) --> T -> ran S C_ T )
65	63, 64	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ran S C_ T )
66		leid 9692	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. RR -> A <_ A )
67	12, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> A <_ A )
68		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A < B )
69	12, 16, 68	ltled 9744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> A <_ B )
70	12, 16, 12, 67, 69	eliccd 31425	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A e. ( A [,] B ) )
71	16	leidd 10131	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B <_ B )
72	12, 16, 16, 69, 71	eliccd 31425	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. ( A [,] B ) )
73	70, 72	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) )
74		prssg 4188	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR /\ B e. RR ) -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
75	12, 16, 74	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
76	73, 75	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> { A , B } C_ ( A [,] B ) )
77	41, 10	sstri 3518	. . . . . . . . . . . . . . . . . . . 20 |- ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B )
78	77	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B ) )
79	76, 78	unssd 3685	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ ( A [,] B ) )
80	25, 79	syl5eqss 3553	. . . . . . . . . . . . . . . . 17 |- ( ph -> T C_ ( A [,] B ) )
81	65, 80	sstrd 3519	. . . . . . . . . . . . . . . 16 |- ( ph -> ran S C_ ( A [,] B ) )
82	8, 81	syl 16	. . . . . . . . . . . . . . 15 |- ( ch -> ran S C_ ( A [,] B ) )
83		ffun 5739	. . . . . . . . . . . . . . . . 17 |- ( S : ( 0 ... N ) --> RR -> Fun S )
84	55, 83	syl 16	. . . . . . . . . . . . . . . 16 |- ( ch -> Fun S )
85		fdm 5741	. . . . . . . . . . . . . . . . . . 19 |- ( S : ( 0 ... N ) --> RR -> dom S = ( 0 ... N ) )
86	55, 85	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ch -> dom S = ( 0 ... N ) )
87	86	eqcomd 2475	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( 0 ... N ) = dom S )
88	60, 87	eleqtrd 2557	. . . . . . . . . . . . . . . 16 |- ( ch -> j e. dom S )
89		fvelrn 6025	. . . . . . . . . . . . . . . 16 |- ( ( Fun S /\ j e. dom S ) -> ( S ` j ) e. ran S )
90	84, 88, 89	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ch -> ( S ` j ) e. ran S )
91	82, 90	sseldd 3510	. . . . . . . . . . . . . 14 |- ( ch -> ( S ` j ) e. ( A [,] B ) )
92		iccgelb 11593	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ ( S ` j ) e. ( A [,] B ) ) -> A <_ ( S ` j ) )
93	14, 18, 91, 92	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ch -> A <_ ( S ` j ) )
94	93	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A <_ ( S ` j ) )
95	62	rexrd 9655	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) e. RR* )
96		fzofzp1 11889	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
97	58, 96	syl 16	. . . . . . . . . . . . . . . 16 |- ( ch -> ( j + 1 ) e. ( 0 ... N ) )
98	55, 97	ffvelrnd 6033	. . . . . . . . . . . . . . 15 |- ( ch -> ( S ` ( j + 1 ) ) e. RR )
99	98	rexrd 9655	. . . . . . . . . . . . . 14 |- ( ch -> ( S ` ( j + 1 ) ) e. RR* )
100	99	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) e. RR* )
101		simpr 461	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
102		ioogtlb 31415	. . . . . . . . . . . . 13 |- ( ( ( S ` j ) e. RR* /\ ( S ` ( j + 1 ) ) e. RR* /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) < s )
103	95, 100, 101, 102	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) < s )
104	24, 62, 22, 94, 103	lelttrd 9751	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A < s )
105	98	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) e. RR )
106	8, 16	syl 16	. . . . . . . . . . . . 13 |- ( ch -> B e. RR )
107	106	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> B e. RR )
108		iooltub 31435	. . . . . . . . . . . . 13 |- ( ( ( S ` j ) e. RR* /\ ( S ` ( j + 1 ) ) e. RR* /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < ( S ` ( j + 1 ) ) )
109	95, 100, 101, 108	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < ( S ` ( j + 1 ) ) )
110	97, 87	eleqtrd 2557	. . . . . . . . . . . . . . . 16 |- ( ch -> ( j + 1 ) e. dom S )
111		fvelrn 6025	. . . . . . . . . . . . . . . 16 |- ( ( Fun S /\ ( j + 1 ) e. dom S ) -> ( S ` ( j + 1 ) ) e. ran S )
112	84, 110, 111	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ch -> ( S ` ( j + 1 ) ) e. ran S )
113	82, 112	sseldd 3510	. . . . . . . . . . . . . 14 |- ( ch -> ( S ` ( j + 1 ) ) e. ( A [,] B ) )
114		iccleub 11592	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) <_ B )
115	14, 18, 113, 114	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ch -> ( S ` ( j + 1 ) ) <_ B )
116	115	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) <_ B )
117	22, 105, 107, 109, 116	ltletrd 9753	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < B )
118	15, 19, 22, 104, 117	eliood 31418	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( A (,) B ) )
119	11, 118	sseldd 3510	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( A [,] B ) )
120		fourierdlem76.f	. . . . . . . . . . 11 |- ( ph -> F : RR --> RR )
121	120	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A [,] B ) ) -> F : RR --> RR )
122		fourierdlem76.xre	. . . . . . . . . . . 12 |- ( ph -> X e. RR )
123	122	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A [,] B ) ) -> X e. RR )
124	12, 16	iccssred 31426	. . . . . . . . . . . . 13 |- ( ph -> ( A [,] B ) C_ RR )
125	124	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A [,] B ) ) -> ( A [,] B ) C_ RR )
126		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ s e. ( A [,] B ) ) -> s e. ( A [,] B ) )
127	125, 126	sseldd 3510	. . . . . . . . . . 11 |- ( ( ph /\ s e. ( A [,] B ) ) -> s e. RR )
128	123, 127	readdcld 9635	. . . . . . . . . 10 |- ( ( ph /\ s e. ( A [,] B ) ) -> ( X + s ) e. RR )
129	121, 128	ffvelrnd 6033	. . . . . . . . 9 |- ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. RR )
130	9, 119, 129	syl2anc 661	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. RR )
131	130	recnd 9634	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
132		ax-resscn 9561	. . . . . . . . . 10 |- RR C_ CC
133		fourierdlem76.c	. . . . . . . . . 10 |- ( ph -> C e. RR )
134	132, 133	sseldi 3507	. . . . . . . . 9 |- ( ph -> C e. CC )
135	8, 134	syl 16	. . . . . . . 8 |- ( ch -> C e. CC )
136	135	adantr 465	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> C e. CC )
137	131, 136	subcld 9942	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
138	20	a1i 11	. . . . . . . 8 |- ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR )
139	138	sselda 3509	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. RR )
140	132, 139	sseldi 3507	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. CC )
141		nne 2668	. . . . . . . . . . . 12 |- ( -. s =/= 0 <-> s = 0 )
142	141	biimpi 194	. . . . . . . . . . 11 |- ( -. s =/= 0 -> s = 0 )
143	142	eqcomd 2475	. . . . . . . . . 10 |- ( -. s =/= 0 -> 0 = s )
144	143	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> 0 = s )
145	126	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> s e. ( A [,] B ) )
146	144, 145	eqeltrd 2555	. . . . . . . 8 |- ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> 0 e. ( A [,] B ) )
147		fourierdlem76.n0	. . . . . . . . 9 |- ( ph -> -. 0 e. ( A [,] B ) )
148	147	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> -. 0 e. ( A [,] B ) )
149	146, 148	condan 792	. . . . . . 7 |- ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 )
150	9, 119, 149	syl2anc 661	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s =/= 0 )
151	137, 140, 150	divcld 10332	. . . . 5 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - C ) / s ) e. CC )
152		2cn 10618	. . . . . . . 8 |- 2 e. CC
153	152	a1i 11	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. CC )
154	140	halfcld 10795	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / 2 ) e. CC )
155	154	sincld 13743	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. CC )
156	153, 155	mulcld 9628	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
157		2ne0 10640	. . . . . . . 8 |- 2 =/= 0
158	157	a1i 11	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 =/= 0 )
159	132, 21	sseldi 3507	. . . . . . . . . . . 12 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> s e. CC )
160	159	adantl 466	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. CC )
161		halfcl 10776	. . . . . . . . . . 11 |- ( s e. CC -> ( s / 2 ) e. CC )
162	160, 161	syl 16	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / 2 ) e. CC )
163		sincl 13739	. . . . . . . . . 10 |- ( ( s / 2 ) e. CC -> ( sin ` ( s / 2 ) ) e. CC )
164	162, 163	syl 16	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. CC )
165		fourierdlem76.ab	. . . . . . . . . . . . . . 15 |- ( ph -> ( A [,] B ) C_ ( -u pi [,] pi ) )
166	8, 165	syl 16	. . . . . . . . . . . . . 14 |- ( ch -> ( A [,] B ) C_ ( -u pi [,] pi ) )
167	166	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( A [,] B ) C_ ( -u pi [,] pi ) )
168	167, 119	sseldd 3510	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( -u pi [,] pi ) )
169		fourierdlem44 31774	. . . . . . . . . . . 12 |- ( ( s e. ( -u pi [,] pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
170	168, 150, 169	syl2anc 661	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
171	153, 164, 158, 170	mulne0d 10213	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
172	153, 164, 171	mulne0bbd 10217	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
173	153, 164, 158, 172	mulne0d 10213	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
174	153, 155, 173	mulne0bbd 10217	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
175	153, 155, 158, 174	mulne0d 10213	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
176	140, 156, 175	divcld 10332	. . . . 5 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
177		eqid 2467	. . . . . 6 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) )
178		eqid 2467	. . . . . 6 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s )
179	150	neneqd 2669	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. s = 0 )
180		elsn 4047	. . . . . . . 8 |- ( s e. { 0 } <-> s = 0 )
181	179, 180	sylnibr 305	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. s e. { 0 } )
182	140, 181	eldifd 3492	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( CC \ { 0 } ) )
183		eqid 2467	. . . . . . 7 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) )
184		eqid 2467	. . . . . . 7 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C )
185		elfzofz 11823	. . . . . . . . . . . . . . 15 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
186	185	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
187		pire 22718	. . . . . . . . . . . . . . . . . . . . . 22 |- pi e. RR
188	187	renegcli 9892	. . . . . . . . . . . . . . . . . . . . 21 |- -u pi e. RR
189	188	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -u pi e. RR )
190	189, 122	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( -u pi e. RR /\ X e. RR ) )
191		readdcl 9587	. . . . . . . . . . . . . . . . . . 19 |- ( ( -u pi e. RR /\ X e. RR ) -> ( -u pi + X ) e. RR )
192	190, 191	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( -u pi + X ) e. RR )
193	187	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> pi e. RR )
194	193, 122	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( pi e. RR /\ X e. RR ) )
195		readdcl 9587	. . . . . . . . . . . . . . . . . . 19 |- ( ( pi e. RR /\ X e. RR ) -> ( pi + X ) e. RR )
196	194, 195	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( pi + X ) e. RR )
197		iccssre 11618	. . . . . . . . . . . . . . . . . 18 |- ( ( ( -u pi + X ) e. RR /\ ( pi + X ) e. RR ) -> ( ( -u pi + X ) [,] ( pi + X ) ) C_ RR )
198	192, 196, 197	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( -u pi + X ) [,] ( pi + X ) ) C_ RR )
199	198	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( -u pi + X ) [,] ( pi + X ) ) C_ RR )
200		fourierdlem76.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 ) ) ) } )
201		fourierdlem76.m	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> M e. NN )
202		fourierdlem76.v	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> V e. ( P ` M ) )
203	200, 201, 202	fourierdlem15 31745	. . . . . . . . . . . . . . . . . 18 |- ( ph -> V : ( 0 ... M ) --> ( ( -u pi + X ) [,] ( pi + X ) ) )
204	203	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> V : ( 0 ... M ) --> ( ( -u pi + X ) [,] ( pi + X ) ) )
205	204, 186	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` i ) e. ( ( -u pi + X ) [,] ( pi + X ) ) )
206	199, 205	sseldd 3510	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` i ) e. RR )
207	122	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
208	206, 207	resubcld 9999	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
209	29	fvmpt2 5964	. . . . . . . . . . . . . 14 |- ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
210	186, 208, 209	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
211	210, 208	eqeltrd 2555	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
212	211	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
213	212	adantr 465	. . . . . . . . . 10 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
214	1, 213	sylbi 195	. . . . . . . . 9 |- ( ch -> ( Q ` i ) e. RR )
215		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( V ` i ) = ( V ` j ) )
216	215	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
217	216	cbvmptv 4544	. . . . . . . . . . . . . . . 16 |- ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
218	29, 217	eqtri 2496	. . . . . . . . . . . . . . 15 |- Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
219	218	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
220		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
221	220	oveq1d 6310	. . . . . . . . . . . . . . 15 |- ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
222	221	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
223		fzofzp1 11889	. . . . . . . . . . . . . . 15 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
224	223	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
225	204, 224	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` ( i + 1 ) ) e. ( ( -u pi + X ) [,] ( pi + X ) ) )
226	199, 225	sseldd 3510	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
227	226, 207	resubcld 9999	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
228	219, 222, 224, 227	fvmptd 5962	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
229	228, 227	eqeltrd 2555	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
230	229	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
231	230	adantr 465	. . . . . . . . . 10 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
232	1, 231	sylbi 195	. . . . . . . . 9 |- ( ch -> ( Q ` ( i + 1 ) ) e. RR )
233	200	fourierdlem2 31732	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) ) )
234	201, 233	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) ) ) )
235	202, 234	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) )
236	235	simprd 463	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( V ` 0 ) = ( -u pi + X ) /\ ( V ` M ) = ( pi + X ) ) /\ A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) )
237	236	simprd 463	. . . . . . . . . . . . . . . 16 |- ( ph -> A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
238	237	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
239		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0..^ M ) )
240		rspa 2834	. . . . . . . . . . . . . . 15 |- ( ( A. i e. ( 0..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) /\ i e. ( 0..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
241	238, 239, 240	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
242	206, 226, 207, 241	ltsub1dd 10176	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( V ` i ) - X ) < ( ( V ` ( i + 1 ) ) - X ) )
243	210, 228	breq12d 4466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( ( V ` i ) - X ) < ( ( V ` ( i + 1 ) ) - X ) ) )
244	242, 243	mpbird 232	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
245	244	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
246	245	adantr 465	. . . . . . . . . 10 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
247	1, 246	sylbi 195	. . . . . . . . 9 |- ( ch -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
248		simplr 754	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ j e. ( 0..^ N ) ) /\ i e. ( 0..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
249	6, 248	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ch -> i e. ( 0..^ M ) )
250	8, 249, 206	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ch -> ( V ` i ) e. RR )
251	250	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ch -> ( V ` i ) e. RR* )
252	251	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
253	8, 249, 226	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ch -> ( V ` ( i + 1 ) ) e. RR )
254	253	rexrd 9655	. . . . . . . . . . . . . . 15 |- ( ch -> ( V ` ( i + 1 ) ) e. RR* )
255	254	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` ( i + 1 ) ) e. RR* )
256	8, 122	syl 16	. . . . . . . . . . . . . . . 16 |- ( ch -> X e. RR )
257	256	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
258		elioore 11571	. . . . . . . . . . . . . . . 16 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
259	258	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
260	257, 259	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
261	8, 249, 210	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( Q ` i ) = ( ( V ` i ) - X ) )
262	261	oveq2d 6311	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( X + ( Q ` i ) ) = ( X + ( ( V ` i ) - X ) ) )
263	256	recnd 9634	. . . . . . . . . . . . . . . . . 18 |- ( ch -> X e. CC )
264	132, 250	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( V ` i ) e. CC )
265	263, 264	pncan3d 9945	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( X + ( ( V ` i ) - X ) ) = ( V ` i ) )
266	262, 265	eqtr2d 2509	. . . . . . . . . . . . . . . 16 |- ( ch -> ( V ` i ) = ( X + ( Q ` i ) ) )
267	266	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
268	6, 213	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( Q ` i ) e. RR )
269	268	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
270	268	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( Q ` i ) e. RR* )
271	270	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
272	6, 231	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ch -> ( Q ` ( i + 1 ) ) e. RR )
273	272	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( Q ` ( i + 1 ) ) e. RR* )
274	273	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
275		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
276		ioogtlb 31415	. . . . . . . . . . . . . . . . 17 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
277	271, 274, 275, 276	syl3anc 1228	. . . . . . . . . . . . . . . 16 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
278	269, 259, 257, 277	ltadd2dd 9752	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` i ) ) < ( X + s ) )
279	267, 278	eqbrtrd 4473	. . . . . . . . . . . . . 14 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
280	272	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
281		iooltub 31435	. . . . . . . . . . . . . . . . 17 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
282	271, 274, 275, 281	syl3anc 1228	. . . . . . . . . . . . . . . 16 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
283	259, 280, 257, 282	ltadd2dd 9752	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( X + ( Q ` ( i + 1 ) ) ) )
284	8, 249, 228	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
285	284	oveq2d 6311	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( X + ( Q ` ( i + 1 ) ) ) = ( X + ( ( V ` ( i + 1 ) ) - X ) ) )
286	132, 253	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( V ` ( i + 1 ) ) e. CC )
287	263, 286	pncan3d 9945	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( X + ( ( V ` ( i + 1 ) ) - X ) ) = ( V ` ( i + 1 ) ) )
288	285, 287	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ch -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
289	288	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
290	283, 289	breqtrd 4477	. . . . . . . . . . . . . 14 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( V ` ( i + 1 ) ) )
291	252, 255, 260, 279, 290	eliood 31418	. . . . . . . . . . . . 13 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
292		fvres 5886	. . . . . . . . . . . . 13 |- ( ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
293	291, 292	syl 16	. . . . . . . . . . . 12 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
294	293	eqcomd 2475	. . . . . . . . . . 11 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) )
295	294	mpteq2dva 4539	. . . . . . . . . 10 |- ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) )
296		ioossre 11598	. . . . . . . . . . . . 13 |- ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR
297	296, 132	sstri 3518	. . . . . . . . . . . 12 |- ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ CC
298	297	a1i 11	. . . . . . . . . . 11 |- ( ch -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ CC )
299		fourierdlem76.fcn	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
300	8, 249, 299	syl2anc 661	. . . . . . . . . . 11 |- ( ch -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
301		ioosscn 31414	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
302	301	a1i 11	. . . . . . . . . . 11 |- ( ch -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
303	298, 300, 302, 263, 291	fourierdlem23 31753	. . . . . . . . . 10 |- ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
304	295, 303	eqeltrd 2555	. . . . . . . . 9 |- ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
305	8, 120	syl 16	. . . . . . . . . 10 |- ( ch -> F : RR --> RR )
306		ioossre 11598	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
307	306	a1i 11	. . . . . . . . . 10 |- ( ch -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
308		eqid 2467	. . . . . . . . . 10 |- ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) )
309	296	a1i 11	. . . . . . . . . 10 |- ( ch -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR )
310	259, 282	ltned 9732	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= ( Q ` ( i + 1 ) ) )
311		fourierdlem76.l	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
312	8, 249, 311	syl2anc 661	. . . . . . . . . . 11 |- ( ch -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) )
313	288	eqcomd 2475	. . . . . . . . . . . 12 |- ( ch -> ( V ` ( i + 1 ) ) = ( X + ( Q ` ( i + 1 ) ) ) )
314	313	oveq2d 6311	. . . . . . . . . . 11 |- ( ch -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( V ` ( i + 1 ) ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( X + ( Q ` ( i + 1 ) ) ) ) )
315	312, 314	eleqtrd 2557	. . . . . . . . . 10 |- ( ch -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) lim CC ( X + ( Q ` ( i + 1 ) ) ) ) )
316	132, 272	sseldi 3507	. . . . . . . . . 10 |- ( ch -> ( Q ` ( i + 1 ) ) e. CC )
317	305, 256, 307, 308, 291, 309, 310, 315, 316	fourierdlem53 31783	. . . . . . . . 9 |- ( ch -> L e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
318	55, 60	ffvelrnd 6033	. . . . . . . . 9 |- ( ch -> ( S ` j ) e. RR )
319		elfzoelz 11809	. . . . . . . . . . . 12 |- ( j e. ( 0..^ N ) -> j e. ZZ )
320		zre 10880	. . . . . . . . . . . 12 |- ( j e. ZZ -> j e. RR )
321	58, 319, 320	3syl 20	. . . . . . . . . . 11 |- ( ch -> j e. RR )
322	321	ltp1d 10488	. . . . . . . . . 10 |- ( ch -> j < ( j + 1 ) )
323		isorel 6221	. . . . . . . . . . 11 |- ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( j e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
324	50, 60, 97, 323	syl12anc 1226	. . . . . . . . . 10 |- ( ch -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
325	322, 324	mpbid 210	. . . . . . . . 9 |- ( ch -> ( S ` j ) < ( S ` ( j + 1 ) ) )
326	1	simprbi 464	. . . . . . . . 9 |- ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
327		eqid 2467	. . . . . . . . 9 |- if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) )
328		eqid 2467	. . . . . . . . 9 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
329	214, 232, 247, 304, 317, 318, 98, 325, 326, 327, 328	fourierdlem33 31763	. . . . . . . 8 |- ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) e. ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
330		iftrue 3951	. . . . . . . . . . . 12 |- ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = L )
331		iftrue 3951	. . . . . . . . . . . 12 |- ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) = L )
332	330, 331	eqtr4d 2511	. . . . . . . . . . 11 |- ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
333	332	adantl 466	. . . . . . . . . 10 |- ( ( ch /\ ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
334		eqidd 2468	. . . . . . . . . . . 12 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
335		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> s = ( S ` ( j + 1 ) ) )
336	335	oveq2d 6311	. . . . . . . . . . . . 13 |- ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> ( X + s ) = ( X + ( S ` ( j + 1 ) ) ) )
337	336	fveq2d 5876	. . . . . . . . . . . 12 |- ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( S ` ( j + 1 ) ) ) ) )
338	214	rexrd 9655	. . . . . . . . . . . . . 14 |- ( ch -> ( Q ` i ) e. RR* )
339	338	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
340	232	rexrd 9655	. . . . . . . . . . . . . 14 |- ( ch -> ( Q ` ( i + 1 ) ) e. RR* )
341	340	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
342	98	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) e. RR )
343	6	simprd 463	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
344	318	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ch -> ( S ` j ) e. RR* )
345	270, 273, 344, 99, 325	ioossioobi 31444	. . . . . . . . . . . . . . . . 17 |- ( ch -> ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( Q ` i ) <_ ( S ` j ) /\ ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) ) ) )
346	343, 345	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ch -> ( ( Q ` i ) <_ ( S ` j ) /\ ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) ) )
347	346	simpld 459	. . . . . . . . . . . . . . 15 |- ( ch -> ( Q ` i ) <_ ( S ` j ) )
348	268, 318, 98, 347, 325	lelttrd 9751	. . . . . . . . . . . . . 14 |- ( ch -> ( Q ` i ) < ( S ` ( j + 1 ) ) )
349	348	adantr 465	. . . . . . . . . . . . 13 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < ( S ` ( j + 1 ) ) )
350	272	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
351	346	simprd 463	. . . . . . . . . . . . . . 15 |- ( ch -> ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
352	351	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
353		neqne 31339	. . . . . . . . . . . . . . . 16 |- ( -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> ( S ` ( j + 1 ) ) =/= ( Q ` ( i + 1 ) ) )
354	353	necomd 2738	. . . . . . . . . . . . . . 15 |- ( -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= ( S ` ( j + 1 ) ) )
355	354	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= ( S ` ( j + 1 ) ) )
356	342, 350, 352, 355	leneltd 31394	. . . . . . . . . . . . 13 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) < ( Q ` ( i + 1 ) ) )
357	339, 341, 342, 349, 356	eliood 31418	. . . . . . . . . . . 12 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
358	256, 98	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ch -> ( X + ( S ` ( j + 1 ) ) ) e. RR )
359	305, 358	ffvelrnd 6033	. . . . . . . . . . . . 13 |- ( ch -> ( F ` ( X + ( S ` ( j + 1 ) ) ) ) e. RR )
360	359	adantr 465	. . . . . . . . . . . 12 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( F ` ( X + ( S ` ( j + 1 ) ) ) ) e. RR )
361	334, 337, 357, 360	fvmptd 5962	. . . . . . . . . . 11 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) = ( F ` ( X + ( S ` ( j + 1 ) ) ) ) )
362	361	ifeq2d 3964	. . . . . . . . . 10 |- ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
363	333, 362	pm2.61dan 789	. . . . . . . . 9 |- ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
364	326	resmptd 5331	. . . . . . . . . 10 |- ( ch -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
365	364	oveq1d 6310	. . . . . . . . 9 |- ( ch -> ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) = ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
366	363, 365	eleq12d 2549	. . . . . . . 8 |- ( ch -> ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) e. ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) <-> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) lim CC ( S ` ( j + 1 ) ) ) ) )
367	329, 366	mpbid 210	. . . . . . 7 |- ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
368	138, 132	syl6ss 3521	. . . . . . . 8 |- ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ CC )
369	132, 98	sseldi 3507	. . . . . . . 8 |- ( ch -> ( S ` ( j + 1 ) ) e. CC )
370	184, 368, 135, 369	constlimc 31489	. . . . . . 7 |- ( ch -> C e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) lim CC ( S ` ( j + 1 ) ) ) )
371	183, 184, 177, 131, 136, 367, 370	sublimc 31517	. . . . . 6 |- ( ch -> ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) lim CC ( S ` ( j + 1 ) ) ) )
372	368, 178, 369	idlimc 31491	. . . . . 6 |- ( ch -> ( S ` ( j + 1 ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) lim CC ( S ` ( j + 1 ) ) ) )
373	8, 113	jca 532	. . . . . . 7 |- ( ch -> ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) )
374		eleq1 2539	. . . . . . . . . 10 |- ( s = ( S ` ( j + 1 ) ) -> ( s e. ( A [,] B ) <-> ( S ` ( j + 1 ) ) e. ( A [,] B ) ) )
375	374	anbi2d 703	. . . . . . . . 9 |- ( s = ( S ` ( j + 1 ) ) -> ( ( ph /\ s e. ( A [,] B ) ) <-> ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) ) )
376		neeq1 2748	. . . . . . . . 9 |- ( s = ( S ` ( j + 1 ) ) -> ( s =/= 0 <-> ( S ` ( j + 1 ) ) =/= 0 ) )
377	375, 376	imbi12d 320	. . . . . . . 8 |- ( s = ( S ` ( j + 1 ) ) -> ( ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 ) <-> ( ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) =/= 0 ) ) )
378	377, 149	vtoclg 3176	. . . . . . 7 |- ( ( S ` ( j + 1 ) ) e. RR -> ( ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) =/= 0 ) )
379	98, 373, 378	sylc 60	. . . . . 6 |- ( ch -> ( S ` ( j + 1 ) ) =/= 0 )
380	177, 178, 3, 137, 182, 371, 372, 379, 150	divlimc 31521	. . . . 5 |- ( ch -> ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) lim CC ( S ` ( j + 1 ) ) ) )
381		eqid 2467	. . . . . 6 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
382	153, 164	mulcld 9628	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
383	171	neneqd 2669	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 )
384		2re 10617	. . . . . . . . . . 11 |- 2 e. RR
385	384	a1i 11	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. RR )
386		rehalfcl 10777	. . . . . . . . . . . . 13 |- ( s e. RR -> ( s / 2 ) e. RR )
387	21, 386	syl 16	. . . . . . . . . . . 12 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( s / 2 ) e. RR )
388		resincl 13753	. . . . . . . . . . . 12 |- ( ( s / 2 ) e. RR -> ( sin ` ( s / 2 ) ) e. RR )
389	387, 388	syl 16	. . . . . . . . . . 11 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( sin ` ( s / 2 ) ) e. RR )
390	389	adantl 466	. . . . . . . . . 10 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. RR )
391	385, 390	remulcld 9636	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
392		elsncg 4056	. . . . . . . . 9 |- ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
393	391, 392	syl 16	. . . . . . . 8 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
394	383, 393	mtbird 301	. . . . . . 7 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } )
395	382, 394	eldifd 3492	. . . . . 6 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
396		eqid 2467	. . . . . . 7 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 )
397		eqid 2467	. . . . . . 7 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) )
398	152	a1i 11	. . . . . . . 8 |- ( ch -> 2 e. CC )
399	396, 368, 398, 369	constlimc 31489	. . . . . . 7 |- ( ch -> 2 e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) lim CC ( S ` ( j + 1 ) ) ) )
400	387	ad2antrl 727	. . . . . . . 8 |- ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) =/= ( ( S ` ( j + 1 ) ) / 2 ) ) ) -> ( s / 2 ) e. RR )
401		sinf 13737	. . . . . . . . . . 11 |- sin : CC --> CC
402	401	a1i 11	. . . . . . . . . 10 |- ( x e. RR -> sin : CC --> CC )
403	132	sseli 3505	. . . . . . . . . 10 |- ( x e. RR -> x e. CC )
404	402, 403	ffvelrnd 6033	. . . . . . . . 9 |- ( x e. RR -> ( sin ` x ) e. CC )
405	404	adantl 466	. . . . . . . 8 |- ( ( ch /\ x e. RR ) -> ( sin ` x ) e. CC )
406		eqid 2467	. . . . . . . . 9 |- ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) )
407		eldifsn 4158	. . . . . . . . . . 11 |- ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
408	152, 157, 407	mpbir2an 918	. . . . . . . . . 10 |- 2 e. ( CC \ { 0 } )
409	408	a1i 11	. . . . . . . . 9 |- ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. ( CC \ { 0 } ) )
410	157	a1i 11	. . . . . . . . 9 |- ( ch -> 2 =/= 0 )
411	178, 396, 406, 160, 409, 372, 399, 410, 158	divlimc 31521	. . . . . . . 8 |- ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) lim CC ( S ` ( j + 1 ) ) ) )
412	401	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> sin : CC --> CC )
413	132	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> RR C_ CC )
414	412, 413	feqresmpt 5928	. . . . . . . . . . . . 13 |- ( T. -> ( sin |` RR ) = ( x e. RR |-> ( sin ` x ) ) )
415	414	trud 1388	. . . . . . . . . . . 12 |- ( sin |` RR ) = ( x e. RR |-> ( sin ` x ) )
416	415	eqcomi 2480	. . . . . . . . . . 11 |- ( x e. RR |-> ( sin ` x ) ) = ( sin |` RR )
417		resincncf 31536	. . . . . . . . . . 11 |- ( sin |` RR ) e. ( RR -cn-> RR )
418	416, 417	eqeltri 2551	. . . . . . . . . 10 |- ( x e. RR |-> ( sin ` x ) ) e. ( RR -cn-> RR )
419	418	a1i 11	. . . . . . . . 9 |- ( ch -> ( x e. RR |-> ( sin ` x ) ) e. ( RR -cn-> RR ) )
420	98	rehalfcld 10797	. . . . . . . . 9 |- ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. RR )
421		fveq2 5872	. . . . . . . . 9 |- ( x = ( ( S ` ( j + 1 ) ) / 2 ) -> ( sin ` x ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
422	419, 420, 421	cnmptlimc 22162	. . . . . . . 8 |- ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. ( ( x e. RR |-> ( sin ` x ) ) lim CC ( ( S ` ( j + 1 ) ) / 2 ) ) )
423		fveq2 5872	. . . . . . . 8 |- ( x = ( s / 2 ) -> ( sin ` x ) = ( sin ` ( s / 2 ) ) )
424		fveq2 5872	. . . . . . . . 9 |- ( ( s / 2 ) = ( ( S ` ( j + 1 ) ) / 2 ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
425	424	ad2antll 728	. . . . . . . 8 |- ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) = ( ( S ` ( j + 1 ) ) / 2 ) ) ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
426	400, 405, 411, 422, 423, 425	limcco 22165	. . . . . . 7 |- ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
427	396, 397, 381, 153, 164, 399, 426	mullimc 31481	. . . . . 6 |- ( ch -> ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
428	369	halfcld 10795	. . . . . . . 8 |- ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. CC )
429	428	sincld 13743	. . . . . . 7 |- ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. CC )
430	166, 113	sseldd 3510	. . . . . . . 8 |- ( ch -> ( S ` ( j + 1 ) ) e. ( -u pi [,] pi ) )
431		fourierdlem44 31774	. . . . . . . 8 |- ( ( ( S ` ( j + 1 ) ) e. ( -u pi [,] pi ) /\ ( S ` ( j + 1 ) ) =/= 0 ) -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) =/= 0 )
432	430, 379, 431	syl2anc 661	. . . . . . 7 |- ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) =/= 0 )
433	398, 429, 410, 432	mulne0d 10213	. . . . . 6 |- ( ch -> ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) =/= 0 )
434	178, 381, 4, 160, 395, 372, 427, 433, 173	divlimc 31521	. . . . 5 |- ( ch -> ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) lim CC ( S ` ( j + 1 ) ) ) )
435	3, 4, 5, 151, 176, 380, 434	mullimc 31481	. . . 4 |- ( ch -> ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( (