Metamath Proof Explorer

Theorem fourierdlem80

Description: The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem80.f 
|- ( ph -> F : RR --> RR )
fourierdlem80.xre 
|- ( ph -> X e. RR )
fourierdlem80.a 
|- ( ph -> A e. RR )
fourierdlem80.b 
|- ( ph -> B e. RR )
fourierdlem80.ab 
|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
fourierdlem80.n0 
|- ( ph -> -. 0 e. ( A [,] B ) )
fourierdlem80.c 
|- ( ph -> C e. RR )
fourierdlem80.o 
|- O = ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
fourierdlem80.i 
|- I = ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) )
fourierdlem80.fbdioo 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w )
fourierdlem80.fdvbdioo 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )
fourierdlem80.sf 
|- ( ph -> S : ( 0 ... N ) --> ( A [,] B ) )
fourierdlem80.slt 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
fourierdlem80.sjss 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
fourierdlem80.relioo 
|- ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0 ..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )
fdv 
|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` I ) ) : I --> RR )
fourierdlem80.y 
|- Y = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
fourierdlem80.ch 
|- ( ch <-> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
Assertion fourierdlem80 
|- ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b )

Proof

Step Hyp Ref Expression
1 fourierdlem80.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem80.xre 
 |-  ( ph -> X e. RR )
3 fourierdlem80.a 
 |-  ( ph -> A e. RR )
4 fourierdlem80.b 
 |-  ( ph -> B e. RR )
5 fourierdlem80.ab 
 |-  ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
6 fourierdlem80.n0 
 |-  ( ph -> -. 0 e. ( A [,] B ) )
7 fourierdlem80.c 
 |-  ( ph -> C e. RR )
8 fourierdlem80.o 
 |-  O = ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
9 fourierdlem80.i 
 |-  I = ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) )
10 fourierdlem80.fbdioo 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w )
11 fourierdlem80.fdvbdioo 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )
12 fourierdlem80.sf 
 |-  ( ph -> S : ( 0 ... N ) --> ( A [,] B ) )
13 fourierdlem80.slt 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
14 fourierdlem80.sjss 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
15 fourierdlem80.relioo 
 |-  ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0 ..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )
16 fdv 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` I ) ) : I --> RR )
17 fourierdlem80.y 
 |-  Y = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
18 fourierdlem80.ch 
 |-  ( ch <-> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
19 oveq2 
 |-  ( s = t -> ( X + s ) = ( X + t ) )
20 19 fveq2d 
 |-  ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) )
21 20 oveq1d 
 |-  ( s = t -> ( ( F ` ( X + s ) ) - C ) = ( ( F ` ( X + t ) ) - C ) )
22 oveq1 
 |-  ( s = t -> ( s / 2 ) = ( t / 2 ) )
23 22 fveq2d 
 |-  ( s = t -> ( sin ` ( s / 2 ) ) = ( sin ` ( t / 2 ) ) )
24 23 oveq2d 
 |-  ( s = t -> ( 2 x. ( sin ` ( s / 2 ) ) ) = ( 2 x. ( sin ` ( t / 2 ) ) ) )
25 21 24 oveq12d 
 |-  ( s = t -> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) )
26 25 cbvmptv 
 |-  ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) )
27 8 26 eqtr2i 
 |-  ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) = O
28 27 oveq2i 
 |-  ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) = ( RR _D O )
29 28 dmeqi 
 |-  dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) = dom ( RR _D O )
30 29 ineq2i 
 |-  ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) = ( ran S i^i dom ( RR _D O ) )
31 30 sneqi 
 |-  { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } = { ( ran S i^i dom ( RR _D O ) ) }
32 31 uneq1i 
 |-  ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
33 snfi 
 |-  { ( ran S i^i dom ( RR _D O ) ) } e. Fin
34 fzofi 
 |-  ( 0 ..^ N ) e. Fin
35 eqid 
 |-  ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
36 35 rnmptfi 
 |-  ( ( 0 ..^ N ) e. Fin -> ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin )
37 34 36 ax-mp 
 |-  ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin
