Metamath Proof Explorer

Theorem fourierdlem57

Description: The derivative of O . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem57.f 
|- ( ph -> F : RR --> RR )
fourierdlem57.xre 
|- ( ph -> X e. RR )
fourierdlem57.a 
|- ( ph -> A e. RR )
fourierdlem57.b 
|- ( ph -> B e. RR )
fourierdlem57.fdv 
|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
fourierdlem57.ab 
|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
fourierdlem57.n0 
|- ( ph -> -. 0 e. ( A (,) B ) )
fourierdlem57.c 
|- ( ph -> C e. RR )
fourierdlem57.o 
|- O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem57.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem57.xre 
 |-  ( ph -> X e. RR )
3 fourierdlem57.a 
 |-  ( ph -> A e. RR )
4 fourierdlem57.b 
 |-  ( ph -> B e. RR )
5 fourierdlem57.fdv 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
6 fourierdlem57.ab 
 |-  ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
7 fourierdlem57.n0 
 |-  ( ph -> -. 0 e. ( A (,) B ) )
8 fourierdlem57.c 
 |-  ( ph -> C e. RR )
9 fourierdlem57.o 
 |-  O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
10 5 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
11 2 3 readdcld 
 |-  ( ph -> ( X + A ) e. RR )
12 11 rexrd 
 |-  ( ph -> ( X + A ) e. RR* )
13 12 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
14 2 4 readdcld 
 |-  ( ph -> ( X + B ) e. RR )
15 14 rexrd 
 |-  ( ph -> ( X + B ) e. RR* )
16 15 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
17 2 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
18 elioore 
 |-  ( s e. ( A (,) B ) -> s e. RR )
19 18 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
20 17 19 readdcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
21 3 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
22 21 rexrd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
23 4 rexrd 
 |-  ( ph -> B e. RR* )
24 23 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
25 simpr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
26 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
27 22 24 25 26 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
28 21 19 17 27 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
29 4 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
30 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
31 22 24 25 30 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
32 19 29 17 31 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
33 13 16 20 28 32 eliood 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
34 10 33 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. RR )
35 2re 
 |-  2 e. RR
36 35 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. RR )
37 rehalfcl 
 |-  ( s e. RR -> ( s / 2 ) e. RR )
38 19 37 syl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR )
39 38 resincld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR )
40 36 39 remulcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
41 34 40 remulcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) x. ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
42 38 recoscld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. RR )
43 1 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
44 43 20 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
45 8 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
46 44 45 resubcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
47 42 46 remulcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( ( F ` ( X + s ) ) - C ) ) e. RR )
48 41 47 resubcld 
 |-  ( ( ph /\ 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 ) ) ) e. RR )
49 40 resqcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) e. RR )
50 2cnd 
 |-  ( s e. RR -> 2 e. CC )
51 37 recnd 
 |-  ( s e. RR -> ( s / 2 ) e. CC )
52 51 sincld 
 |-  ( s e. RR -> ( sin ` ( s / 2 ) ) e. CC )
53 50 52 mulcld 
 |-  ( s e. RR -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
54 19 53 syl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
55 2cnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC )
56 19 52 syl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
57 2ne0 
 |-  2 =/= 0
58 57 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 )
59 6 sselda 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) )
60 eqcom 
 |-  ( s = 0 <-> 0 = s )
61 60 biimpi 
 |-  ( s = 0 -> 0 = s )
62 61 adantl 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 = s )
63 simpl 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> s e. ( A (,) B ) )
64 62 63 eqeltrd 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
65 64 adantll 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
66 7 ad2antrr 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) )
67 65 66 pm2.65da 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
68 67 neqned 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
69 fourierdlem44 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
70 59 68 69 syl2anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
71 55 56 58 70 mulne0d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
72 2z 
 |-  2 e. ZZ
73 72 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. ZZ )
74 54 71 73 expne0d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) =/= 0 )
75 48 49 74 redivcld 
 |-  ( ( ph /\ 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 ) ) e. RR )
76 eqid 
 |-  ( 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 ) ) ) = ( 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 ) ) )
77 75 76 fmptd 
 |-  ( ph -> ( 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 ) ) ) : ( A (,) B ) --> RR )
78 9 a1i 
 |-  ( ph -> O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
79 78 oveq2d 
 |-  ( ph -> ( RR _D O ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
80 reelprrecn 
 |-  RR e. { RR , CC }
81 80 a1i 
 |-  ( ph -> RR e. { RR , CC } )
82 46 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
83 44 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
84 eqid 
 |-  ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
85 1 2 3 4 84 5 fourierdlem28 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
86 45 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
87 0red 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
88 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
89 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
90 88 89 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
91 90 a1i 
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
92 8 recnd 
 |-  ( ph -> C e. CC )
93 81 91 92 dvmptconst 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
94 81 83 34 85 86 87 93 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 ) ) )
95 34 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
96 95 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 ) ) )
97 96 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 ) ) ) )
98 94 97 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 ) ) ) )
99 eldifsn 
 |-  ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) <-> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC /\ ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 ) )
100 54 71 99 sylanbrc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
101 recn 
 |-  ( s e. RR -> s e. CC )
