Metamath Proof Explorer


Theorem fourierdlem56

Description: Derivative of the K function on an interval not containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem56.k
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem56.a
|- ( ph -> ( A (,) B ) C_ ( ( -u _pi [,] _pi ) \ { 0 } ) )
fourierdlem56.r4
|- ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
Assertion fourierdlem56
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( K ` s ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem56.k
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
2 fourierdlem56.a
 |-  ( ph -> ( A (,) B ) C_ ( ( -u _pi [,] _pi ) \ { 0 } ) )
3 fourierdlem56.r4
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
4 2 difss2d
 |-  ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) )
5 4 sselda
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) )
6 1ex
 |-  1 e. _V
7 ovex
 |-  ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. _V
8 6 7 ifex
 |-  if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V
9 8 a1i
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V )
10 1 fvmpt2
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
11 5 9 10 syl2anc
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
12 3 neneqd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
13 12 iffalsed
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
14 elioore
 |-  ( s e. ( A (,) B ) -> s e. RR )
15 14 adantl
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
16 15 recnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
17 16 halfcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. CC )
18 17 sincld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC )
19 2cnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC )
20 fourierdlem44
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
21 5 3 20 syl2anc
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
22 2ne0
 |-  2 =/= 0
23 22 a1i
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 )
24 16 18 19 21 23 divdiv1d
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) = ( s / ( ( sin ` ( s / 2 ) ) x. 2 ) ) )
25 18 19 mulcomd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) x. 2 ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
26 25 oveq2d
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( ( sin ` ( s / 2 ) ) x. 2 ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
27 24 26 eqtr2d
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) )
28 11 13 27 3eqtrd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) )
29 28 mpteq2dva
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( K ` s ) ) = ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) )
30 29 oveq2d
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( K ` s ) ) ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) ) )
31 reelprrecn
 |-  RR e. { RR , CC }
32 31 a1i
 |-  ( ph -> RR e. { RR , CC } )
33 16 18 21 divcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( sin ` ( s / 2 ) ) ) e. CC )
34 1red
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. RR )
35 15 rehalfcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR )
36 35 resincld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR )
37 34 36 remulcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 x. ( sin ` ( s / 2 ) ) ) e. RR )
38 35 recoscld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. RR )
39 34 rehalfcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / 2 ) e. RR )
40 38 39 remulcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) e. RR )
41 40 15 remulcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) e. RR )
42 37 41 resubcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) e. RR )
43 36 resqcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) ^ 2 ) e. RR )
44 2z
 |-  2 e. ZZ
45 44 a1i
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. ZZ )
46 18 21 45 expne0d
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) ^ 2 ) =/= 0 )
47 42 43 46 redivcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) e. RR )
48 1cnd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. CC )
49 recn
 |-  ( s e. RR -> s e. CC )
50 49 adantl
 |-  ( ( ph /\ s e. RR ) -> s e. CC )
51 1red
 |-  ( ( ph /\ s e. RR ) -> 1 e. RR )
52 32 dvmptid
 |-  ( ph -> ( RR _D ( s e. RR |-> s ) ) = ( s e. RR |-> 1 ) )
53 ioossre
 |-  ( A (,) B ) C_ RR
54 53 a1i
 |-  ( ph -> ( A (,) B ) C_ RR )
55 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
56 55 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
57 iooretop
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
58 57 a1i
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
59 32 50 51 52 54 56 55 58 dvmptres
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) )
60 elsni
 |-  ( ( sin ` ( s / 2 ) ) e. { 0 } -> ( sin ` ( s / 2 ) ) = 0 )
61 60 necon3ai
 |-  ( ( sin ` ( s / 2 ) ) =/= 0 -> -. ( sin ` ( s / 2 ) ) e. { 0 } )
62 21 61 syl
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. ( sin ` ( s / 2 ) ) e. { 0 } )
63 18 62 eldifd
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
64 17 coscld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC )
65 48 halfcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / 2 ) e. CC )
66 64 65 mulcld
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) e. CC )
67 cnelprrecn
 |-  CC e. { RR , CC }
