Metamath Proof Explorer

Theorem fourierdlem68

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

Ref Expression
Hypotheses fourierdlem68.f 
|- ( ph -> F : RR --> RR )
fourierdlem68.xre 
|- ( ph -> X e. RR )
fourierdlem68.a 
|- ( ph -> A e. RR )
fourierdlem68.b 
|- ( ph -> B e. RR )
fourierdlem68.altb 
|- ( ph -> A < B )
fourierdlem68.ab 
|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
fourierdlem68.n0 
|- ( ph -> -. 0 e. ( A [,] B ) )
fourierdlem68.fdv 
|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
fourierdlem68.d 
|- ( ph -> D e. RR )
fourierdlem68.fbd 
|- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )
fourierdlem68.e 
|- ( ph -> E e. RR )
fourierdlem68.fdvbd 
|- ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )
fourierdlem68.c 
|- ( ph -> C e. RR )
fourierdlem68.o 
|- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
Assertion fourierdlem68 
|- ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )

Proof

Step Hyp Ref Expression
1 fourierdlem68.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem68.xre 
 |-  ( ph -> X e. RR )
3 fourierdlem68.a 
 |-  ( ph -> A e. RR )
4 fourierdlem68.b 
 |-  ( ph -> B e. RR )
5 fourierdlem68.altb 
 |-  ( ph -> A < B )
6 fourierdlem68.ab 
 |-  ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
7 fourierdlem68.n0 
 |-  ( ph -> -. 0 e. ( A [,] B ) )
8 fourierdlem68.fdv 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
9 fourierdlem68.d 
 |-  ( ph -> D e. RR )
10 fourierdlem68.fbd 
 |-  ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D )
11 fourierdlem68.e 
 |-  ( ph -> E e. RR )
12 fourierdlem68.fdvbd 
 |-  ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E )
13 fourierdlem68.c 
 |-  ( ph -> C e. RR )
14 fourierdlem68.o 
 |-  O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
15 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
16 15 6 sstrid 
 |-  ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
17 15 sseli 
 |-  ( 0 e. ( A (,) B ) -> 0 e. ( A [,] B ) )
18 7 17 nsyl 
 |-  ( ph -> -. 0 e. ( A (,) B ) )
19 1 2 3 4 8 16 18 13 14 fourierdlem57 
 |-  ( ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR /\ ( RR _D O ) = ( s e. ( A (,) B ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( 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. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
20 19 simpli 
 |-  ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR /\ ( RR _D O ) = ( s e. ( A (,) B ) |-> ( ( ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) - ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) ) / ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) ) ) ) )
21 20 simpld 
 |-  ( ph -> ( RR _D O ) : ( A (,) B ) --> RR )
22 21 fdmd 
 |-  ( ph -> dom ( RR _D O ) = ( A (,) B ) )
23 eqid 
 |-  ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) = ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) )
24 3 4 5 ltled 
 |-  ( ph -> A <_ B )
25 2re 
 |-  2 e. RR
26 25 a1i 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. RR )
27 3 4 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
28 27 sselda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. RR )
29 28 rehalfcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t / 2 ) e. RR )
30 29 resincld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) e. RR )
31 26 30 remulcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) e. RR )
32 2cnd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. CC )
33 30 recnd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> 2 =/= 0 )
36 6 sselda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( -u _pi [,] _pi ) )
37 eqcom 
 |-  ( t = 0 <-> 0 = t )
38 37 biimpi 
 |-  ( t = 0 -> 0 = t )
39 38 adantl 
 |-  ( ( t e. ( A [,] B ) /\ t = 0 ) -> 0 = t )
40 simpl 
 |-  ( ( t e. ( A [,] B ) /\ t = 0 ) -> t e. ( A [,] B ) )
41 39 40 eqeltrd 
 |-  ( ( t e. ( A [,] B ) /\ t = 0 ) -> 0 e. ( A [,] B ) )
42 41 adantll 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ t = 0 ) -> 0 e. ( A [,] B ) )
43 7 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A [,] B ) ) /\ t = 0 ) -> -. 0 e. ( A [,] B ) )
44 42 43 pm2.65da 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> -. t = 0 )
45 44 neqned 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t =/= 0 )
46 fourierdlem44 
 |-  ( ( t e. ( -u _pi [,] _pi ) /\ t =/= 0 ) -> ( sin ` ( t / 2 ) ) =/= 0 )
47 36 45 46 syl2anc 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( sin ` ( t / 2 ) ) =/= 0 )
48 32 33 35 47 mulne0d 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) =/= 0 )
49 eldifsn 
 |-  ( ( 2 x. ( sin ` ( t / 2 ) ) ) e. ( RR \ { 0 } ) <-> ( ( 2 x. ( sin ` ( t / 2 ) ) ) e. RR /\ ( 2 x. ( sin ` ( t / 2 ) ) ) =/= 0 ) )
50 31 48 49 sylanbrc 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( 2 x. ( sin ` ( t / 2 ) ) ) e. ( RR \ { 0 } ) )
51 50 23 fmptd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) )
52 difss 
 |-  ( RR \ { 0 } ) C_ RR