102 57 a1i 
 |-  ( s e. RR -> 2 =/= 0 )
103 101 50 102 divrec2d 
 |-  ( s e. RR -> ( s / 2 ) = ( ( 1 / 2 ) x. s ) )
104 103 eqcomd 
 |-  ( s e. RR -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
105 18 104 syl 
 |-  ( s e. ( A (,) B ) -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
106 105 fveq2d 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) = ( cos ` ( s / 2 ) ) )
107 halfcn 
 |-  ( 1 / 2 ) e. CC
108 107 a1i 
 |-  ( s e. CC -> ( 1 / 2 ) e. CC )
109 id 
 |-  ( s e. CC -> s e. CC )
110 108 109 mulcld 
 |-  ( s e. CC -> ( ( 1 / 2 ) x. s ) e. CC )
111 110 coscld 
 |-  ( s e. CC -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
112 18 101 111 3syl 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
113 106 112 eqeltrrd 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
114 113 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
115 ioossre 
 |-  ( A (,) B ) C_ RR
116 resmpt 
 |-  ( ( A (,) B ) C_ RR -> ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
117 115 116 ax-mp 
 |-  ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
118 117 eqcomi 
 |-  ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) )
119 118 oveq2i 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) )
120 ax-resscn 
 |-  RR C_ CC
121 eqid 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
122 121 53 fmpti 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC
123 ssid 
 |-  RR C_ RR
124 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
125 124 89 dvres 
 |-  ( ( ( RR C_ CC /\ ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC ) /\ ( RR C_ RR /\ ( A (,) B ) C_ RR ) ) -> ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) )
126 120 122 123 115 125 mp4an 
 |-  ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
127 resmpt 
 |-  ( RR C_ CC -> ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
128 120 127 ax-mp 
 |-  ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
129 104 fveq2d 
 |-  ( s e. RR -> ( sin ` ( ( 1 / 2 ) x. s ) ) = ( sin ` ( s / 2 ) ) )
130 129 oveq2d 
 |-  ( s e. RR -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
131 130 mpteq2ia 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
132 128 131 eqtr2i 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
133 132 oveq2i 
 |-  ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) )
134 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
135 133 134 reseq12i 
 |-  ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) = ( ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) |` ( A (,) B ) )
136 eqid 
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
137 2cnd 
 |-  ( s e. CC -> 2 e. CC )
138 110 sincld 
 |-  ( s e. CC -> ( sin ` ( ( 1 / 2 ) x. s ) ) e. CC )
139 137 138 mulcld 
 |-  ( s e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
140 136 139 fmpti 
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC
141 ssid 
 |-  CC C_ CC
142 dmmptg 
 |-  ( A. s e. CC ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) e. CC -> dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = CC )
143 2cn 
 |-  2 e. CC
144 143 107 mulcli 
 |-  ( 2 x. ( 1 / 2 ) ) e. CC
145 144 a1i 
 |-  ( s e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
146 145 111 mulcld 
 |-  ( s e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
147 142 146 mprg 
 |-  dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = CC
148 120 147 sseqtrri 
 |-  RR C_ dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
149 dvasinbx 
 |-  ( ( 2 e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) )
150 143 107 149 mp2an 
 |-  ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
151 150 dmeqi 
 |-  dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
152 148 151 sseqtrri 
 |-  RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
153 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) ) ) -> ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) )
154 80 140 141 152 153 mp4an 
 |-  ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR )
155 154 reseq1i 
 |-  ( ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) |` ( A (,) B ) ) = ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) )
156 150 reseq1i 
 |-  ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
157 156 reseq1i 
 |-  ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) )
158 resabs1 
 |-  ( ( A (,) B ) C_ RR -> ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) )
159 115 158 ax-mp 
 |-  ( ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) )
160 ioosscn 
 |-  ( A (,) B ) C_ CC
161 resmpt 
 |-  ( ( A (,) B ) C_ CC -> ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) )
162 160 161 ax-mp 
 |-  ( ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
163 157 159 162 3eqtri 
 |-  ( ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
164 135 155 163 3eqtri 
 |-  ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
165 119 126 164 3eqtri 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
166 143 57 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
167 166 oveq1i 
 |-  ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) )
168 167 a1i 
 |-  ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
169 112 mullidd 
 |-  ( s e. ( A (,) B ) -> ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( ( 1 / 2 ) x. s ) ) )
170 168 169 106 3eqtrd 
 |-  ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( s / 2 ) ) )
171 170 mpteq2ia 
 |-  ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
172 165 171 eqtri 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
173 172 a1i 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
174 81 82 34 98 100 114 173 dvmptdiv 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( 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 ) ) ) )
175 79 174 eqtrd 
 |-  ( ph -> ( 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 ) ) ) )
176 175 feq1d 
 |-  ( ph -> ( ( RR _D O ) : ( A (,) B ) --> RR <-> ( 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 ) ) ) : ( A (,) B ) --> RR ) )
177 77 176 mpbird 
 |-  ( ph -> ( RR _D O ) : ( A (,) B ) --> RR )
178 177 175 jca 
 |-  ( 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 ) ) ) ) )
179 178 172 pm3.2i 
 |-  ( ( 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 ) ) ) )