Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem58.k |
⊢ 𝐾 = ( 𝑠 ∈ 𝐴 ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) |
2 |
|
fourierdlem58.ass |
⊢ ( 𝜑 → 𝐴 ⊆ ( - π [,] π ) ) |
3 |
|
fourierdlem58.0nA |
⊢ ( 𝜑 → ¬ 0 ∈ 𝐴 ) |
4 |
|
fourierdlem58.4 |
⊢ ( 𝜑 → 𝐴 ∈ ( topGen ‘ ran (,) ) ) |
5 |
|
pire |
⊢ π ∈ ℝ |
6 |
5
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → π ∈ ℝ ) |
7 |
6
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → - π ∈ ℝ ) |
8 |
7 6
|
iccssred |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( - π [,] π ) ⊆ ℝ ) |
9 |
2
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( - π [,] π ) ) |
10 |
8 9
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ ) |
11 |
|
2re |
⊢ 2 ∈ ℝ |
12 |
11
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℝ ) |
13 |
10
|
rehalfcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / 2 ) ∈ ℝ ) |
14 |
13
|
resincld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ ) |
15 |
12 14
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ ) |
16 |
|
2cnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ∈ ℂ ) |
17 |
10
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℂ ) |
18 |
17
|
halfcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / 2 ) ∈ ℂ ) |
19 |
18
|
sincld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ ) |
20 |
|
2ne0 |
⊢ 2 ≠ 0 |
21 |
20
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 2 ≠ 0 ) |
22 |
|
eqcom |
⊢ ( 𝑠 = 0 ↔ 0 = 𝑠 ) |
23 |
22
|
biimpi |
⊢ ( 𝑠 = 0 → 0 = 𝑠 ) |
24 |
23
|
adantl |
⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝑠 = 0 ) → 0 = 𝑠 ) |
25 |
|
simpl |
⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝑠 = 0 ) → 𝑠 ∈ 𝐴 ) |
26 |
24 25
|
eqeltrd |
⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝑠 = 0 ) → 0 ∈ 𝐴 ) |
27 |
26
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑠 = 0 ) → 0 ∈ 𝐴 ) |
28 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ 𝐴 ) |
29 |
27 28
|
pm2.65da |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ 𝑠 = 0 ) |
30 |
29
|
neqned |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 0 ) |
31 |
|
fourierdlem44 |
⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 ) |
32 |
9 30 31
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 ) |
33 |
16 19 21 32
|
mulne0d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 ) |
34 |
10 15 33
|
redivcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℝ ) |
35 |
34 1
|
fmptd |
⊢ ( 𝜑 → 𝐾 : 𝐴 ⟶ ℝ ) |
36 |
5
|
a1i |
⊢ ( 𝜑 → π ∈ ℝ ) |
37 |
36
|
renegcld |
⊢ ( 𝜑 → - π ∈ ℝ ) |
38 |
37 36
|
iccssred |
⊢ ( 𝜑 → ( - π [,] π ) ⊆ ℝ ) |
39 |
2 38
|
sstrd |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
40 |
|
dvfre |
⊢ ( ( 𝐾 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ℝ D 𝐾 ) : dom ( ℝ D 𝐾 ) ⟶ ℝ ) |
41 |
35 39 40
|
syl2anc |
⊢ ( 𝜑 → ( ℝ D 𝐾 ) : dom ( ℝ D 𝐾 ) ⟶ ℝ ) |
42 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ) |
43 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) |
44 |
4 10 15 42 43
|
offval2 |
⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ∘f / ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) |
45 |
1 44
|
eqtr4id |
⊢ ( 𝜑 → 𝐾 = ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ∘f / ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) |
46 |
45
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D 𝐾 ) = ( ℝ D ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ∘f / ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ) |
47 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
48 |
47
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
49 |
|
eqid |
⊢ ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) |
50 |
17 49
|
fmptd |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) : 𝐴 ⟶ ℂ ) |
51 |
16 19
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ ) |
52 |
33
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) |
53 |
|
elsng |
⊢ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) ) |
54 |
15 53
|
syl |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) ) |
55 |
52 54
|
mtbird |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ) |
56 |
51 55
|
eldifd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) ) |
57 |
|
eqid |
⊢ ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) |
58 |
56 57
|
fmptd |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) |
59 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
60 |
59
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
61 |
4 60
|
eleqtrdi |
⊢ ( 𝜑 → 𝐴 ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
62 |
48 61
|
dvmptidg |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ) = ( 𝑠 ∈ 𝐴 ↦ 1 ) ) |
63 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
64 |
63
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
65 |
39 64
|
sstrd |
⊢ ( 𝜑 → 𝐴 ⊆ ℂ ) |
66 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
67 |
|
ssid |
⊢ ℂ ⊆ ℂ |
68 |
67
|
a1i |
⊢ ( 𝜑 → ℂ ⊆ ℂ ) |
69 |
65 66 68
|
constcncfg |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ 1 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
70 |
62 69
|
eqeltrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
71 |
39
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ 𝐴 ) = ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) |
72 |
71
|
eqcomd |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ 𝐴 ) ) |
73 |
72
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ 𝐴 ) ) ) |
74 |
|
eqid |
⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) |
75 |
|
2cnd |
⊢ ( 𝑠 ∈ ℝ → 2 ∈ ℂ ) |
76 |
|
recn |
⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ ) |
77 |
76
|
halfcld |
⊢ ( 𝑠 ∈ ℝ → ( 𝑠 / 2 ) ∈ ℂ ) |
78 |
77
|
sincld |
⊢ ( 𝑠 ∈ ℝ → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ ) |
79 |
75 78
|
mulcld |
⊢ ( 𝑠 ∈ ℝ → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ ) |
80 |
74 79
|
fmpti |
⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ |
81 |
80
|
a1i |
⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ ) |
82 |
|
ssid |
⊢ ℝ ⊆ ℝ |
83 |
82
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℝ ) |
84 |
59 60
|
dvres |
⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ 𝐴 ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ) ) |
85 |
64 81 83 39 84
|
syl22anc |
⊢ ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ↾ 𝐴 ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ) ) |
86 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
87 |
86
|
a1i |
⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top ) |
88 |
|
uniretop |
⊢ ℝ = ∪ ( topGen ‘ ran (,) ) |
89 |
88
|
isopn3 |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ⊆ ℝ ) → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 ) ) |
90 |
87 39 89
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 ) ) |
91 |
4 90
|
mpbid |
⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 ) |
92 |
91
|
reseq2d |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ) = ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ 𝐴 ) ) |
93 |
|
resmpt |
⊢ ( ℝ ⊆ ℂ → ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) |
94 |
63 93
|
ax-mp |
⊢ ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) |
95 |
|
id |
⊢ ( 𝑠 ∈ ℂ → 𝑠 ∈ ℂ ) |
96 |
|
2cnd |
⊢ ( 𝑠 ∈ ℂ → 2 ∈ ℂ ) |
97 |
20
|
a1i |
⊢ ( 𝑠 ∈ ℂ → 2 ≠ 0 ) |
98 |
95 96 97
|
divrec2d |
⊢ ( 𝑠 ∈ ℂ → ( 𝑠 / 2 ) = ( ( 1 / 2 ) · 𝑠 ) ) |
99 |
98
|
eqcomd |
⊢ ( 𝑠 ∈ ℂ → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) ) |
100 |
76 99
|
syl |
⊢ ( 𝑠 ∈ ℝ → ( ( 1 / 2 ) · 𝑠 ) = ( 𝑠 / 2 ) ) |
101 |
100
|
fveq2d |
⊢ ( 𝑠 ∈ ℝ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) ) |
102 |
101
|
oveq2d |
⊢ ( 𝑠 ∈ ℝ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) |
103 |
102
|
mpteq2ia |
⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) |
104 |
94 103
|
eqtr2i |
⊢ ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) |
105 |
104
|
oveq2i |
⊢ ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) |
106 |
|
eqid |
⊢ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) |
107 |
|
halfcn |
⊢ ( 1 / 2 ) ∈ ℂ |
108 |
107
|
a1i |
⊢ ( 𝑠 ∈ ℂ → ( 1 / 2 ) ∈ ℂ ) |
109 |
108 95
|
mulcld |
⊢ ( 𝑠 ∈ ℂ → ( ( 1 / 2 ) · 𝑠 ) ∈ ℂ ) |
110 |
109
|
sincld |
⊢ ( 𝑠 ∈ ℂ → ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ∈ ℂ ) |
111 |
96 110
|
mulcld |
⊢ ( 𝑠 ∈ ℂ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ∈ ℂ ) |
112 |
106 111
|
fmpti |
⊢ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ |
113 |
|
2cn |
⊢ 2 ∈ ℂ |
114 |
|
dvasinbx |
⊢ ( ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) |
115 |
113 107 114
|
mp2an |
⊢ ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) |
116 |
113 20
|
recidi |
⊢ ( 2 · ( 1 / 2 ) ) = 1 |
117 |
116
|
a1i |
⊢ ( 𝑠 ∈ ℂ → ( 2 · ( 1 / 2 ) ) = 1 ) |
118 |
99
|
fveq2d |
⊢ ( 𝑠 ∈ ℂ → ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) = ( cos ‘ ( 𝑠 / 2 ) ) ) |
119 |
117 118
|
oveq12d |
⊢ ( 𝑠 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( 1 · ( cos ‘ ( 𝑠 / 2 ) ) ) ) |
120 |
|
halfcl |
⊢ ( 𝑠 ∈ ℂ → ( 𝑠 / 2 ) ∈ ℂ ) |
121 |
120
|
coscld |
⊢ ( 𝑠 ∈ ℂ → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ ) |
122 |
121
|
mulid2d |
⊢ ( 𝑠 ∈ ℂ → ( 1 · ( cos ‘ ( 𝑠 / 2 ) ) ) = ( cos ‘ ( 𝑠 / 2 ) ) ) |
123 |
119 122
|
eqtrd |
⊢ ( 𝑠 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) = ( cos ‘ ( 𝑠 / 2 ) ) ) |
124 |
123
|
mpteq2ia |
⊢ ( 𝑠 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) |
125 |
115 124
|
eqtri |
⊢ ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) |
126 |
125
|
dmeqi |
⊢ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = dom ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) |
127 |
|
dmmptg |
⊢ ( ∀ 𝑠 ∈ ℂ ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ → dom ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) = ℂ ) |
128 |
127 121
|
mprg |
⊢ dom ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) = ℂ |
129 |
126 128
|
eqtri |
⊢ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) = ℂ |
130 |
63 129
|
sseqtrri |
⊢ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) |
131 |
|
dvres3 |
⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ) ) → ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) ) |
132 |
47 112 67 130 131
|
mp4an |
⊢ ( ℝ D ( ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) |
133 |
125
|
reseq1i |
⊢ ( ( ℂ D ( 𝑠 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑠 ) ) ) ) ) ↾ ℝ ) = ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) |
134 |
105 132 133
|
3eqtri |
⊢ ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) |
135 |
134
|
reseq1i |
⊢ ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ 𝐴 ) = ( ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) ↾ 𝐴 ) |
136 |
135
|
a1i |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ 𝐴 ) = ( ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) ↾ 𝐴 ) ) |
137 |
39
|
resabs1d |
⊢ ( 𝜑 → ( ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) ↾ 𝐴 ) = ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ 𝐴 ) ) |
138 |
65
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ 𝐴 ) = ( 𝑠 ∈ 𝐴 ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ) |
139 |
137 138
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑠 ∈ ℂ ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ↾ ℝ ) ↾ 𝐴 ) = ( 𝑠 ∈ 𝐴 ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ) |
140 |
92 136 139
|
3eqtrd |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑠 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ) |
141 |
73 85 140
|
3eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ 𝐴 ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ) |
142 |
|
coscn |
⊢ cos ∈ ( ℂ –cn→ ℂ ) |
143 |
142
|
a1i |
⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) ) |
144 |
65 68
|
idcncfg |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
145 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
146 |
20
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
147 |
|
eldifsn |
⊢ ( 2 ∈ ( ℂ ∖ { 0 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) |
148 |
145 146 147
|
sylanbrc |
⊢ ( 𝜑 → 2 ∈ ( ℂ ∖ { 0 } ) ) |
149 |
|
difssd |
⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ ) |
150 |
65 148 149
|
constcncfg |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ 2 ) ∈ ( 𝐴 –cn→ ( ℂ ∖ { 0 } ) ) ) |
151 |
144 150
|
divcncf |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 𝑠 / 2 ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
152 |
143 151
|
cncfmpt1f |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
153 |
141 152
|
eqeltrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
154 |
48 50 58 70 153
|
dvdivcncf |
⊢ ( 𝜑 → ( ℝ D ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) ∘f / ( 𝑠 ∈ 𝐴 ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ∈ ( 𝐴 –cn→ ℂ ) ) |
155 |
46 154
|
eqeltrd |
⊢ ( 𝜑 → ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℂ ) ) |
156 |
|
cncff |
⊢ ( ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℂ ) → ( ℝ D 𝐾 ) : 𝐴 ⟶ ℂ ) |
157 |
|
fdm |
⊢ ( ( ℝ D 𝐾 ) : 𝐴 ⟶ ℂ → dom ( ℝ D 𝐾 ) = 𝐴 ) |
158 |
155 156 157
|
3syl |
⊢ ( 𝜑 → dom ( ℝ D 𝐾 ) = 𝐴 ) |
159 |
158
|
feq2d |
⊢ ( 𝜑 → ( ( ℝ D 𝐾 ) : dom ( ℝ D 𝐾 ) ⟶ ℝ ↔ ( ℝ D 𝐾 ) : 𝐴 ⟶ ℝ ) ) |
160 |
41 159
|
mpbid |
⊢ ( 𝜑 → ( ℝ D 𝐾 ) : 𝐴 ⟶ ℝ ) |
161 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℂ ) ) → ( ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℝ ) ↔ ( ℝ D 𝐾 ) : 𝐴 ⟶ ℝ ) ) |
162 |
64 155 161
|
syl2anc |
⊢ ( 𝜑 → ( ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℝ ) ↔ ( ℝ D 𝐾 ) : 𝐴 ⟶ ℝ ) ) |
163 |
160 162
|
mpbird |
⊢ ( 𝜑 → ( ℝ D 𝐾 ) ∈ ( 𝐴 –cn→ ℝ ) ) |