fourierdlem86

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem86.f	\|- ( ph -> F : RR --> RR )
2		fourierdlem86.xre	\|- ( ph -> X e. RR )
3		fourierdlem86.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 ) ) ) } )
4		fourierdlem86.m	\|- ( ph -> M e. NN )
5		fourierdlem86.v	\|- ( ph -> V e. ( P ` M ) )
6		fourierdlem86.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
7		fourierdlem86.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
8		fourierdlem86.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
9		fourierdlem86.a	\|- ( ph -> A e. RR )
10		fourierdlem86.b	\|- ( ph -> B e. RR )
11		fourierdlem86.altb	\|- ( ph -> A < B )
12		fourierdlem86.ab	\|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
13		fourierdlem86.n0	\|- ( ph -> -. 0 e. ( A [,] B ) )
14		fourierdlem86.c	\|- ( ph -> C e. RR )
15		fourierdlem86.o	\|- O = ( s e. ( A [,] B ) \|-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
16		fourierdlem86.q	\|- Q = ( i e. ( 0 ... M ) \|-> ( ( V ` i ) - X ) )
17		fourierdlem86.t	\|- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
18		fourierdlem86.n	\|- N = ( ( # ` T ) - 1 )
19		fourierdlem86.s	\|- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
20		fourierdlem86.d	\|- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )
21		fourierdlem86.e	\|- E = ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
22		fourierdlem86.u	\|- U = ( iota_ i e. ( 0 ..^ M ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
23	2	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> X e. RR )
24	4	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> M e. NN )
25	5	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> V e. ( P ` M ) )
26	9	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> A e. RR )
27	10	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> B e. RR )
28	11	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> A < B )
29	12	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
30		simpr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
31		biid	\|- ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` y ) (,) ( Q ` ( y + 1 ) ) ) ) <-> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` y ) (,) ( Q ` ( y + 1 ) ) ) ) )
32	23 3 24 25 26 27 28 29 16 17 18 19 30 22 31	fourierdlem50	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( U e. ( 0 ..^ M ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )
33	32	simpld	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> U e. ( 0 ..^ M ) )
34		id	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ph /\ j e. ( 0 ..^ N ) ) )
35	32	simprd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
36	34 33 35	jca31	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )
37		nfv	\|- F/ i ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
38		nfv	\|- F/ i ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) )
39		nfcsb1v	\|- F/_ i [_ U / i ]_ L
40		nfcv	\|- F/_ i ( F ` ( X + ( S ` ( j + 1 ) ) ) )
41	38 39 40	nfif	\|- F/_ i if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) )
42		nfcv	\|- F/_ i -
43		nfcv	\|- F/_ i C
44	41 42 43	nfov	\|- F/_ i ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C )
45		nfcv	\|- F/_ i /
46		nfcv	\|- F/_ i ( S ` ( j + 1 ) )
47	44 45 46	nfov	\|- F/_ i ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) )
48		nfcv	\|- F/_ i x.
49		nfcv	\|- F/_ i ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) )
50	47 48 49	nfov	\|- F/_ i ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )
51	50	nfel1	\|- F/ i ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) )
52		nfv	\|- F/ i ( S ` j ) = ( Q ` U )
53		nfcsb1v	\|- F/_ i [_ U / i ]_ R
54		nfcv	\|- F/_ i ( F ` ( X + ( S ` j ) ) )
55	52 53 54	nfif	\|- F/_ i if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) )
56	55 42 43	nfov	\|- F/_ i ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C )
57		nfcv	\|- F/_ i ( S ` j )
58	56 45 57	nfov	\|- F/_ i ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) )
59		nfcv	\|- F/_ i ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) )
60	58 48 59	nfov	\|- F/_ i ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
61	60	nfel1	\|- F/ i ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) )
62	51 61	nfan	\|- F/ i ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
63		nfv	\|- F/ i ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC )
64	62 63	nfan	\|- F/ i ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
65	37 64	nfim	\|- F/ i ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) -> ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
66		eleq1	\|- ( i = U -> ( i e. ( 0 ..^ M ) <-> U e. ( 0 ..^ M ) ) )
67	66	anbi2d	\|- ( i = U -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) <-> ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) ) )
68		fveq2	\|- ( i = U -> ( Q ` i ) = ( Q ` U ) )
69		oveq1	\|- ( i = U -> ( i + 1 ) = ( U + 1 ) )
70	69	fveq2d	\|- ( i = U -> ( Q ` ( i + 1 ) ) = ( Q ` ( U + 1 ) ) )
71	68 70	oveq12d	\|- ( i = U -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) )
72	71	sseq2d	\|- ( i = U -> ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) )
73	67 72	anbi12d	\|- ( i = U -> ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) <-> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) ) )
74	70	eqeq2d	\|- ( i = U -> ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) <-> ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) ) )
75		csbeq1a	\|- ( i = U -> L = [_ U / i ]_ L )
76	74 75	ifbieq1d	\|- ( i = U -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
77	76	oveq1d	\|- ( i = U -> ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) = ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) )
78	77	oveq1d	\|- ( i = U -> ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) = ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) )
79	78	oveq1d	\|- ( i = U -> ( ( ( 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 ) ) ) ) ) = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) )
80	79	eleq1d	\|- ( i = U -> ( ( ( ( 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 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) <-> ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) ) )
81	68	eqeq2d	\|- ( i = U -> ( ( S ` j ) = ( Q ` i ) <-> ( S ` j ) = ( Q ` U ) ) )
82		csbeq1a	\|- ( i = U -> R = [_ U / i ]_ R )
83	81 82	ifbieq1d	\|- ( i = U -> if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) = if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) )
84	83	oveq1d	\|- ( i = U -> ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) = ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) )
85	84	oveq1d	\|- ( i = U -> ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) = ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) )
86	85	oveq1d	\|- ( i = U -> ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) = ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) )
87	86	eleq1d	\|- ( i = U -> ( ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) <-> ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) )
88	80 87	anbi12d	\|- ( i = U -> ( ( ( ( ( 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 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) <-> ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) ) )
89	88	anbi1d	\|- ( i = U -> ( ( ( ( ( ( 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 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) <-> ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
90	73 89	imbi12d	\|- ( i = U -> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( ( 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 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) ) <-> ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) -> ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) ) ) )
91		eqid	\|- ( ( ( 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 ) ) ) ) ) = ( ( ( 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 ) ) ) ) )
92		eqid	\|- ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
93		biid	\|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) <-> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
94	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 91 92 93	fourierdlem76	\|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( ( ( 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 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
95	65 90 94	vtoclg1f	\|- ( U e. ( 0 ..^ M ) -> ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ U e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` U ) (,) ( Q ` ( U + 1 ) ) ) ) -> ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
96	33 36 95	sylc	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )
97	96	simpld	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) )
98	97	simpld	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( U + 1 ) ) , [_ U / i ]_ L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
99	20 98	eqeltrid	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> D e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
100	97	simprd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( ( if ( ( S ` j ) = ( Q ` U ) , [_ U / i ]_ R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
101	21 100	eqeltrid	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
102	96	simprd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
103	99 101 102	jca31	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( D e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )

Metamath Proof Explorer

Theorem fourierdlem86

Proof