This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
56 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
57 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
58 57 a1i 
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
59 32 50 51 52 54 55 56 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 ffvelcdmda 
 |-  ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC )
72 cosf 
 |-  cos : CC --> CC
73 72 a1i 
 |-  ( ph -> cos : CC --> CC )
74 73 ffvelcdmda 
 |-  ( ( 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 mullidd 
 |-  ( 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 ) ) )