38 unfi 
 |-  ( ( { ( ran S i^i dom ( RR _D O ) ) } e. Fin /\ ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. Fin ) -> ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin )
39 33 37 38 mp2an 
 |-  ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin
40 39 a1i 
 |-  ( ph -> ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin )
41 32 40 eqeltrid 
 |-  ( ph -> ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) e. Fin )
42 id 
 |-  ( s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
43 32 unieqi 
 |-  U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
44 42 43 eleqtrdi 
 |-  ( s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
45 simpl 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ph )
46 uniun 
 |-  U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
47 46 eleq2i 
 |-  ( s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> s e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
48 elun 
 |-  ( s e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
49 47 48 sylbb 
 |-  ( s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
50 49 adantl 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
51 ovex 
 |-  ( 0 ... N ) e. _V
52 51 a1i 
 |-  ( ph -> ( 0 ... N ) e. _V )
53 12 52 fexd 
 |-  ( ph -> S e. _V )
54 rnexg 
 |-  ( S e. _V -> ran S e. _V )
55 inex1g 
 |-  ( ran S e. _V -> ( ran S i^i dom ( RR _D O ) ) e. _V )
56 unisng 
 |-  ( ( ran S i^i dom ( RR _D O ) ) e. _V -> U. { ( ran S i^i dom ( RR _D O ) ) } = ( ran S i^i dom ( RR _D O ) ) )
57 53 54 55 56 4syl 
 |-  ( ph -> U. { ( ran S i^i dom ( RR _D O ) ) } = ( ran S i^i dom ( RR _D O ) ) )
58 57 eleq2d 
 |-  ( ph -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } <-> s e. ( ran S i^i dom ( RR _D O ) ) ) )
59 58 adantr 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } <-> s e. ( ran S i^i dom ( RR _D O ) ) ) )
60 59 orbi1d 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( s e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) )
61 50 60 mpbid 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
62 dvf 
 |-  ( RR _D O ) : dom ( RR _D O ) --> CC
63 62 a1i 
 |-  ( s e. ( ran S i^i dom ( RR _D O ) ) -> ( RR _D O ) : dom ( RR _D O ) --> CC )
64 elinel2 
 |-  ( s e. ( ran S i^i dom ( RR _D O ) ) -> s e. dom ( RR _D O ) )
65 63 64 ffvelcdmd 
 |-  ( s e. ( ran S i^i dom ( RR _D O ) ) -> ( ( RR _D O ) ` s ) e. CC )
66 65 adantl 
 |-  ( ( ph /\ s e. ( ran S i^i dom ( RR _D O ) ) ) -> ( ( RR _D O ) ` s ) e. CC )
67 ovex 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) e. _V
68 67 dfiun3 
 |-  U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
69 68 eleq2i 
 |-  ( s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) <-> s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
