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	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
	fourierdlem56.a	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ( - π [,] π ) ∖ { 0 } ) )
	fourierdlem56.r4	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
Assertion	fourierdlem56	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem56.k	⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
2		fourierdlem56.a	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( ( - π [,] π ) ∖ { 0 } ) )
3		fourierdlem56.r4	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ≠ 0 )
4	2	difss2d	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( - π [,] π ) )
5	4	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
6		1ex	⊢ 1 ∈ V
7		ovex	⊢ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ V
8	6 7	ifex	⊢ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ V
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ V )
10	1	fvmpt2	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ V ) → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
11	5 9 10	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
12	3	neneqd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑠 = 0 )
13	12	iffalsed	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
14		elioore	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
16	15	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
17	16	halfcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℂ )
18	17	sincld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
19		2cnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
20		fourierdlem44	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
21	5 3 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
22		2ne0	⊢ 2 ≠ 0
23	22	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
24	16 18 19 21 23	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) = ( 𝑠 / ( ( sin ‘ ( 𝑠 / 2 ) ) · 2 ) ) )
25	18 19	mulcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( sin ‘ ( 𝑠 / 2 ) ) · 2 ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
26	25	oveq2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / ( ( sin ‘ ( 𝑠 / 2 ) ) · 2 ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
27	24 26	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) )
28	11 13 27	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐾 ‘ 𝑠 ) = ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) )
29	28	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐾 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) ) )
30	29	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐾 ‘ 𝑠 ) ) ) = ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) ) ) )
31		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
32	31	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
33	16 18 21	divcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
34		1red	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
35	15	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℝ )
36	35	resincld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
37	34 36	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
38	35	recoscld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
39	34	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 2 ) ∈ ℝ )
40	38 39	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) ∈ ℝ )
41	40 15	remulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ∈ ℝ )
42	37 41	resubcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) ∈ ℝ )
43	36	resqcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ∈ ℝ )
44		2z	⊢ 2 ∈ ℤ
45	44	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℤ )
46	18 21 45	expne0d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ≠ 0 )
47	42 43 46	redivcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) ∈ ℝ )
48		1cnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℂ )
49		recn	⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
50	49	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 𝑠 ∈ ℂ )
51		1red	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → 1 ∈ ℝ )
52	32	dvmptid	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ℝ ↦ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ 1 ) )
53		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
54	53	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
55		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
56	55	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
57		iooretop	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
58	57	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
59	32 50 51 52 54 56 55 58	dvmptres	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
60		elsni	⊢ ( ( sin ‘ ( 𝑠 / 2 ) ) ∈ { 0 } → ( sin ‘ ( 𝑠 / 2 ) ) = 0 )
61	60	necon3ai	⊢ ( ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 → ¬ ( sin ‘ ( 𝑠 / 2 ) ) ∈ { 0 } )
62	21 61	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ ( sin ‘ ( 𝑠 / 2 ) ) ∈ { 0 } )
63	18 62	eldifd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ( ℂ ∖ { 0 } ) )
64	17	coscld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
65	48	halfcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 2 ) ∈ ℂ )
66	64 65	mulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) ∈ ℂ )
67		cnelprrecn	⊢ ℂ ∈ { ℝ , ℂ }
68	67	a1i	⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
69		sinf	⊢ sin : ℂ ⟶ ℂ
70	69	a1i	⊢ ( 𝜑 → sin : ℂ ⟶ ℂ )
71	70	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
72		cosf	⊢ cos : ℂ ⟶ ℂ
73	72	a1i	⊢ ( 𝜑 → cos : ℂ ⟶ ℂ )
74	73	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ ℂ )
75		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
76	22	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
77	32 16 34 59 75 76	dvmptdivc	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑠 / 2 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 2 ) ) )
78		ffn	⊢ ( sin : ℂ ⟶ ℂ → sin Fn ℂ )
79	69 78	ax-mp	⊢ sin Fn ℂ
80		dffn5	⊢ ( sin Fn ℂ ↔ sin = ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) )
81	79 80	mpbi	⊢ sin = ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) )
82	81	eqcomi	⊢ ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) = sin
83	82	oveq2i	⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( ℂ D sin )
84		dvsin	⊢ ( ℂ D sin ) = cos
85		ffn	⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
86	72 85	ax-mp	⊢ cos Fn ℂ
87		dffn5	⊢ ( cos Fn ℂ ↔ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
88	86 87	mpbi	⊢ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) )
89	83 84 88	3eqtri	⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) )
90	89	a1i	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
91		fveq2	⊢ ( 𝑥 = ( 𝑠 / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( 𝑠 / 2 ) ) )
92		fveq2	⊢ ( 𝑥 = ( 𝑠 / 2 ) → ( cos ‘ 𝑥 ) = ( cos ‘ ( 𝑠 / 2 ) ) )
93	32 68 17 39 71 74 77 90 91 92	dvmptco	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) ) )
94	32 16 48 59 63 66 93	dvmptdiv	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) ) )
95	32 33 47 94 75 76	dvmptdivc	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝑠 / ( sin ‘ ( 𝑠 / 2 ) ) ) / 2 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) )
96	14	recnd	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℂ )
97	96	halfcld	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑠 / 2 ) ∈ ℂ )
98	97	sincld	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
99	98	mullidd	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
100	97	coscld	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
101		2cnd	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 2 ∈ ℂ )
102	22	a1i	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 2 ≠ 0 )
103	100 101 102	divrecd	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) = ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) )
104	103	eqcomd	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) = ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) )
105	104	oveq1d	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) = ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) )
106	99 105	oveq12d	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) = ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) )
107	106	oveq1d	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) = ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) )
108	107	oveq1d	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) = ( ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) )
109	108	mpteq2ia	⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) )
110	109	a1i	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 1 · ( sin ‘ ( 𝑠 / 2 ) ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) · ( 1 / 2 ) ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) )
111	30 95 110	3eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( sin ‘ ( 𝑠 / 2 ) ) − ( ( ( cos ‘ ( 𝑠 / 2 ) ) / 2 ) · 𝑠 ) ) / ( ( sin ‘ ( 𝑠 / 2 ) ) ↑ 2 ) ) / 2 ) ) )