This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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