70 69 biimpri 
 |-  ( s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
71 70 adantl 
 |-  ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
72 eliun 
 |-  ( s e. U_ j e. ( 0 ..^ N ) ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) <-> E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
73 71 72 sylib 
 |-  ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
74 nfv 
 |-  F/ j ph
75 nfmpt1 
 |-  F/_ j ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
76 75 nfrn 
 |-  F/_ j ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
77 76 nfuni 
 |-  F/_ j U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
78 77 nfcri 
 |-  F/ j s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
79 74 78 nfan 
 |-  F/ j ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
80 nfv 
 |-  F/ j ( ( RR _D O ) ` s ) e. CC
81 62 a1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( RR _D O ) : dom ( RR _D O ) --> CC )
82 8 reseq1i 
 |-  ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
83 ioossicc 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( S ` j ) [,] ( S ` ( j + 1 ) ) )
84 83 14 sstrid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
85 84 resmptd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
86 82 85 eqtrid 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
87 17 86 eqtr4id 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> Y = ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
88 87 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D Y ) = ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
89 ax-resscn 
 |-  RR C_ CC
90 89 a1i 
 |-  ( ph -> RR C_ CC )
91 1 adantr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> F : RR --> RR )
92 2 adantr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> X e. RR )
93 3 4 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
94 93 sselda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. RR )
95 92 94 readdcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( X + s ) e. RR )
96 91 95 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. RR )
97 96 recnd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. CC )
98 7 recnd 
 |-  ( ph -> C e. CC )
99 98 adantr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> C e. CC )
100 97 99 subcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
101 2cnd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> 2 e. CC )
102 93 90 sstrd 
 |-  ( ph -> ( A [,] B ) C_ CC )
103 102 sselda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. CC )
104 103 halfcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( s / 2 ) e. CC )
105 104 sincld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
106 101 105 mulcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
107 2ne0 
 |-  2 =/= 0
108 107 a1i 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> 2 =/= 0 )
109 5 sselda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. ( -u _pi [,] _pi ) )
110 eqcom 
 |-  ( s = 0 <-> 0 = s )
111 110 biimpi 
 |-  ( s = 0 -> 0 = s )
112 111 adantl 
 |-  ( ( s e. ( A [,] B ) /\ s = 0 ) -> 0 = s )
113 simpl 
 |-  ( ( s e. ( A [,] B ) /\ s = 0 ) -> s e. ( A [,] B ) )
114 112 113 eqeltrd 
 |-  ( ( s e. ( A [,] B ) /\ s = 0 ) -> 0 e. ( A [,] B ) )
115 114 adantll 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ s = 0 ) -> 0 e. ( A [,] B ) )
116 6 ad2antrr 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ s = 0 ) -> -. 0 e. ( A [,] B ) )
117 115 116 pm2.65da 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> -. s = 0 )
118 117 neqned 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 )
119 fourierdlem44 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
120 109 118 119 syl2anc 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
121 101 105 108 120 mulne0d 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
122 100 106 121 divcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
123 122 8 fmptd 
 |-  ( ph -> O : ( A [,] B ) --> CC )
124 ioossre 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR
125 124 a1i 
 |-  ( ph -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR )
126 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
127 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
128 126 127 dvres 
 |-  ( ( ( RR C_ CC /\ O : ( A [,] B ) --> CC ) /\ ( ( A [,] B ) C_ RR /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR ) ) -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
129 90 123 93 125 128 syl22anc 
 |-  ( ph -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
130 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) )
131 130 reseq2i 
 |-  ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
132 129 131 eqtrdi 
 |-  ( ph -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
133 132 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) = ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
134 88 133 eqtr2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( RR _D Y ) )
135 134 dmeqd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = dom ( RR _D Y ) )
136 1 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> F : RR --> RR )
137 2 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> X e. RR )
138 93 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ RR )
139 12 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> ( A [,] B ) )
140 elfzofz 
 |-  ( j e. ( 0 ..^ N ) -> j e. ( 0 ... N ) )
141 140 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ... N ) )
142 139 141 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. ( A [,] B ) )
143 138 142 sseldd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` j ) e. RR )
144 fzofzp1 
 |-  ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
145 144 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( j + 1 ) e. ( 0 ... N ) )
146 139 145 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. ( A [,] B ) )
147 138 146 sseldd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( S ` ( j + 1 ) ) e. RR )
148 9 feq2i 
 |-  ( ( RR _D ( F |` I ) ) : I --> RR <-> ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR )
149 16 148 sylib 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR )
150 9 reseq2i 
 |-  ( F |` I ) = ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) )
151 150 oveq2i 
 |-  ( RR _D ( F |` I ) ) = ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) )
152 151 feq1i 
 |-  ( ( RR _D ( F |` I ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR <-> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR )
153 149 152 sylib 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR )
154 5 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
155 84 154 sstrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
156 6 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( A [,] B ) )
157 84 156 ssneldd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
158 7 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> C e. RR )
159 136 137 143 147 153 155 157 158 17 fourierdlem57 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR /\ ( RR _D Y ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) ) /\ ( RR _D ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( cos ` ( s / 2 ) ) ) )
160 159 simpli 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR /\ ( RR _D Y ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) )
161 160 simpld 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR )
162 fdm 
 |-  ( ( RR _D Y ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> RR -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
163 161 162 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
164 135 163 eqtr2d 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
165 resss 
 |-  ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ ( RR _D O )
166 dmss 
 |-  ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ ( RR _D O ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ dom ( RR _D O ) )
167 165 166 mp1i 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> dom ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) C_ dom ( RR _D O ) )
168 164 167 eqsstrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ dom ( RR _D O ) )
169 168 3adant3 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ dom ( RR _D O ) )
170 simp3 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
171 169 170 sseldd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. dom ( RR _D O ) )
172 81 171 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC )
173 172 3exp 
 |-  ( ph -> ( j e. ( 0 ..^ N ) -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) ) )
