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 ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
72 cosf ⊢ cos : ℂ ⟶ ℂ
73 72 a1i ⊢ ( 𝜑 → cos : ℂ ⟶ ℂ )
74 73 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 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 mulid2d ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → ( 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 ) ) )