68 67 a1i
 |-  ( ph -> CC e. { RR , CC } )
69 sinf
 |-  sin : CC --> CC
70 69 a1i
 |-  ( ph -> sin : CC --> CC )
71 70 ffvelrnda
 |-  ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC )
72 cosf
 |-  cos : CC --> CC
73 72 a1i
 |-  ( ph -> cos : CC --> CC )
74 73 ffvelrnda
 |-  ( ( ph /\ x e. CC ) -> ( cos ` x ) e. CC )
75 2cnd
 |-  ( ph -> 2 e. CC )
76 22 a1i
 |-  ( ph -> 2 =/= 0 )
77 32 16 34 59 75 76 dvmptdivc
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( s / 2 ) ) ) = ( s e. ( A (,) B ) |-> ( 1 / 2 ) ) )
78 ffn
 |-  ( sin : CC --> CC -> sin Fn CC )
79 69 78 ax-mp
 |-  sin Fn CC
80 dffn5
 |-  ( sin Fn CC <-> sin = ( x e. CC |-> ( sin ` x ) ) )
81 79 80 mpbi
 |-  sin = ( x e. CC |-> ( sin ` x ) )
82 81 eqcomi
 |-  ( x e. CC |-> ( sin ` x ) ) = sin
83 82 oveq2i
 |-  ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( CC _D sin )
84 dvsin
 |-  ( CC _D sin ) = cos
85 ffn
 |-  ( cos : CC --> CC -> cos Fn CC )
86 72 85 ax-mp
 |-  cos Fn CC
87 dffn5
 |-  ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) )
88 86 87 mpbi
 |-  cos = ( x e. CC |-> ( cos ` x ) )
89 83 84 88 3eqtri
 |-  ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) )
90 89 a1i
 |-  ( ph -> ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) )
91 fveq2
 |-  ( x = ( s / 2 ) -> ( sin ` x ) = ( sin ` ( s / 2 ) ) )
92 fveq2
 |-  ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) )
93 32 68 17 39 71 74 77 90 91 92 dvmptco
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( sin ` ( s / 2 ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) ) )
94 32 16 48 59 63 66 93 dvmptdiv
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( s / ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) ) )
95 32 33 47 94 75 76 dvmptdivc
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) )
96 14 recnd
 |-  ( s e. ( A (,) B ) -> s e. CC )
97 96 halfcld
 |-  ( s e. ( A (,) B ) -> ( s / 2 ) e. CC )
98 97 sincld
 |-  ( s e. ( A (,) B ) -> ( sin ` ( s / 2 ) ) e. CC )
99 98 mulid2d
 |-  ( s e. ( A (,) B ) -> ( 1 x. ( sin ` ( s / 2 ) ) ) = ( sin ` ( s / 2 ) ) )
100 97 coscld
 |-  ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC )
101 2cnd
 |-  ( s e. ( A (,) B ) -> 2 e. CC )
102 22 a1i
 |-  ( s e. ( A (,) B ) -> 2 =/= 0 )
103 100 101 102 divrecd
 |-  ( s e. ( A (,) B ) -> ( ( cos ` ( s / 2 ) ) / 2 ) = ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) )
104 103 eqcomd
 |-  ( s e. ( A (,) B ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) = ( ( cos ` ( s / 2 ) ) / 2 ) )
105 104 oveq1d
 |-  ( s e. ( A (,) B ) -> ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) = ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) )
106 99 105 oveq12d
 |-  ( s e. ( A (,) B ) -> ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) = ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) )
107 106 oveq1d
 |-  ( s e. ( A (,) B ) -> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) = ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) )
108 107 oveq1d
 |-  ( s e. ( A (,) B ) -> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) = ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) )
109 108 mpteq2ia
 |-  ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) )
110 109 a1i
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) )
111 30 95 110 3eqtrd
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( K ` s ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) )