Metamath Proof Explorer


Theorem fourierdlem58

Description: The derivative of K is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem58.k 𝐾 = ( 𝑠𝐴 ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
fourierdlem58.ass ( 𝜑𝐴 ⊆ ( - π [,] π ) )
fourierdlem58.0nA ( 𝜑 → ¬ 0 ∈ 𝐴 )
fourierdlem58.4 ( 𝜑𝐴 ∈ ( topGen ‘ ran (,) ) )
Assertion fourierdlem58 ( 𝜑 → ( ℝ D 𝐾 ) ∈ ( 𝐴cn→ ℝ ) )

Proof

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