Metamath Proof Explorer


Theorem fourierdlem80

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

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

Proof

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