Step | Hyp | Ref
| Expression |
1 | | fourierdlem56.a |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((-π[,]π) ∖
{0})) |
2 | 1 | difss2d 4094 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) |
3 | 2 | sselda 3944 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π)) |
4 | | 1ex 11151 |
. . . . . . . 8
⊢ 1 ∈
V |
5 | | ovex 7390 |
. . . . . . . 8
⊢ (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈
V |
6 | 4, 5 | ifex 4536 |
. . . . . . 7
⊢ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ V |
7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ V) |
8 | | fourierdlem56.k |
. . . . . . 7
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
9 | 8 | fvmpt2 6959 |
. . . . . 6
⊢ ((𝑠 ∈ (-π[,]π) ∧
if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ V) →
(𝐾‘𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
10 | 3, 7, 9 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐾‘𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
11 | | fourierdlem56.r4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) |
12 | 11 | neneqd 2948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) |
13 | 12 | iffalsed 4497 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2))))) |
14 | | elioore 13294 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) |
15 | 14 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) |
16 | 15 | recnd 11183 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ) |
17 | 16 | halfcld 12398 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℂ) |
18 | 17 | sincld 16012 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ) |
19 | | 2cnd 12231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) |
20 | | fourierdlem44 44382 |
. . . . . . . 8
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 ≠ 0) →
(sin‘(𝑠 / 2)) ≠
0) |
21 | 3, 11, 20 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0) |
22 | | 2ne0 12257 |
. . . . . . . 8
⊢ 2 ≠
0 |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
24 | 16, 18, 19, 21, 23 | divdiv1d 11962 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝑠 / (sin‘(𝑠 / 2))) / 2) = (𝑠 / ((sin‘(𝑠 / 2)) · 2))) |
25 | 18, 19 | mulcomd 11176 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑠 / 2)) · 2) = (2 ·
(sin‘(𝑠 /
2)))) |
26 | 25 | oveq2d 7373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / ((sin‘(𝑠 / 2)) · 2)) = (𝑠 / (2 · (sin‘(𝑠 / 2))))) |
27 | 24, 26 | eqtr2d 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) = ((𝑠 / (sin‘(𝑠 / 2))) / 2)) |
28 | 10, 13, 27 | 3eqtrd 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐾‘𝑠) = ((𝑠 / (sin‘(𝑠 / 2))) / 2)) |
29 | 28 | mpteq2dva 5205 |
. . 3
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑠 / (sin‘(𝑠 / 2))) / 2))) |
30 | 29 | oveq2d 7373 |
. 2
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑠 / (sin‘(𝑠 / 2))) / 2)))) |
31 | | reelprrecn 11143 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
32 | 31 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
33 | 16, 18, 21 | divcld 11931 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (sin‘(𝑠 / 2))) ∈ ℂ) |
34 | | 1red 11156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) |
35 | 15 | rehalfcld 12400 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ) |
36 | 35 | resincld 16025 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ) |
37 | 34, 36 | remulcld 11185 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 · (sin‘(𝑠 / 2))) ∈
ℝ) |
38 | 35 | recoscld 16026 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℝ) |
39 | 34 | rehalfcld 12400 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈
ℝ) |
40 | 38, 39 | remulcld 11185 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · (1 / 2)) ∈
ℝ) |
41 | 40, 15 | remulcld 11185 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((cos‘(𝑠 / 2)) · (1 / 2)) · 𝑠) ∈
ℝ) |
42 | 37, 41 | resubcld 11583 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) ∈ ℝ) |
43 | 36 | resqcld 14030 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑠 / 2))↑2) ∈
ℝ) |
44 | | 2z 12535 |
. . . . . 6
⊢ 2 ∈
ℤ |
45 | 44 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ) |
46 | 18, 21, 45 | expne0d 14057 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑠 / 2))↑2) ≠ 0) |
47 | 42, 43, 46 | redivcld 11983 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) ∈
ℝ) |
48 | | 1cnd 11150 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
49 | | recn 11141 |
. . . . . 6
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
50 | 49 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℂ) |
51 | | 1red 11156 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → 1 ∈
ℝ) |
52 | 32 | dvmptid 25321 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ ℝ ↦ 𝑠)) = (𝑠 ∈ ℝ ↦ 1)) |
53 | | ioossre 13325 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℝ |
54 | 53 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
55 | | eqid 2736 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
56 | 55 | tgioo2 24166 |
. . . . 5
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
57 | | iooretop 24129 |
. . . . . 6
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
58 | 57 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
59 | 32, 50, 51, 52, 54, 56, 55, 58 | dvmptres 25327 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 1)) |
60 | | elsni 4603 |
. . . . . . 7
⊢
((sin‘(𝑠 / 2))
∈ {0} → (sin‘(𝑠 / 2)) = 0) |
61 | 60 | necon3ai 2968 |
. . . . . 6
⊢
((sin‘(𝑠 / 2))
≠ 0 → ¬ (sin‘(𝑠 / 2)) ∈ {0}) |
62 | 21, 61 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ (sin‘(𝑠 / 2)) ∈
{0}) |
63 | 18, 62 | eldifd 3921 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ (ℂ ∖
{0})) |
64 | 17 | coscld 16013 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ) |
65 | 48 | halfcld 12398 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈
ℂ) |
66 | 64, 65 | mulcld 11175 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · (1 / 2)) ∈
ℂ) |
67 | | cnelprrecn 11144 |
. . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} |
68 | 67 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
69 | | sinf 16006 |
. . . . . . 7
⊢
sin:ℂ⟶ℂ |
70 | 69 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
sin:ℂ⟶ℂ) |
71 | 70 | ffvelcdmda 7035 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) ∈
ℂ) |
72 | | cosf 16007 |
. . . . . . 7
⊢
cos:ℂ⟶ℂ |
73 | 72 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
cos:ℂ⟶ℂ) |
74 | 73 | ffvelcdmda 7035 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈
ℂ) |
75 | | 2cnd 12231 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℂ) |
76 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ≠ 0) |
77 | 32, 16, 34, 59, 75, 76 | dvmptdivc 25329 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 / 2))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 2))) |
78 | | ffn 6668 |
. . . . . . . . . . 11
⊢
(sin:ℂ⟶ℂ → sin Fn ℂ) |
79 | 69, 78 | ax-mp 5 |
. . . . . . . . . 10
⊢ sin Fn
ℂ |
80 | | dffn5 6901 |
. . . . . . . . . 10
⊢ (sin Fn
ℂ ↔ sin = (𝑥
∈ ℂ ↦ (sin‘𝑥))) |
81 | 79, 80 | mpbi 229 |
. . . . . . . . 9
⊢ sin =
(𝑥 ∈ ℂ ↦
(sin‘𝑥)) |
82 | 81 | eqcomi 2745 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ ↦
(sin‘𝑥)) =
sin |
83 | 82 | oveq2i 7368 |
. . . . . . 7
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(sin‘𝑥))) = (ℂ
D sin) |
84 | | dvsin 25346 |
. . . . . . 7
⊢ (ℂ
D sin) = cos |
85 | | ffn 6668 |
. . . . . . . . 9
⊢
(cos:ℂ⟶ℂ → cos Fn ℂ) |
86 | 72, 85 | ax-mp 5 |
. . . . . . . 8
⊢ cos Fn
ℂ |
87 | | dffn5 6901 |
. . . . . . . 8
⊢ (cos Fn
ℂ ↔ cos = (𝑥
∈ ℂ ↦ (cos‘𝑥))) |
88 | 86, 87 | mpbi 229 |
. . . . . . 7
⊢ cos =
(𝑥 ∈ ℂ ↦
(cos‘𝑥)) |
89 | 83, 84, 88 | 3eqtri 2768 |
. . . . . 6
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(sin‘𝑥))) = (𝑥 ∈ ℂ ↦
(cos‘𝑥)) |
90 | 89 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦
(sin‘𝑥))) = (𝑥 ∈ ℂ ↦
(cos‘𝑥))) |
91 | | fveq2 6842 |
. . . . 5
⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2))) |
92 | | fveq2 6842 |
. . . . 5
⊢ (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2))) |
93 | 32, 68, 17, 39, 71, 74, 77, 90, 91, 92 | dvmptco 25336 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑠 / 2)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((cos‘(𝑠 / 2)) · (1 / 2)))) |
94 | 32, 16, 48, 59, 63, 66, 93 | dvmptdiv 25338 |
. . 3
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 / (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)))) |
95 | 32, 33, 47, 94, 75, 76 | dvmptdivc 25329 |
. 2
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑠 / (sin‘(𝑠 / 2))) / 2))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) / 2))) |
96 | 14 | recnd 11183 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ) |
97 | 96 | halfcld 12398 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ) |
98 | 97 | sincld 16012 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ) |
99 | 98 | mulid2d 11173 |
. . . . . . 7
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (1 · (sin‘(𝑠 / 2))) = (sin‘(𝑠 / 2))) |
100 | 97 | coscld 16013 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ) |
101 | | 2cnd 12231 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ) |
102 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ≠ 0) |
103 | 100, 101,
102 | divrecd 11934 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((cos‘(𝑠 / 2)) / 2) = ((cos‘(𝑠 / 2)) · (1 / 2))) |
104 | 103 | eqcomd 2742 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((cos‘(𝑠 / 2)) · (1 / 2)) = ((cos‘(𝑠 / 2)) / 2)) |
105 | 104 | oveq1d 7372 |
. . . . . . 7
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (((cos‘(𝑠 / 2)) · (1 / 2)) · 𝑠) = (((cos‘(𝑠 / 2)) / 2) · 𝑠)) |
106 | 99, 105 | oveq12d 7375 |
. . . . . 6
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) = ((sin‘(𝑠 / 2)) − (((cos‘(𝑠 / 2)) / 2) · 𝑠))) |
107 | 106 | oveq1d 7372 |
. . . . 5
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) = (((sin‘(𝑠 / 2)) −
(((cos‘(𝑠 / 2)) / 2)
· 𝑠)) /
((sin‘(𝑠 /
2))↑2))) |
108 | 107 | oveq1d 7372 |
. . . 4
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) / 2) = ((((sin‘(𝑠 / 2)) −
(((cos‘(𝑠 / 2)) / 2)
· 𝑠)) /
((sin‘(𝑠 /
2))↑2)) / 2)) |
109 | 108 | mpteq2ia 5208 |
. . 3
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((1 · (sin‘(𝑠 / 2))) −
(((cos‘(𝑠 / 2))
· (1 / 2)) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) / 2)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((sin‘(𝑠 / 2)) − (((cos‘(𝑠 / 2)) / 2) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) /
2)) |
110 | 109 | a1i 11 |
. 2
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((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 2780 |
1
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((sin‘(𝑠 / 2)) − (((cos‘(𝑠 / 2)) / 2) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) /
2))) |