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