174 173 adantr 
 |-  ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( j e. ( 0 ..^ N ) -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) ) )
175 79 80 174 rexlimd 
 |-  ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( E. j e. ( 0 ..^ N ) s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( RR _D O ) ` s ) e. CC ) )
176 73 175 mpd 
 |-  ( ( ph /\ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC )
177 66 176 jaodan 
 |-  ( ( ph /\ ( s e. ( ran S i^i dom ( RR _D O ) ) \/ s e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC )
178 45 61 177 syl2anc 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( ( RR _D O ) ` s ) e. CC )
179 178 abscld 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR )
180 44 179 sylan2 
 |-  ( ( ph /\ s e. U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR )
181 id 
 |-  ( r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
182 181 32 eleqtrdi 
 |-  ( r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
183 elsni 
 |-  ( r e. { ( ran S i^i dom ( RR _D O ) ) } -> r = ( ran S i^i dom ( RR _D O ) ) )
184 simpr 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> r = ( ran S i^i dom ( RR _D O ) ) )
185 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
186 rnffi 
 |-  ( ( S : ( 0 ... N ) --> ( A [,] B ) /\ ( 0 ... N ) e. Fin ) -> ran S e. Fin )
187 12 185 186 syl2anc 
 |-  ( ph -> ran S e. Fin )
188 infi 
 |-  ( ran S e. Fin -> ( ran S i^i dom ( RR _D O ) ) e. Fin )
189 187 188 syl 
 |-  ( ph -> ( ran S i^i dom ( RR _D O ) ) e. Fin )
190 189 adantr 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> ( ran S i^i dom ( RR _D O ) ) e. Fin )
191 184 190 eqeltrd 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> r e. Fin )
192 nfv 
 |-  F/ s ph
193 nfcv 
 |-  F/_ s ran S
194 nfcv 
 |-  F/_ s RR
195 nfcv 
 |-  F/_ s _D
196 nfmpt1 
 |-  F/_ s ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
197 8 196 nfcxfr 
 |-  F/_ s O
198 194 195 197 nfov 
 |-  F/_ s ( RR _D O )
199 198 nfdm 
 |-  F/_ s dom ( RR _D O )
200 193 199 nfin 
 |-  F/_ s ( ran S i^i dom ( RR _D O ) )
201 200 nfeq2 
 |-  F/ s r = ( ran S i^i dom ( RR _D O ) )
202 192 201 nfan 
 |-  F/ s ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) )
203 simpr 
 |-  ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. r )
204 simpl 
 |-  ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> r = ( ran S i^i dom ( RR _D O ) ) )
205 203 204 eleqtrd 
 |-  ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. ( ran S i^i dom ( RR _D O ) ) )
206 205 64 syl 
 |-  ( ( r = ( ran S i^i dom ( RR _D O ) ) /\ s e. r ) -> s e. dom ( RR _D O ) )
207 206 adantll 
 |-  ( ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) /\ s e. r ) -> s e. dom ( RR _D O ) )