53 ax-resscn 
 |-  RR C_ CC
54 52 53 sstri 
 |-  ( RR \ { 0 } ) C_ CC
55 54 a1i 
 |-  ( ph -> ( RR \ { 0 } ) C_ CC )
56 27 53 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
57 2cnd 
 |-  ( ph -> 2 e. CC )
58 ssid 
 |-  CC C_ CC
59 58 a1i 
 |-  ( ph -> CC C_ CC )
60 56 57 59 constcncfg 
 |-  ( ph -> ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> CC ) )
61 sincn 
 |-  sin e. ( CC -cn-> CC )
62 61 a1i 
 |-  ( ph -> sin e. ( CC -cn-> CC ) )
63 56 59 idcncfg 
 |-  ( ph -> ( t e. ( A [,] B ) |-> t ) e. ( ( A [,] B ) -cn-> CC ) )
64 eldifsn 
 |-  ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
65 32 35 64 sylanbrc 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> 2 e. ( CC \ { 0 } ) )
66 eqid 
 |-  ( t e. ( A [,] B ) |-> 2 ) = ( t e. ( A [,] B ) |-> 2 )
67 65 66 fmptd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) )
68 difssd 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
69 cncffvrn 
 |-  ( ( ( CC \ { 0 } ) C_ CC /\ ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) ) )
70 68 60 69 syl2anc 
 |-  ( ph -> ( ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> 2 ) : ( A [,] B ) --> ( CC \ { 0 } ) ) )
71 67 70 mpbird 
 |-  ( ph -> ( t e. ( A [,] B ) |-> 2 ) e. ( ( A [,] B ) -cn-> ( CC \ { 0 } ) ) )
72 63 71 divcncf 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t / 2 ) ) e. ( ( A [,] B ) -cn-> CC ) )
73 62 72 cncfmpt1f 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( sin ` ( t / 2 ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
74 60 73 mulcncf 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
75 cncffvrn 
 |-  ( ( ( RR \ { 0 } ) C_ CC /\ ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) ) )
76 55 74 75 syl2anc 
 |-  ( ph -> ( ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) <-> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) : ( A [,] B ) --> ( RR \ { 0 } ) ) )
77 51 76 mpbird 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( 2 x. ( sin ` ( t / 2 ) ) ) ) e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) )
78 23 3 4 24 77 cncficcgt0 
 |-  ( ph -> E. c e. RR+ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) )
79 reelprrecn 
 |-  RR e. { RR , CC }
80 79 a1i 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> RR e. { RR , CC } )
81 1 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
82 2 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
83 elioore 
 |-  ( s e. ( A (,) B ) -> s e. RR )
84 83 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
85 82 84 readdcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
86 81 85 ffvelrnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
87 13 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
88 86 87 resubcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
89 88 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
90 89 3ad2antl1 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
91 79 a1i 
 |-  ( ph -> RR e. { RR , CC } )
92 86 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
93 8 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
94 2 3 readdcld 
 |-  ( ph -> ( X + A ) e. RR )
95 94 rexrd 
 |-  ( ph -> ( X + A ) e. RR* )
96 95 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
97 2 4 readdcld 
 |-  ( ph -> ( X + B ) e. RR )
98 97 rexrd 
 |-  ( ph -> ( X + B ) e. RR* )
99 98 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
100 3 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
101 100 rexrd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
102 4 rexrd 
 |-  ( ph -> B e. RR* )
103 102 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
104 simpr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
105 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
106 101 103 104 105 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
107 100 84 82 106 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
108 4 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
109 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
110 101 103 104 109 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
111 84 108 82 110 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
112 96 99 85 107 111 eliood 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
113 93 112 ffvelrnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. RR )
114 eqid 
 |-  ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
115 1 2 3 4 114 8 fourierdlem28 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
116 87 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
117 0red 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
118 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
119 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
120 119 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
121 118 120 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
122 121 a1i 
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
123 13 recnd 
 |-  ( ph -> C e. CC )
124 91 122 123 dvmptconst 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
125 91 92 113 115 116 117 124 dvmptsub 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) ) )
126 113 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
127 126 subid1d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) = ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) )
128 127 mpteq2dva 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) - 0 ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
129 125 128 eqtrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
130 129 3ad2ant1 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
131 126 3ad2antl1 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
132 2cnd 
 |-  ( s e. ( A (,) B ) -> 2 e. CC )
