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