Metamath Proof Explorer

Theorem 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 ) ) )