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 bilani 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 = s )
62 simpl 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> s e. ( A (,) B ) )
63 61 62 eqeltrd 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
64 63 adantll 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
65 7 ad2antrr 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) )
66 64 65 pm2.65da 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
67 66 neqned 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
68 fourierdlem44 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
69 59 67 68 syl2anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
70 55 56 58 69 mulne0d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
71 2z 
 |-  2 e. ZZ
72 71 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. ZZ )
73 54 70 72 expne0d 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) ^ 2 ) =/= 0 )
74 48 49 73 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 )
75 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 ) ) )
76 74 75 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 )
77 9 a1i 
 |-  ( ph -> O = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
78 77 oveq2d 
 |-  ( ph -> ( RR _D O ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
79 reelprrecn 
 |-  RR e. { RR , CC }
80 79 a1i 
 |-  ( ph -> RR e. { RR , CC } )
81 46 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
82 44 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
83 eqid 
 |-  ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
84 1 2 3 4 83 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 ) ) ) )
85 45 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
86 0red 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
87 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
88 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
89 87 88 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
90 89 a1i 
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
91 8 recnd 
 |-  ( ph -> C e. CC )
92 80 90 91 dvmptconst 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
93 80 82 34 84 85 86 92 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 ) ) )
94 34 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) e. CC )
95 94 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 ) ) )
96 95 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 ) ) ) )
97 93 96 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 ) ) ) )
98 eldifsn 
 |-  ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) <-> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC /\ ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 ) )
99 54 70 98 sylanbrc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
100 recn 
 |-  ( s e. RR -> s e. CC )
101 57 a1i 
 |-  ( s e. RR -> 2 =/= 0 )
102 100 50 101 divrec2d 
 |-  ( s e. RR -> ( s / 2 ) = ( ( 1 / 2 ) x. s ) )
103 102 eqcomd 
 |-  ( s e. RR -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
104 18 103 syl 
 |-  ( s e. ( A (,) B ) -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
105 104 fveq2d 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) = ( cos ` ( s / 2 ) ) )
106 halfcn 
 |-  ( 1 / 2 ) e. CC
107 106 a1i 
 |-  ( s e. CC -> ( 1 / 2 ) e. CC )
108 id 
 |-  ( s e. CC -> s e. CC )
109 107 108 mulcld 
 |-  ( s e. CC -> ( ( 1 / 2 ) x. s ) e. CC )
110 109 coscld 
 |-  ( s e. CC -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
111 18 100 110 3syl 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( ( 1 / 2 ) x. s ) ) e. CC )
112 105 111 eqeltrrd 
 |-  ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
113 112 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
114 ioossre 
 |-  ( A (,) B ) C_ RR
115 resmpt 
 |-  ( ( A (,) B ) C_ RR -> ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
116 114 115 ax-mp 
 |-  ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) = ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
117 116 eqcomi 
 |-  ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) )
118 117 oveq2i 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` ( A (,) B ) ) )
119 ax-resscn 
 |-  RR C_ CC
120 eqid 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
121 120 53 fmpti 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC
122 ssid 
 |-  RR C_ RR
123 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
124 123 88 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 ) ) ) )
125 119 121 122 114 124 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 ) ) )
126 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 ) ) ) ) )
127 119 126 ax-mp 
 |-  ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
128 103 fveq2d 
 |-  ( s e. RR -> ( sin ` ( ( 1 / 2 ) x. s ) ) = ( sin ` ( s / 2 ) ) )
129 128 oveq2d 
 |-  ( s e. RR -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
130 129 mpteq2ia 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
131 127 130 eqtr2i 
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
132 131 oveq2i 
 |-  ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) )
133 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
134 132 133 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 ) )
135 eqid 
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
136 2cnd 
 |-  ( s e. CC -> 2 e. CC )
137 109 sincld 
 |-  ( s e. CC -> ( sin ` ( ( 1 / 2 ) x. s ) ) e. CC )
138 136 137 mulcld 
 |-  ( s e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
139 135 138 fmpti 
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC
140 ssid 
 |-  CC C_ CC
141 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 )
142 2cn 
 |-  2 e. CC
143 142 106 mulcli 
 |-  ( 2 x. ( 1 / 2 ) ) e. CC
144 143 a1i 
 |-  ( s e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
145 144 110 mulcld 
 |-  ( s e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
146 141 145 mprg 
 |-  dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = CC
147 119 146 sseqtrri 
 |-  RR C_ dom ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
148 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 ) ) ) ) )
149 142 106 148 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 ) ) ) )
150 149 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 ) ) ) )
151 147 150 sseqtrri 
 |-  RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
152 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 ) )
153 79 139 140 151 152 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 )
154 153 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 ) )
155 149 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 )
156 155 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 ) )
157 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 ) ) )
158 114 157 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 ) )
159 ioosscn 
 |-  ( A (,) B ) C_ CC
160 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 ) ) ) ) )
161 159 160 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 ) ) ) )
162 156 158 161 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 ) ) ) )
163 134 154 162 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 ) ) ) )
164 118 125 163 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 ) ) ) )
165 142 57 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
166 165 oveq1i 
 |-  ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) )
167 166 a1i 
 |-  ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
168 111 mullidd 
 |-  ( s e. ( A (,) B ) -> ( 1 x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( ( 1 / 2 ) x. s ) ) )
169 167 168 105 3eqtrd 
 |-  ( s e. ( A (,) B ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( s / 2 ) ) )
170 169 mpteq2ia 
 |-  ( s e. ( A (,) B ) |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
171 164 170 eqtri 
 |-  ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) )
172 171 a1i 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( cos ` ( s / 2 ) ) ) )
173 80 81 34 97 99 113 172 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 ) ) ) )
174 78 173 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 ) ) ) )
175 174 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 ) )
176 76 175 mpbird 
 |-  ( ph -> ( RR _D O ) : ( A (,) B ) --> RR )
177 176 174 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 ) ) ) ) )
178 177 171 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 ) ) ) )