133 83 recnd 
 |-  ( s e. ( A (,) B ) -> s e. CC )
134 133 halfcld 
 |-  ( s e. ( A (,) B ) -> ( s / 2 ) e. CC )
135 134 sincld 
 |-  ( s e. ( A (,) B ) -> ( sin ` ( s / 2 ) ) e. CC )
136 132 135 mulcld 
 |-  ( s e. ( A (,) B ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
137 136 adantl 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
138 11 3ad2ant1 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> E e. RR )
139 1re 
 |-  1 e. RR
140 25 139 remulcli 
 |-  ( 2 x. 1 ) e. RR
141 140 a1i 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( 2 x. 1 ) e. RR )
142 1red 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> 1 e. RR )
143 123 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
144 9 143 readdcld 
 |-  ( ph -> ( D + ( abs ` C ) ) e. RR )
145 144 3ad2ant1 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( D + ( abs ` C ) ) e. RR )
146 simpl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ph )
147 146 112 jca 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) )
148 eleq1 
 |-  ( t = ( X + s ) -> ( t e. ( ( X + A ) (,) ( X + B ) ) <-> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) )
149 148 anbi2d 
 |-  ( t = ( X + s ) -> ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) <-> ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) ) )
150 fveq2 
 |-  ( t = ( X + s ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) = ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) )
151 150 fveq2d 
 |-  ( t = ( X + s ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
152 151 breq1d 
 |-  ( t = ( X + s ) -> ( ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E <-> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) )
153 149 152 imbi12d 
 |-  ( t = ( X + s ) -> ( ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` t ) ) <_ E ) <-> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) ) )
154 153 12 vtoclg 
 |-  ( ( X + s ) e. RR -> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E ) )
155 85 147 154 sylc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E )
156 155 3ad2antl1 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) <_ E )
157 132 135 absmuld 
 |-  ( s e. ( A (,) B ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) )
158 0le2 
 |-  0 <_ 2
159 absid 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
160 25 158 159 mp2an 
 |-  ( abs ` 2 ) = 2
161 160 oveq1i 
 |-  ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) = ( 2 x. ( abs ` ( sin ` ( s / 2 ) ) ) )
162 135 abscld 
 |-  ( s e. ( A (,) B ) -> ( abs ` ( sin ` ( s / 2 ) ) ) e. RR )
163 1red 
 |-  ( s e. ( A (,) B ) -> 1 e. RR )
164 25 a1i 
 |-  ( s e. ( A (,) B ) -> 2 e. RR )
165 158 a1i 
 |-  ( s e. ( A (,) B ) -> 0 <_ 2 )
166 83 rehalfcld 
 |-  ( s e. ( A (,) B ) -> ( s / 2 ) e. RR )
167 abssinbd 
 |-  ( ( s / 2 ) e. RR -> ( abs ` ( sin ` ( s / 2 ) ) ) <_ 1 )
168 166 167 syl 
 |-  ( s e. ( A (,) B ) -> ( abs ` ( sin ` ( s / 2 ) ) ) <_ 1 )
169 162 163 164 165 168 lemul2ad 
 |-  ( s e. ( A (,) B ) -> ( 2 x. ( abs ` ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
170 161 169 eqbrtrid 
 |-  ( s e. ( A (,) B ) -> ( ( abs ` 2 ) x. ( abs ` ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
171 157 170 eqbrtrd 
 |-  ( s e. ( A (,) B ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
172 171 adantl 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) <_ ( 2 x. 1 ) )
173 abscosbd 
 |-  ( ( s / 2 ) e. RR -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
174 104 166 173 3syl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
175 174 3ad2antl1 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( cos ` ( s / 2 ) ) ) <_ 1 )
176 89 abscld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) e. RR )
177 92 abscld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( F ` ( X + s ) ) ) e. RR )
178 116 abscld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` C ) e. RR )
179 177 178 readdcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) e. RR )
180 9 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> D e. RR )
181 180 178 readdcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( D + ( abs ` C ) ) e. RR )
182 92 116 abs2dif2d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) )
183 fveq2 
 |-  ( t = ( X + s ) -> ( F ` t ) = ( F ` ( X + s ) ) )
184 183 fveq2d 
 |-  ( t = ( X + s ) -> ( abs ` ( F ` t ) ) = ( abs ` ( F ` ( X + s ) ) ) )
185 184 breq1d 
 |-  ( t = ( X + s ) -> ( ( abs ` ( F ` t ) ) <_ D <-> ( abs ` ( F ` ( X + s ) ) ) <_ D ) )