208 62 ffvelcdmi 
 |-  ( s e. dom ( RR _D O ) -> ( ( RR _D O ) ` s ) e. CC )
209 208 abscld 
 |-  ( s e. dom ( RR _D O ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR )
210 207 209 syl 
 |-  ( ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) /\ s e. r ) -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR )
211 210 ex 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> ( s e. r -> ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) )
212 202 211 ralrimi 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) e. RR )
213 fimaxre3 
 |-  ( ( r e. Fin /\ A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) e. RR ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
214 191 212 213 syl2anc 
 |-  ( ( ph /\ r = ( ran S i^i dom ( RR _D O ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
215 183 214 sylan2 
 |-  ( ( ph /\ r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
216 215 adantlr 
 |-  ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
217 simpll 
 |-  ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> ph )
218 elunnel1 
 |-  ( ( r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
219 218 adantll 
 |-  ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
220 vex 
 |-  r e. _V
221 35 elrnmpt 
 |-  ( r e. _V -> ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
222 220 221 ax-mp 
 |-  ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
223 222 biimpi 
 |-  ( r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
224 223 adantl 
 |-  ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
225 76 nfcri 
 |-  F/ j r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
226 74 225 nfan 
 |-  F/ j ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
227 nfv 
 |-  F/ j E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y
228 reeanv 
 |-  ( E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) <-> ( E. w e. RR A. t e. I ( abs ` ( F ` t ) ) <_ w /\ E. z e. RR A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
229 10 11 228 sylanbrc 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
230 simp1 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ph /\ j e. ( 0 ..^ N ) ) )
231 simp2l 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> w e. RR )
232 simp2r 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> z e. RR )
233 230 231 232 jca31 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) )
234 simp3l 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> A. t e. I ( abs ` ( F ` t ) ) <_ w )
235 simp3r 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )
236 233 234 235 jca31 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
237 236 18 sylibr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> ch )
238 18 biimpi 
 |-  ( ch -> ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) )
239 simp-5l 
 |-  ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> ph )
240 238 239 syl 
 |-  ( ch -> ph )
241 240 1 syl 
 |-  ( ch -> F : RR --> RR )
242 240 2 syl 
 |-  ( ch -> X e. RR )
243 simp-4l 
 |-  ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> ( ph /\ j e. ( 0 ..^ N ) ) )
244 238 243 syl 
 |-  ( ch -> ( ph /\ j e. ( 0 ..^ N ) ) )
245 244 143 syl 
 |-  ( ch -> ( S ` j ) e. RR )
246 244 147 syl 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. RR )
247 244 13 syl 
 |-  ( ch -> ( S ` j ) < ( S ` ( j + 1 ) ) )
248 14 154 sstrd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
249 244 248 syl 
 |-  ( ch -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
250 14 156 ssneldd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> -. 0 e. ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) )
251 244 250 syl 
 |-  ( ch -> -. 0 e. ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) )
252 244 153 syl 
 |-  ( ch -> ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) : ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) --> RR )
253 simp-4r 
 |-  ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> w e. RR )
254 238 253 syl 
 |-  ( ch -> w e. RR )
255 238 simplrd 
 |-  ( ch -> A. t e. I ( abs ` ( F ` t ) ) <_ w )
256 id 
 |-  ( t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) -> t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) )
257 256 9 eleqtrrdi 
 |-  ( t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) -> t e. I )
258 rspa 
 |-  ( ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ t e. I ) -> ( abs ` ( F ` t ) ) <_ w )
259 255 257 258 syl2an 
 |-  ( ( ch /\ t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w )
260 simpllr 
 |-  ( ( ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ w e. RR ) /\ z e. RR ) /\ A. t e. I ( abs ` ( F ` t ) ) <_ w ) /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> z e. RR )
261 238 260 syl 
 |-  ( ch -> z e. RR )
262 151 fveq1i 
 |-  ( ( RR _D ( F |` I ) ) ` t ) = ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t )
263 262 fveq2i 
 |-  ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) = ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) )
264 238 simprd 
 |-  ( ch -> A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )
265 264 r19.21bi 
 |-  ( ( ch /\ t e. I ) -> ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z )
266 263 265 eqbrtrrid 
 |-  ( ( ch /\ t e. I ) -> ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) ) <_ z )
