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 ) ) )