186 149 185 imbi12d 
 |-  ( t = ( X + s ) -> ( ( ( ph /\ t e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` t ) ) <_ D ) <-> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D ) ) )
187 186 10 vtoclg 
 |-  ( ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) -> ( ( ph /\ ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D ) )
188 112 147 187 sylc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( F ` ( X + s ) ) ) <_ D )
189 177 180 178 188 leadd1dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( abs ` ( F ` ( X + s ) ) ) + ( abs ` C ) ) <_ ( D + ( abs ` C ) ) )
190 176 179 181 182 189 letrd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( D + ( abs ` C ) ) )
191 190 3ad2antl1 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( abs ` ( ( F ` ( X + s ) ) - C ) ) <_ ( D + ( abs ` C ) ) )
192 19 simpri 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
193 192 a1i 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
194 134 coscld 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
195 194 adantl 
 |-  ( ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
196 simp2 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> c e. RR+ )
197 oveq1 
 |-  ( t = s -> ( t / 2 ) = ( s / 2 ) )
198 197 fveq2d 
 |-  ( t = s -> ( sin ` ( t / 2 ) ) = ( sin ` ( s / 2 ) ) )
199 198 oveq2d 
 |-  ( t = s -> ( 2 x. ( sin ` ( t / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
200 199 fveq2d 
 |-  ( t = s -> ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) = ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
201 200 breq2d 
 |-  ( t = s -> ( c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) <-> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
202 201 cbvralvw 
 |-  ( A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) <-> A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
203 nfv 
 |-  F/ s ph
204 nfra1 
 |-  F/ s A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) )
205 203 204 nfan 
 |-  F/ s ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
206 simplr 
 |-  ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
207 15 104 sseldi 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A [,] B ) )
208 207 adantlr 
 |-  ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> s e. ( A [,] B ) )
209 rspa 
 |-  ( ( A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) /\ s e. ( A [,] B ) ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
210 206 208 209 syl2anc 
 |-  ( ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) /\ s e. ( A (,) B ) ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
211 210 ex 
 |-  ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) -> ( s e. ( A (,) B ) -> c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
212 205 211 ralrimi 
 |-  ( ( ph /\ A. s e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
213 202 212 sylan2b 
 |-  ( ( ph /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
214 213 3adant2 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> A. s e. ( A (,) B ) c <_ ( abs ` ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
215 eqid 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
216 80 90 130 131 137 138 141 142 145 156 172 175 191 193 195 196 214 215 dvdivbd 
 |-  ( ( ph /\ c e. RR+ /\ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) ) -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
217 216 rexlimdv3a 
 |-  ( ph -> ( E. c e. RR+ A. t e. ( A [,] B ) c <_ ( abs ` ( 2 x. ( sin ` ( t / 2 ) ) ) ) -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
218 78 217 mpd 
 |-  ( ph -> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
219 nfcv 
 |-  F/_ s RR
220 nfcv 
 |-  F/_ s _D
221 nfmpt1 
 |-  F/_ s ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
222 14 221 nfcxfr 
 |-  F/_ s O
223 219 220 222 nfov 
 |-  F/_ s ( RR _D O )
224 223 nfdm 
 |-  F/_ s dom ( RR _D O )
225 nfcv 
 |-  F/_ s ( A (,) B )
226 224 225 raleqf 
 |-  ( dom ( RR _D O ) = ( A (,) B ) -> ( A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
227 22 226 syl 
 |-  ( ph -> ( A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
228 227 rexbidv 
 |-  ( ph -> ( E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b <-> E. b e. RR A. s e. ( A (,) B ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
229 218 228 mpbird 
 |-  ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b )
230 14 a1i 
 |-  ( ph -> O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
231 230 oveq2d 
 |-  ( ph -> ( RR _D O ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
232 231 fveq1d 
 |-  ( ph -> ( ( RR _D O ) ` s ) = ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) )
233 232 fveq2d 
 |-  ( ph -> ( abs ` ( ( RR _D O ) ` s ) ) = ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) )
234 233 breq1d 
 |-  ( ph -> ( ( abs ` ( ( RR _D O ) ` s ) ) <_ b <-> ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
235 234 rexralbidv 
 |-  ( ph -> ( E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b <-> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) ` s ) ) <_ b ) )
236 229 235 mpbird 
 |-  ( ph -> E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b )
237 22 236 jca 
 |-  ( ph -> ( dom ( RR _D O ) = ( A (,) B ) /\ E. b e. RR A. s e. dom ( RR _D O ) ( abs ` ( ( RR _D O ) ` s ) ) <_ b ) )