267 257 266 sylan2 
 |-  ( ( ch /\ t e. ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + ( S ` j ) ) (,) ( X + ( S ` ( j + 1 ) ) ) ) ) ) ` t ) ) <_ z )
268 240 7 syl 
 |-  ( ch -> C e. RR )
269 241 242 245 246 247 249 251 252 254 259 261 267 268 17 fourierdlem68 
 |-  ( ch -> ( dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
270 269 simprd 
 |-  ( ch -> E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y )
271 269 simpld 
 |-  ( ch -> dom ( RR _D Y ) = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
272 271 raleqdv 
 |-  ( ch -> ( A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
273 272 rexbidv 
 |-  ( ch -> ( E. y e. RR A. s e. dom ( RR _D Y ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
274 270 273 mpbid 
 |-  ( ch -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y )
275 130 eqcomi 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
276 275 reseq2i 
 |-  ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
277 276 fveq1i 
 |-  ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s )
278 fvres 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( RR _D O ) ` s ) )
279 278 adantl 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( RR _D O ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` s ) = ( ( RR _D O ) ` s ) )
280 244 84 syl 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
281 280 resmptd 
 |-  ( ch -> ( ( s e. ( A [,] B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
282 82 281 eqtrid 
 |-  ( ch -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
283 17 282 eqtr4id 
 |-  ( ch -> Y = ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
284 283 oveq2d 
 |-  ( ch -> ( RR _D Y ) = ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
285 284 fveq1d 
 |-  ( ch -> ( ( RR _D Y ) ` s ) = ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) )
286 129 fveq1d 
 |-  ( ph -> ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) )
287 240 286 syl 
 |-  ( ch -> ( ( RR _D ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) )
288 285 287 eqtr2d 
 |-  ( ch -> ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( RR _D Y ) ` s ) )
289 288 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( RR _D O ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ` s ) = ( ( RR _D Y ) ` s ) )
290 277 279 289 3eqtr3a 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( RR _D O ) ` s ) = ( ( RR _D Y ) ` s ) )
291 290 fveq2d 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( abs ` ( ( RR _D O ) ` s ) ) = ( abs ` ( ( RR _D Y ) ` s ) ) )
292 291 breq1d 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
293 292 ralbidva 
 |-  ( ch -> ( A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
294 293 rexbidv 
 |-  ( ch -> ( E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D Y ) ` s ) ) <_ y ) )
295 274 294 mpbird 
 |-  ( ch -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
296 237 295 syl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ ( w e. RR /\ z e. RR ) /\ ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
297 296 3exp 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( w e. RR /\ z e. RR ) -> ( ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) )
298 297 rexlimdvv 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( E. w e. RR E. z e. RR ( A. t e. I ( abs ` ( F ` t ) ) <_ w /\ A. t e. I ( abs ` ( ( RR _D ( F |` I ) ) ` t ) ) <_ z ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) )
299 229 298 mpd 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
300 299 3adant3 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
301 raleq 
 |-  ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) )
302 301 3ad2ant3 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) )
303 302 rexbidv 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y <-> E. y e. RR A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) )
304 300 303 mpbird 
 |-  ( ( ph /\ j e. ( 0 ..^ N ) /\ r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
305 304 3exp 
 |-  ( ph -> ( j e. ( 0 ..^ N ) -> ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) )
306 305 adantr 
 |-  ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( j e. ( 0 ..^ N ) -> ( r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) ) )
307 226 227 306 rexlimd 
 |-  ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> ( E. j e. ( 0 ..^ N ) r = ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y ) )
308 224 307 mpd 
 |-  ( ( ph /\ r e. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
309 217 219 308 syl2anc 
 |-  ( ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) /\ -. r e. { ( ran S i^i dom ( RR _D O ) ) } ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
310 216 309 pm2.61dan 
 |-  ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
311 182 310 sylan2 
 |-  ( ( ph /\ r e. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) ) -> E. y e. RR A. s e. r ( abs ` ( ( RR _D O ) ` s ) ) <_ y )
312 pm3.22 
 |-  ( ( r e. dom ( RR _D O ) /\ r e. ran S ) -> ( r e. ran S /\ r e. dom ( RR _D O ) ) )
313 elin 
 |-  ( r e. ( ran S i^i dom ( RR _D O ) ) <-> ( r e. ran S /\ r e. dom ( RR _D O ) ) )
314 312 313 sylibr 
 |-  ( ( r e. dom ( RR _D O ) /\ r e. ran S ) -> r e. ( ran S i^i dom ( RR _D O ) ) )
315 314 adantll 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> r e. ( ran S i^i dom ( RR _D O ) ) )
316 57 eqcomd 
 |-  ( ph -> ( ran S i^i dom ( RR _D O ) ) = U. { ( ran S i^i dom ( RR _D O ) ) } )
317 316 ad2antrr 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> ( ran S i^i dom ( RR _D O ) ) = U. { ( ran S i^i dom ( RR _D O ) ) } )
318 315 317 eleqtrd 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> r e. U. { ( ran S i^i dom ( RR _D O ) ) } )
319 318 orcd 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ r e. ran S ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
320 simpll 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ph )
321 89 a1i 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> RR C_ CC )
322 123 adantr 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> O : ( A [,] B ) --> CC )
323 3 adantr 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> A e. RR )
324 4 adantr 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> B e. RR )
325 323 324 iccssred 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> ( A [,] B ) C_ RR )
326 321 322 325 dvbss 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> dom ( RR _D O ) C_ ( A [,] B ) )
327 simpr 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. dom ( RR _D O ) )
328 326 327 sseldd 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. ( A [,] B ) )
329 328 adantr 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> r e. ( A [,] B ) )
330 simpr 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> -. r e. ran S )
331 fveq2 
 |-  ( j = k -> ( S ` j ) = ( S ` k ) )
332 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
333 332 fveq2d 
 |-  ( j = k -> ( S ` ( j + 1 ) ) = ( S ` ( k + 1 ) ) )
334 331 333 oveq12d 
 |-  ( j = k -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) = ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )
335 ovex 
 |-  ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) e. _V
336 334 35 335 fvmpt 
 |-  ( k e. ( 0 ..^ N ) -> ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) = ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )
337 336 eleq2d 
 |-  ( k e. ( 0 ..^ N ) -> ( r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) ) )
338 337 rexbiia 
 |-  ( E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> E. k e. ( 0 ..^ N ) r e. ( ( S ` k ) (,) ( S ` ( k + 1 ) ) ) )
339 15 338 sylibr 
 |-  ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) )
340 67 35 dmmpti 
 |-  dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( 0 ..^ N )
341 340 rexeqi 
 |-  ( E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) <-> E. k e. ( 0 ..^ N ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) )
342 339 341 sylibr 
 |-  ( ( ( ph /\ r e. ( A [,] B ) ) /\ -. r e. ran S ) -> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) )
343 320 329 330 342 syl21anc 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) )
344 funmpt 
 |-  Fun ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
345 elunirn 
 |-  ( Fun ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) )
346 344 345 mp1i 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ( r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) <-> E. k e. dom ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) r e. ( ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ` k ) ) )
347 343 346 mpbird 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
348 347 olcd 
 |-  ( ( ( ph /\ r e. dom ( RR _D O ) ) /\ -. r e. ran S ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
349 319 348 pm2.61dan 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
350 elun 
 |-  ( r e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> ( r e. U. { ( ran S i^i dom ( RR _D O ) ) } \/ r e. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
351 349 350 sylibr 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. ( U. { ( ran S i^i dom ( RR _D O ) ) } u. U. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
352 351 46 eleqtrrdi 
 |-  ( ( ph /\ r e. dom ( RR _D O ) ) -> r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
353 352 ralrimiva 
 |-  ( ph -> A. r e. dom ( RR _D O ) r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
354 dfss3 
 |-  ( dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) <-> A. r e. dom ( RR _D O ) r e. U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
355 353 354 sylibr 
 |-  ( ph -> dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D O ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
356 355 43 sseqtrrdi 
 |-  ( ph -> dom ( RR _D O ) C_ U. ( { ( ran S i^i dom ( RR _D ( t e. ( A [,] B ) |-> ( ( ( F ` ( X + t ) ) - C ) / ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) ) ) } u. ran ( j e. ( 0 ..^ N ) |-> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) ) )
357 41 180 311 356 ssfiunibd 
 |-  ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b )