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

Metamath Proof Explorer

Theorem fourierdlem62

Description: The function K is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem62.k ⊢ 𝐾 = ( 𝑦 ∈ ( - π [,] π ) ↦ if ( 𝑦 = 0 , 1 , ( 𝑦 / ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
Assertion fourierdlem62 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ )

Proof

Step Hyp Ref Expression
1 fourierdlem62.k ⊢ 𝐾 = ( 𝑦 ∈ ( - π [,] π ) ↦ if ( 𝑦 = 0 , 1 , ( 𝑦 / ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
2 eqeq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 = 0 ↔ 𝑠 = 0 ) )
3 id ⊢ ( 𝑦 = 𝑠 → 𝑦 = 𝑠 )
4 oveq1 ⊢ ( 𝑦 = 𝑠 → ( 𝑦 / 2 ) = ( 𝑠 / 2 ) )
5 4 fveq2d ⊢ ( 𝑦 = 𝑠 → ( sin ‘ ( 𝑦 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
6 5 oveq2d ⊢ ( 𝑦 = 𝑠 → ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
7 3 6 oveq12d ⊢ ( 𝑦 = 𝑠 → ( 𝑦 / ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
8 2 7 ifbieq2d ⊢ ( 𝑦 = 𝑠 → if ( 𝑦 = 0 , 1 , ( 𝑦 / ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) = if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
9 8 cbvmptv ⊢ ( 𝑦 ∈ ( - π [,] π ) ↦ if ( 𝑦 = 0 , 1 , ( 𝑦 / ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
10 1 9 eqtri ⊢ 𝐾 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
11 10 fourierdlem43 ⊢ 𝐾 : ( - π [,] π ) ⟶ ℝ
12 ax-resscn ⊢ ℝ ⊆ ℂ
13 fss ⊢ ( ( 𝐾 : ( - π [,] π ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐾 : ( - π [,] π ) ⟶ ℂ )
14 11 12 13 mp2an ⊢ 𝐾 : ( - π [,] π ) ⟶ ℂ
15 14 a1i ⊢ ( 𝑠 = 0 → 𝐾 : ( - π [,] π ) ⟶ ℂ )
16 difss ⊢ ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( - π (,) π )
17 elioore ⊢ ( 𝑠 ∈ ( - π (,) π ) → 𝑠 ∈ ℝ )
18 17 ssriv ⊢ ( - π (,) π ) ⊆ ℝ
19 16 18 sstri ⊢ ( ( - π (,) π ) ∖ { 0 } ) ⊆ ℝ
20 19 a1i ⊢ ( ⊤ → ( ( - π (,) π ) ∖ { 0 } ) ⊆ ℝ )
21 eqid ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 )
22 19 sseli ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑥 ∈ ℝ )
23 21 22 fmpti ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) : ( ( - π (,) π ) ∖ { 0 } ) ⟶ ℝ
24 23 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) : ( ( - π (,) π ) ∖ { 0 } ) ⟶ ℝ )
25 eqid ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) )
26 2re ⊢ 2 ∈ ℝ
27 26 a1i ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℝ )
28 22 rehalfcld ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 / 2 ) ∈ ℝ )
29 28 resincld ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( sin ‘ ( 𝑥 / 2 ) ) ∈ ℝ )
30 27 29 remulcld ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℝ )
31 25 30 fmpti ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( ( - π (,) π ) ∖ { 0 } ) ⟶ ℝ
32 31 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( ( - π (,) π ) ∖ { 0 } ) ⟶ ℝ )
33 iooretop ⊢ ( - π (,) π ) ∈ ( topGen ‘ ran (,) )
34 33 a1i ⊢ ( ⊤ → ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) )
35 0re ⊢ 0 ∈ ℝ
36 negpilt0 ⊢ - π < 0
37 pipos ⊢ 0 < π
38 pire ⊢ π ∈ ℝ
39 38 renegcli ⊢ - π ∈ ℝ
40 39 rexri ⊢ - π ∈ ℝ*
41 38 rexri ⊢ π ∈ ℝ*
42 elioo2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( 0 ∈ ( - π (,) π ) ↔ ( 0 ∈ ℝ ∧ - π < 0 ∧ 0 < π ) ) )
43 40 41 42 mp2an ⊢ ( 0 ∈ ( - π (,) π ) ↔ ( 0 ∈ ℝ ∧ - π < 0 ∧ 0 < π ) )
44 35 36 37 43 mpbir3an ⊢ 0 ∈ ( - π (,) π )
45 44 a1i ⊢ ( ⊤ → 0 ∈ ( - π (,) π ) )
46 eqid ⊢ ( ( - π (,) π ) ∖ { 0 } ) = ( ( - π (,) π ) ∖ { 0 } )
47 1ex ⊢ 1 ∈ V
48 eqid ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 )
49 47 48 dmmpti ⊢ dom ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) = ( ( - π (,) π ) ∖ { 0 } )
50 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
51 50 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
52 12 sseli ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
53 52 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
54 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
55 51 dvmptid ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
56 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
57 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
58 sncldre ⊢ ( 0 ∈ ℝ → { 0 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
59 35 58 ax-mp ⊢ { 0 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) )
60 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
61 60 toponunii ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
62 61 difopn ⊢ ( ( ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ∧ { 0 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) → ( ( - π (,) π ) ∖ { 0 } ) ∈ ( topGen ‘ ran (,) ) )
63 33 59 62 mp2an ⊢ ( ( - π (,) π ) ∖ { 0 } ) ∈ ( topGen ‘ ran (,) )
64 63 a1i ⊢ ( ⊤ → ( ( - π (,) π ) ∖ { 0 } ) ∈ ( topGen ‘ ran (,) ) )
65 51 53 54 55 20 56 57 64 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) )
66 65 mptru ⊢ ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 )
67 66 eqcomi ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) = ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
68 67 dmeqi ⊢ dom ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) = dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
69 49 68 eqtr3i ⊢ ( ( - π (,) π ) ∖ { 0 } ) = dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
70 69 eqimssi ⊢ ( ( - π (,) π ) ∖ { 0 } ) ⊆ dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
71 70 a1i ⊢ ( ⊤ → ( ( - π (,) π ) ∖ { 0 } ) ⊆ dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) )
72 fvex ⊢ ( cos ‘ ( 𝑥 / 2 ) ) ∈ V
73 eqid ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
74 72 73 dmmpti ⊢ dom ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) = ( ( - π (,) π ) ∖ { 0 } )
75 2cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 2 ∈ ℂ )
76 53 halfcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 / 2 ) ∈ ℂ )
77 76 sincld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
78 75 77 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℂ )
79 76 coscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( cos ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
80 2cnd ⊢ ( 𝑥 ∈ ℝ → 2 ∈ ℂ )
81 2ne0 ⊢ 2 ≠ 0
82 81 a1i ⊢ ( 𝑥 ∈ ℝ → 2 ≠ 0 )
83 52 80 82 divrec2d ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 / 2 ) = ( ( 1 / 2 ) · 𝑥 ) )
84 83 fveq2d ⊢ ( 𝑥 ∈ ℝ → ( sin ‘ ( 𝑥 / 2 ) ) = ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) )
85 84 oveq2d ⊢ ( 𝑥 ∈ ℝ → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
86 85 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
87 86 oveq2i ⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) )
88 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) )
89 12 88 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
90 89 eqcomi ⊢ ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ )
91 90 oveq2i ⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) = ( ℝ D ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) )
92 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
93 2cnd ⊢ ( 𝑥 ∈ ℂ → 2 ∈ ℂ )
94 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
95 94 a1i ⊢ ( 𝑥 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
96 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
97 95 96 mulcld ⊢ ( 𝑥 ∈ ℂ → ( ( 1 / 2 ) · 𝑥 ) ∈ ℂ )
98 97 sincld ⊢ ( 𝑥 ∈ ℂ → ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ∈ ℂ )
99 93 98 mulcld ⊢ ( 𝑥 ∈ ℂ → ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ∈ ℂ )
100 92 99 fmpti ⊢ ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) : ℂ ⟶ ℂ
101 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
102 2cn ⊢ 2 ∈ ℂ
103 102 94 mulcli ⊢ ( 2 · ( 1 / 2 ) ) ∈ ℂ
104 103 a1i ⊢ ( 𝑥 ∈ ℂ → ( 2 · ( 1 / 2 ) ) ∈ ℂ )
105 97 coscld ⊢ ( 𝑥 ∈ ℂ → ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ∈ ℂ )
106 104 105 mulcld ⊢ ( 𝑥 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ∈ ℂ )
107 106 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ∈ ℂ )
108 101 107 dmmptd ⊢ ( ⊤ → dom ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ℂ )
109 108 mptru ⊢ dom ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ℂ
110 12 109 sseqtrri ⊢ ℝ ⊆ dom ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
111 dvasinbx ⊢ ( ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) )
112 102 94 111 mp2an ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
113 112 dmeqi ⊢ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) = dom ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
114 110 113 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) )
115 dvcnre ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) ) → ( ℝ D ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) ↾ ℝ ) )
116 100 114 115 mp2an ⊢ ( ℝ D ( ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) ) = ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) ↾ ℝ )
117 112 reseq1i ⊢ ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) ↾ ℝ ) = ( ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ )
118 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) )
119 12 118 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) )
120 102 81 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
121 120 a1i ⊢ ( 𝑥 ∈ ℝ → ( 2 · ( 1 / 2 ) ) = 1 )
122 83 eqcomd ⊢ ( 𝑥 ∈ ℝ → ( ( 1 / 2 ) · 𝑥 ) = ( 𝑥 / 2 ) )
123 122 fveq2d ⊢ ( 𝑥 ∈ ℝ → ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) = ( cos ‘ ( 𝑥 / 2 ) ) )
124 121 123 oveq12d ⊢ ( 𝑥 ∈ ℝ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) = ( 1 · ( cos ‘ ( 𝑥 / 2 ) ) ) )
125 52 halfcld ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 / 2 ) ∈ ℂ )
126 125 coscld ⊢ ( 𝑥 ∈ ℝ → ( cos ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
127 126 mullidd ⊢ ( 𝑥 ∈ ℝ → ( 1 · ( cos ‘ ( 𝑥 / 2 ) ) ) = ( cos ‘ ( 𝑥 / 2 ) ) )
128 124 127 eqtrd ⊢ ( 𝑥 ∈ ℝ → ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) = ( cos ‘ ( 𝑥 / 2 ) ) )
129 128 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ ( ( 2 · ( 1 / 2 ) ) · ( cos ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
130 117 119 129 3eqtri ⊢ ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
131 91 116 130 3eqtri ⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( ( 1 / 2 ) · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
132 87 131 eqtri ⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
133 132 a1i ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) )
134 51 78 79 133 20 56 57 64 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) )
135 134 mptru ⊢ ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) )
136 135 eqcomi ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) = ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
137 136 dmeqi ⊢ dom ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) = dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
138 74 137 eqtr3i ⊢ ( ( - π (,) π ) ∖ { 0 } ) = dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
139 138 eqimssi ⊢ ( ( - π (,) π ) ∖ { 0 } ) ⊆ dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
140 139 a1i ⊢ ( ⊤ → ( ( - π (,) π ) ∖ { 0 } ) ⊆ dom ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) )
141 17 recnd ⊢ ( 𝑠 ∈ ( - π (,) π ) → 𝑠 ∈ ℂ )
142 141 ssriv ⊢ ( - π (,) π ) ⊆ ℂ
143 142 a1i ⊢ ( ⊤ → ( - π (,) π ) ⊆ ℂ )
144 ssid ⊢ ℂ ⊆ ℂ
145 144 a1i ⊢ ( ⊤ → ℂ ⊆ ℂ )
146 143 145 idcncfg ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
147 146 mptru ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ∈ ( ( - π (,) π ) –cn→ ℂ )
148 cnlimc ⊢ ( ( - π (,) π ) ⊆ ℂ → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) ) ) )
149 142 148 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) ) )
150 147 149 mpbi ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) )
151 150 simpri ⊢ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 )
152 fveq2 ⊢ ( 𝑦 = 0 → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) )
153 oveq2 ⊢ ( 𝑦 = 0 → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) = ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) )
154 152 153 eleq12d ⊢ ( 𝑦 = 0 → ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) ) )
155 154 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 𝑦 ) ∧ 0 ∈ ( - π (,) π ) ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) )
156 151 44 155 mp2an ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 )
157 id ⊢ ( 𝑥 = 0 → 𝑥 = 0 )
158 eqid ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) = ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 )
159 c0ex ⊢ 0 ∈ V
160 157 158 159 fvmpt ⊢ ( 0 ∈ ( - π (,) π ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) = 0 )
161 44 160 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ‘ 0 ) = 0
162 elioore ⊢ ( 𝑥 ∈ ( - π (,) π ) → 𝑥 ∈ ℝ )
163 162 recnd ⊢ ( 𝑥 ∈ ( - π (,) π ) → 𝑥 ∈ ℂ )
164 158 163 fmpti ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) : ( - π (,) π ) ⟶ ℂ
165 164 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) : ( - π (,) π ) ⟶ ℂ )
166 165 limcdif ⊢ ( ⊤ → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) = ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) )
167 166 mptru ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) = ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 )
168 resmpt ⊢ ( ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( - π (,) π ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
169 16 168 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 )
170 169 oveq1i ⊢ ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) limℂ 0 )
171 167 170 eqtri ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ 𝑥 ) limℂ 0 ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) limℂ 0 )
172 156 161 171 3eltr3i ⊢ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) limℂ 0 )
173 172 a1i ⊢ ( ⊤ → 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) limℂ 0 ) )
174 eqid ⊢ ( 𝑥 ∈ ℂ ↦ 2 ) = ( 𝑥 ∈ ℂ ↦ 2 )
175 144 a1i ⊢ ( 2 ∈ ℂ → ℂ ⊆ ℂ )
176 2cnd ⊢ ( 2 ∈ ℂ → 2 ∈ ℂ )
177 175 176 175 constcncfg ⊢ ( 2 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ℂ –cn→ ℂ ) )
178 102 177 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ℂ –cn→ ℂ ) )
179 2cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( - π (,) π ) ) → 2 ∈ ℂ )
180 174 178 143 145 179 cncfmptssg ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ 2 ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
181 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
182 181 a1i ⊢ ( ⊤ → sin ∈ ( ℂ –cn→ ℂ ) )
183 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) )
184 183 divccncf ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
185 102 81 184 mp2an ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ℂ –cn→ ℂ )
186 185 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
187 163 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑥 ∈ ℂ )
188 187 halfcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝑥 / 2 ) ∈ ℂ )
189 183 186 143 145 188 cncfmptssg ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ ( 𝑥 / 2 ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
190 182 189 cncfmpt1f ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
191 180 190 mulcncf ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
192 191 mptru ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ∈ ( ( - π (,) π ) –cn→ ℂ )
193 cnlimc ⊢ ( ( - π (,) π ) ⊆ ℂ → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) ) ) )
194 142 193 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) ) )
195 192 194 mpbi ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( - π (,) π ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) )
196 195 simpri ⊢ ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 )
197 fveq2 ⊢ ( 𝑦 = 0 → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) )
198 oveq2 ⊢ ( 𝑦 = 0 → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) = ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) )
199 197 198 eleq12d ⊢ ( 𝑦 = 0 → ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) ↔ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) ) )
200 199 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( - π (,) π ) ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 𝑦 ) ∧ 0 ∈ ( - π (,) π ) ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) )
201 196 44 200 mp2an ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) ∈ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 )
202 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 / 2 ) = ( 0 / 2 ) )
203 102 81 div0i ⊢ ( 0 / 2 ) = 0
204 202 203 eqtrdi ⊢ ( 𝑥 = 0 → ( 𝑥 / 2 ) = 0 )
205 204 fveq2d ⊢ ( 𝑥 = 0 → ( sin ‘ ( 𝑥 / 2 ) ) = ( sin ‘ 0 ) )
206 sin0 ⊢ ( sin ‘ 0 ) = 0
207 205 206 eqtrdi ⊢ ( 𝑥 = 0 → ( sin ‘ ( 𝑥 / 2 ) ) = 0 )
208 207 oveq2d ⊢ ( 𝑥 = 0 → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( 2 · 0 ) )
209 2t0e0 ⊢ ( 2 · 0 ) = 0
210 208 209 eqtrdi ⊢ ( 𝑥 = 0 → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = 0 )
211 eqid ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) )
212 210 211 159 fvmpt ⊢ ( 0 ∈ ( - π (,) π ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) = 0 )
213 44 212 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 0 ) = 0
214 2cnd ⊢ ( 𝑥 ∈ ( - π (,) π ) → 2 ∈ ℂ )
215 163 halfcld ⊢ ( 𝑥 ∈ ( - π (,) π ) → ( 𝑥 / 2 ) ∈ ℂ )
216 215 sincld ⊢ ( 𝑥 ∈ ( - π (,) π ) → ( sin ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
217 214 216 mulcld ⊢ ( 𝑥 ∈ ( - π (,) π ) → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℂ )
218 211 217 fmpti ⊢ ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( - π (,) π ) ⟶ ℂ
219 218 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) : ( - π (,) π ) ⟶ ℂ )
220 219 limcdif ⊢ ( ⊤ → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) = ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) )
221 220 mptru ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) = ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 )
222 resmpt ⊢ ( ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( - π (,) π ) → ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
223 16 222 ax-mp ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) )
224 223 oveq1i ⊢ ( ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 )
225 221 224 eqtri ⊢ ( ( 𝑥 ∈ ( - π (,) π ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 )
226 201 213 225 3eltr3i ⊢ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 )
227 226 a1i ⊢ ( ⊤ → 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) limℂ 0 ) )
228 eqidd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
229 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 / 2 ) = ( 𝑦 / 2 ) )
230 229 fveq2d ⊢ ( 𝑥 = 𝑦 → ( sin ‘ ( 𝑥 / 2 ) ) = ( sin ‘ ( 𝑦 / 2 ) ) )
231 230 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) )
232 231 adantl ⊢ ( ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑦 ) → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) )
233 id ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) )
234 26 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℝ )
235 19 sseli ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ∈ ℝ )
236 235 rehalfcld ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑦 / 2 ) ∈ ℝ )
237 236 resincld ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℝ )
238 234 237 remulcld ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ∈ ℝ )
239 228 232 233 238 fvmptd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) )
240 2cnd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℂ )
241 237 recnd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( sin ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
242 81 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ≠ 0 )
243 ioossicc ⊢ ( - π (,) π ) ⊆ ( - π [,] π )
244 eldifi ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ∈ ( - π (,) π ) )
245 243 244 sselid ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ∈ ( - π [,] π ) )
246 eldifsni ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ≠ 0 )
247 fourierdlem44 ⊢ ( ( 𝑦 ∈ ( - π [,] π ) ∧ 𝑦 ≠ 0 ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
248 245 246 247 syl2anc ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
249 240 241 242 248 mulne0d ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑦 / 2 ) ) ) ≠ 0 )
250 239 249 eqnetrd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) ≠ 0 )
251 250 neneqd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = 0 )
252 251 nrex ⊢ ¬ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = 0
253 25 fnmpt ⊢ ( ∀ 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℝ → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) Fn ( ( - π (,) π ) ∖ { 0 } ) )
254 253 30 mprg ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) Fn ( ( - π (,) π ) ∖ { 0 } )
255 ssid ⊢ ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( ( - π (,) π ) ∖ { 0 } )
256 fvelimab ⊢ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) Fn ( ( - π (,) π ) ∖ { 0 } ) ∧ ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( ( - π (,) π ) ∖ { 0 } ) ) → ( 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) ↔ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = 0 ) )
257 254 255 256 mp2an ⊢ ( 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) ↔ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑦 ) = 0 )
258 252 257 mtbir ⊢ ¬ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) )
259 258 a1i ⊢ ( ⊤ → ¬ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) )
260 eqidd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) )
261 229 fveq2d ⊢ ( 𝑥 = 𝑦 → ( cos ‘ ( 𝑥 / 2 ) ) = ( cos ‘ ( 𝑦 / 2 ) ) )
262 261 adantl ⊢ ( ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑦 ) → ( cos ‘ ( 𝑥 / 2 ) ) = ( cos ‘ ( 𝑦 / 2 ) ) )
263 235 recnd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 ∈ ℂ )
264 263 halfcld ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑦 / 2 ) ∈ ℂ )
265 264 coscld ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑦 / 2 ) ) ∈ ℂ )
266 260 262 233 265 fvmptd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) = ( cos ‘ ( 𝑦 / 2 ) ) )
267 236 rered ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ℜ ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
268 halfpire ⊢ ( π / 2 ) ∈ ℝ
269 268 renegcli ⊢ - ( π / 2 ) ∈ ℝ
270 269 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) ∈ ℝ )
271 270 rexrd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) ∈ ℝ* )
272 268 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( π / 2 ) ∈ ℝ )
273 272 rexrd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( π / 2 ) ∈ ℝ* )
274 picn ⊢ π ∈ ℂ
275 divneg ⊢ ( ( π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( π / 2 ) = ( - π / 2 ) )
276 274 102 81 275 mp3an ⊢ - ( π / 2 ) = ( - π / 2 )
277 39 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π ∈ ℝ )
278 2rp ⊢ 2 ∈ ℝ+
279 278 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℝ+ )
280 40 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π ∈ ℝ* )
281 41 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → π ∈ ℝ* )
282 ioogtlb ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑦 ∈ ( - π (,) π ) ) → - π < 𝑦 )
283 280 281 244 282 syl3anc ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π < 𝑦 )
284 277 235 279 283 ltdiv1dd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( - π / 2 ) < ( 𝑦 / 2 ) )
285 276 284 eqbrtrid ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) < ( 𝑦 / 2 ) )
286 38 a1i ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → π ∈ ℝ )
287 iooltub ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑦 ∈ ( - π (,) π ) ) → 𝑦 < π )
288 280 281 244 287 syl3anc ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑦 < π )
289 235 286 279 288 ltdiv1dd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑦 / 2 ) < ( π / 2 ) )
290 271 273 236 285 289 eliood ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑦 / 2 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
291 267 290 eqeltrd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ℜ ‘ ( 𝑦 / 2 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
292 cosne0 ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ ( ℜ ‘ ( 𝑦 / 2 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
293 264 291 292 syl2anc ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
294 266 293 eqnetrd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) ≠ 0 )
295 294 neneqd ⊢ ( 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) = 0 )
296 295 nrex ⊢ ¬ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) = 0
297 72 73 fnmpti ⊢ ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) Fn ( ( - π (,) π ) ∖ { 0 } )
298 fvelimab ⊢ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) Fn ( ( - π (,) π ) ∖ { 0 } ) ∧ ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( ( - π (,) π ) ∖ { 0 } ) ) → ( 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) ↔ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) = 0 ) )
299 297 255 298 mp2an ⊢ ( 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) ↔ ∃ 𝑦 ∈ ( ( - π (,) π ) ∖ { 0 } ) ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) ‘ 𝑦 ) = 0 )
300 296 299 mtbir ⊢ ¬ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) )
301 135 imaeq1i ⊢ ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) )
302 301 eleq2i ⊢ ( 0 ∈ ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) ↔ 0 ∈ ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) )
303 300 302 mtbir ⊢ ¬ 0 ∈ ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) )
304 303 a1i ⊢ ( ⊤ → ¬ 0 ∈ ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) “ ( ( - π (,) π ) ∖ { 0 } ) ) )
305 eqid ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) )
306 eqid ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) )
307 19 sseli ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑠 ∈ ℝ )
308 307 recnd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑠 ∈ ℂ )
309 308 halfcld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑠 / 2 ) ∈ ℂ )
310 309 coscld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
311 307 rehalfcld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑠 / 2 ) ∈ ℝ )
312 311 rered ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ℜ ‘ ( 𝑠 / 2 ) ) = ( 𝑠 / 2 ) )
313 269 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) ∈ ℝ )
314 313 rexrd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) ∈ ℝ* )
315 268 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( π / 2 ) ∈ ℝ )
316 315 rexrd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( π / 2 ) ∈ ℝ* )
317 38 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → π ∈ ℝ )
318 317 renegcld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π ∈ ℝ )
319 278 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℝ+ )
320 40 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π ∈ ℝ* )
321 41 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → π ∈ ℝ* )
322 eldifi ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑠 ∈ ( - π (,) π ) )
323 ioogtlb ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( - π (,) π ) ) → - π < 𝑠 )
324 320 321 322 323 syl3anc ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - π < 𝑠 )
325 318 307 319 324 ltdiv1dd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( - π / 2 ) < ( 𝑠 / 2 ) )
326 276 325 eqbrtrid ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → - ( π / 2 ) < ( 𝑠 / 2 ) )
327 iooltub ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( - π (,) π ) ) → 𝑠 < π )
328 320 321 322 327 syl3anc ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑠 < π )
329 307 317 319 328 ltdiv1dd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑠 / 2 ) < ( π / 2 ) )
330 314 316 311 326 329 eliood ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑠 / 2 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
331 312 330 eqeltrd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ℜ ‘ ( 𝑠 / 2 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
332 cosne0 ⊢ ( ( ( 𝑠 / 2 ) ∈ ℂ ∧ ( ℜ ‘ ( 𝑠 / 2 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ≠ 0 )
333 309 331 332 syl2anc ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑠 / 2 ) ) ≠ 0 )
334 333 neneqd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ ( cos ‘ ( 𝑠 / 2 ) ) = 0 )
335 311 recoscld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
336 elsng ⊢ ( ( cos ‘ ( 𝑠 / 2 ) ) ∈ ℝ → ( ( cos ‘ ( 𝑠 / 2 ) ) ∈ { 0 } ↔ ( cos ‘ ( 𝑠 / 2 ) ) = 0 ) )
337 335 336 syl ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( cos ‘ ( 𝑠 / 2 ) ) ∈ { 0 } ↔ ( cos ‘ ( 𝑠 / 2 ) ) = 0 ) )
338 334 337 mtbird ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ ( cos ‘ ( 𝑠 / 2 ) ) ∈ { 0 } )
339 310 338 eldifd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ( ℂ ∖ { 0 } ) )
340 339 adantl ⊢ ( ( ⊤ ∧ 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ) → ( cos ‘ ( 𝑠 / 2 ) ) ∈ ( ℂ ∖ { 0 } ) )
341 309 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ ( 𝑠 / 2 ) ≠ 0 ) ) → ( 𝑠 / 2 ) ∈ ℂ )
342 cosf ⊢ cos : ℂ ⟶ ℂ
343 342 a1i ⊢ ( ⊤ → cos : ℂ ⟶ ℂ )
344 343 ffvelcdmda ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ ℂ )
345 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 / 2 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 / 2 ) )
346 345 divccncf ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑠 ∈ ℂ ↦ ( 𝑠 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
347 102 81 346 mp2an ⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 / 2 ) ) ∈ ( ℂ –cn→ ℂ )
348 347 a1i ⊢ ( ⊤ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
349 141 adantl ⊢ ( ( ⊤ ∧ 𝑠 ∈ ( - π (,) π ) ) → 𝑠 ∈ ℂ )
350 349 halfcld ⊢ ( ( ⊤ ∧ 𝑠 ∈ ( - π (,) π ) ) → ( 𝑠 / 2 ) ∈ ℂ )
351 345 348 143 145 350 cncfmptssg ⊢ ( ⊤ → ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ∈ ( ( - π (,) π ) –cn→ ℂ ) )
352 oveq1 ⊢ ( 𝑠 = 0 → ( 𝑠 / 2 ) = ( 0 / 2 ) )
353 352 203 eqtrdi ⊢ ( 𝑠 = 0 → ( 𝑠 / 2 ) = 0 )
354 351 45 353 cnmptlimc ⊢ ( ⊤ → 0 ∈ ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) limℂ 0 ) )
355 eqid ⊢ ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) = ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) )
356 141 halfcld ⊢ ( 𝑠 ∈ ( - π (,) π ) → ( 𝑠 / 2 ) ∈ ℂ )
357 355 356 fmpti ⊢ ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) : ( - π (,) π ) ⟶ ℂ
358 357 a1i ⊢ ( ⊤ → ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) : ( - π (,) π ) ⟶ ℂ )
359 358 limcdif ⊢ ( ⊤ → ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) limℂ 0 ) = ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) )
360 359 mptru ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) limℂ 0 ) = ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 )
361 resmpt ⊢ ( ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( - π (,) π ) → ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) )
362 16 361 ax-mp ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) )
363 362 oveq1i ⊢ ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) limℂ 0 )
364 360 363 eqtri ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ ( 𝑠 / 2 ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) limℂ 0 )
365 354 364 eleqtrdi ⊢ ( ⊤ → 0 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) limℂ 0 ) )
366 ffn ⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
367 342 366 ax-mp ⊢ cos Fn ℂ
368 dffn5 ⊢ ( cos Fn ℂ ↔ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
369 367 368 mpbi ⊢ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) )
370 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
371 369 370 eqeltrri ⊢ ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ∈ ( ℂ –cn→ ℂ )
372 371 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
373 0cnd ⊢ ( ⊤ → 0 ∈ ℂ )
374 fveq2 ⊢ ( 𝑥 = 0 → ( cos ‘ 𝑥 ) = ( cos ‘ 0 ) )
375 cos0 ⊢ ( cos ‘ 0 ) = 1
376 374 375 eqtrdi ⊢ ( 𝑥 = 0 → ( cos ‘ 𝑥 ) = 1 )
377 372 373 376 cnmptlimc ⊢ ( ⊤ → 1 ∈ ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) limℂ 0 ) )
378 fveq2 ⊢ ( 𝑥 = ( 𝑠 / 2 ) → ( cos ‘ 𝑥 ) = ( cos ‘ ( 𝑠 / 2 ) ) )
379 fveq2 ⊢ ( ( 𝑠 / 2 ) = 0 → ( cos ‘ ( 𝑠 / 2 ) ) = ( cos ‘ 0 ) )
380 379 375 eqtrdi ⊢ ( ( 𝑠 / 2 ) = 0 → ( cos ‘ ( 𝑠 / 2 ) ) = 1 )
381 380 ad2antll ⊢ ( ( ⊤ ∧ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ ( 𝑠 / 2 ) = 0 ) ) → ( cos ‘ ( 𝑠 / 2 ) ) = 1 )
382 341 344 365 377 378 381 limcco ⊢ ( ⊤ → 1 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) limℂ 0 ) )
383 ax-1ne0 ⊢ 1 ≠ 0
384 383 a1i ⊢ ( ⊤ → 1 ≠ 0 )
385 305 306 340 382 384 reclimc ⊢ ( ⊤ → ( 1 / 1 ) ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) ) limℂ 0 ) )
386 1div1e1 ⊢ ( 1 / 1 ) = 1
387 66 fveq1i ⊢ ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) = ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) ‘ 𝑠 )
388 eqidd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) )
389 eqidd ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → 1 = 1 )
390 id ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) )
391 1red ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 1 ∈ ℝ )
392 388 389 390 391 fvmptd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 1 ) ‘ 𝑠 ) = 1 )
393 387 392 eqtr2id ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 1 = ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) )
394 135 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( cos ‘ ( 𝑥 / 2 ) ) ) )
395 oveq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 / 2 ) = ( 𝑠 / 2 ) )
396 395 fveq2d ⊢ ( 𝑥 = 𝑠 → ( cos ‘ ( 𝑥 / 2 ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
397 396 adantl ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → ( cos ‘ ( 𝑥 / 2 ) ) = ( cos ‘ ( 𝑠 / 2 ) ) )
398 394 397 390 335 fvmptd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) = ( cos ‘ ( 𝑠 / 2 ) ) )
399 398 eqcomd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( cos ‘ ( 𝑠 / 2 ) ) = ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) )
400 393 399 oveq12d ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) = ( ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) / ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) ) )
401 400 mpteq2ia ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) / ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) ) )
402 401 oveq1i ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 1 / ( cos ‘ ( 𝑠 / 2 ) ) ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) / ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) ) ) limℂ 0 )
403 385 386 402 3eltr3g ⊢ ( ⊤ → 1 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ) ‘ 𝑠 ) / ( ( ℝ D ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) ‘ 𝑠 ) ) ) limℂ 0 ) )
404 20 24 32 34 45 46 71 140 173 227 259 304 403 lhop ⊢ ( ⊤ → 1 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) / ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) ) ) limℂ 0 ) )
405 404 mptru ⊢ 1 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) / ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) ) ) limℂ 0 )
406 eqidd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) )
407 simpr ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → 𝑥 = 𝑠 )
408 406 407 390 307 fvmptd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) = 𝑠 )
409 eqidd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
410 407 oveq1d ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → ( 𝑥 / 2 ) = ( 𝑠 / 2 ) )
411 410 fveq2d ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → ( sin ‘ ( 𝑥 / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
412 411 oveq2d ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ∧ 𝑥 = 𝑠 ) → ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
413 26 a1i ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → 2 ∈ ℝ )
414 311 resincld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
415 413 414 remulcld ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
416 409 412 390 415 fvmptd ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) = ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
417 408 416 oveq12d ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) / ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
418 417 mpteq2ia ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) / ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
419 418 oveq1i ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ 𝑥 ) ‘ 𝑠 ) / ( ( 𝑥 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ‘ 𝑠 ) ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ 0 )
420 405 419 eleqtri ⊢ 1 ∈ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ 0 )
421 10 oveq1i ⊢ ( 𝐾 limℂ 0 ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 )
422 10 feq1i ⊢ ( 𝐾 : ( - π [,] π ) ⟶ ℂ ↔ ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) : ( - π [,] π ) ⟶ ℂ )
423 14 422 mpbi ⊢ ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) : ( - π [,] π ) ⟶ ℂ
424 423 a1i ⊢ ( ⊤ → ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) : ( - π [,] π ) ⟶ ℂ )
425 243 a1i ⊢ ( ⊤ → ( - π (,) π ) ⊆ ( - π [,] π ) )
426 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
427 39 38 426 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
428 427 a1i ⊢ ( ⊤ → ( - π [,] π ) ⊆ ℝ )
429 428 12 sstrdi ⊢ ( ⊤ → ( - π [,] π ) ⊆ ℂ )
430 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) )
431 39 35 36 ltleii ⊢ - π ≤ 0
432 35 38 37 ltleii ⊢ 0 ≤ π
433 39 38 elicc2i ⊢ ( 0 ∈ ( - π [,] π ) ↔ ( 0 ∈ ℝ ∧ - π ≤ 0 ∧ 0 ≤ π ) )
434 35 431 432 433 mpbir3an ⊢ 0 ∈ ( - π [,] π )
435 159 snss ⊢ ( 0 ∈ ( - π [,] π ) ↔ { 0 } ⊆ ( - π [,] π ) )
436 434 435 mpbi ⊢ { 0 } ⊆ ( - π [,] π )
437 ssequn2 ⊢ ( { 0 } ⊆ ( - π [,] π ) ↔ ( ( - π [,] π ) ∪ { 0 } ) = ( - π [,] π ) )
438 436 437 mpbi ⊢ ( ( - π [,] π ) ∪ { 0 } ) = ( - π [,] π )
439 438 oveq2i ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) )
440 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
441 57 440 rerest ⊢ ( ( - π [,] π ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) )
442 427 441 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) )
443 439 442 eqtri ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) )
444 443 fveq2i ⊢ ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) ) = ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) )
445 159 snss ⊢ ( 0 ∈ ( - π (,) π ) ↔ { 0 } ⊆ ( - π (,) π ) )
446 44 445 mpbi ⊢ { 0 } ⊆ ( - π (,) π )
447 ssequn2 ⊢ ( { 0 } ⊆ ( - π (,) π ) ↔ ( ( - π (,) π ) ∪ { 0 } ) = ( - π (,) π ) )
448 446 447 mpbi ⊢ ( ( - π (,) π ) ∪ { 0 } ) = ( - π (,) π )
449 444 448 fveq12i ⊢ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) ) ‘ ( ( - π (,) π ) ∪ { 0 } ) ) = ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( - π (,) π ) )
450 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( - π [,] π ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ ( TopOn ‘ ( - π [,] π ) ) )
451 60 427 450 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ ( TopOn ‘ ( - π [,] π ) )
452 451 topontopi ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ Top
453 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
454 ovex ⊢ ( - π [,] π ) ∈ V
455 453 454 pm3.2i ⊢ ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( - π [,] π ) ∈ V )
456 ssid ⊢ ( - π (,) π ) ⊆ ( - π (,) π )
457 33 243 456 3pm3.2i ⊢ ( ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ∧ ( - π (,) π ) ⊆ ( - π [,] π ) ∧ ( - π (,) π ) ⊆ ( - π (,) π ) )
458 restopnb ⊢ ( ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( - π [,] π ) ∈ V ) ∧ ( ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ∧ ( - π (,) π ) ⊆ ( - π [,] π ) ∧ ( - π (,) π ) ⊆ ( - π (,) π ) ) ) → ( ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ↔ ( - π (,) π ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) )
459 455 457 458 mp2an ⊢ ( ( - π (,) π ) ∈ ( topGen ‘ ran (,) ) ↔ ( - π (,) π ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) )
460 33 459 mpbi ⊢ ( - π (,) π ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) )
461 isopn3i ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ Top ∧ ( - π (,) π ) ∈ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( - π (,) π ) ) = ( - π (,) π ) )
462 452 460 461 mp2an ⊢ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( - π (,) π ) ) = ( - π (,) π )
463 eqid ⊢ ( - π (,) π ) = ( - π (,) π )
464 449 462 463 3eqtrri ⊢ ( - π (,) π ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) ) ‘ ( ( - π (,) π ) ∪ { 0 } ) )
465 44 464 eleqtri ⊢ 0 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) ) ‘ ( ( - π (,) π ) ∪ { 0 } ) )
466 465 a1i ⊢ ( ⊤ → 0 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∪ { 0 } ) ) ) ‘ ( ( - π (,) π ) ∪ { 0 } ) ) )
467 424 425 429 57 430 466 limcres ⊢ ( ⊤ → ( ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 ) )
468 467 mptru ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 )
469 468 eqcomi ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 ) = ( ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) limℂ 0 )
470 resmpt ⊢ ( ( - π (,) π ) ⊆ ( - π [,] π ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) = ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
471 243 470 ax-mp ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) = ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
472 471 oveq1i ⊢ ( ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( - π (,) π ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 )
473 421 469 472 3eqtri ⊢ ( 𝐾 limℂ 0 ) = ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 )
474 eqid ⊢ ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
475 iftrue ⊢ ( 𝑠 = 0 → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = 1 )
476 1cnd ⊢ ( 𝑠 = 0 → 1 ∈ ℂ )
477 475 476 eqeltrd ⊢ ( 𝑠 = 0 → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℂ )
478 477 adantl ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ 𝑠 = 0 ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℂ )
479 iffalse ⊢ ( ¬ 𝑠 = 0 → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
480 479 adantl ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
481 141 adantr ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ℂ )
482 2cnd ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → 2 ∈ ℂ )
483 481 halfcld ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( 𝑠 / 2 ) ∈ ℂ )
484 483 sincld ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
485 482 484 mulcld ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
486 81 a1i ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → 2 ≠ 0 )
487 243 sseli ⊢ ( 𝑠 ∈ ( - π (,) π ) → 𝑠 ∈ ( - π [,] π ) )
488 neqne ⊢ ( ¬ 𝑠 = 0 → 𝑠 ≠ 0 )
489 fourierdlem44 ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
490 487 488 489 syl2an ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
491 482 484 486 490 mulne0d ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
492 481 485 491 divcld ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
493 480 492 eqeltrd ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ∧ ¬ 𝑠 = 0 ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℂ )
494 478 493 pm2.61dan ⊢ ( 𝑠 ∈ ( - π (,) π ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ℂ )
495 474 494 fmpti ⊢ ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) : ( - π (,) π ) ⟶ ℂ
496 495 a1i ⊢ ( ⊤ → ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) : ( - π (,) π ) ⟶ ℂ )
497 496 limcdif ⊢ ( ⊤ → ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 ) = ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) )
498 497 mptru ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ 0 ) = ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 )
499 resmpt ⊢ ( ( ( - π (,) π ) ∖ { 0 } ) ⊆ ( - π (,) π ) → ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
500 16 499 ax-mp ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
501 eldifn ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ 𝑠 ∈ { 0 } )
502 velsn ⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
503 501 502 sylnib ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → ¬ 𝑠 = 0 )
504 503 479 syl ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
505 504 mpteq2ia ⊢ ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
506 500 505 eqtri ⊢ ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
507 506 oveq1i ⊢ ( ( ( 𝑠 ∈ ( - π (,) π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π (,) π ) ∖ { 0 } ) ) limℂ 0 ) = ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ 0 )
508 473 498 507 3eqtrri ⊢ ( ( 𝑠 ∈ ( ( - π (,) π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ 0 ) = ( 𝐾 limℂ 0 )
509 420 508 eleqtri ⊢ 1 ∈ ( 𝐾 limℂ 0 )
510 509 a1i ⊢ ( 𝑠 = 0 → 1 ∈ ( 𝐾 limℂ 0 ) )
511 fveq2 ⊢ ( 𝑠 = 0 → ( 𝐾 ‘ 𝑠 ) = ( 𝐾 ‘ 0 ) )
512 475 10 47 fvmpt ⊢ ( 0 ∈ ( - π [,] π ) → ( 𝐾 ‘ 0 ) = 1 )
513 434 512 ax-mp ⊢ ( 𝐾 ‘ 0 ) = 1
514 511 513 eqtrdi ⊢ ( 𝑠 = 0 → ( 𝐾 ‘ 𝑠 ) = 1 )
515 oveq2 ⊢ ( 𝑠 = 0 → ( 𝐾 limℂ 𝑠 ) = ( 𝐾 limℂ 0 ) )
516 510 514 515 3eltr4d ⊢ ( 𝑠 = 0 → ( 𝐾 ‘ 𝑠 ) ∈ ( 𝐾 limℂ 𝑠 ) )
517 427 12 sstri ⊢ ( - π [,] π ) ⊆ ℂ
518 517 a1i ⊢ ( 𝑠 = 0 → ( - π [,] π ) ⊆ ℂ )
519 38 a1i ⊢ ( 𝑠 = 0 → π ∈ ℝ )
520 519 renegcld ⊢ ( 𝑠 = 0 → - π ∈ ℝ )
521 id ⊢ ( 𝑠 = 0 → 𝑠 = 0 )
522 35 a1i ⊢ ( 𝑠 = 0 → 0 ∈ ℝ )
523 521 522 eqeltrd ⊢ ( 𝑠 = 0 → 𝑠 ∈ ℝ )
524 431 521 breqtrrid ⊢ ( 𝑠 = 0 → - π ≤ 𝑠 )
525 521 432 eqbrtrdi ⊢ ( 𝑠 = 0 → 𝑠 ≤ π )
526 520 519 523 524 525 eliccd ⊢ ( 𝑠 = 0 → 𝑠 ∈ ( - π [,] π ) )
527 56 oveq1i ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( - π [,] π ) )
528 57 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
529 reex ⊢ ℝ ∈ V
530 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( - π [,] π ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( - π [,] π ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) ) )
531 528 427 529 530 mp3an ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( - π [,] π ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) )
532 527 531 eqtri ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( - π [,] π ) )
533 57 532 cnplimc ⊢ ( ( ( - π [,] π ) ⊆ ℂ ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝐾 : ( - π [,] π ) ⟶ ℂ ∧ ( 𝐾 ‘ 𝑠 ) ∈ ( 𝐾 limℂ 𝑠 ) ) ) )
534 518 526 533 syl2anc ⊢ ( 𝑠 = 0 → ( 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝐾 : ( - π [,] π ) ⟶ ℂ ∧ ( 𝐾 ‘ 𝑠 ) ∈ ( 𝐾 limℂ 𝑠 ) ) ) )
535 15 516 534 mpbir2and ⊢ ( 𝑠 = 0 → 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
536 535 adantl ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 = 0 ) → 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
537 simpl ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( - π [,] π ) )
538 502 notbii ⊢ ( ¬ 𝑠 ∈ { 0 } ↔ ¬ 𝑠 = 0 )
539 538 biimpri ⊢ ( ¬ 𝑠 = 0 → ¬ 𝑠 ∈ { 0 } )
540 539 adantl ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ¬ 𝑠 ∈ { 0 } )
541 537 540 eldifd ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
542 fveq2 ⊢ ( 𝑥 = 𝑠 → ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
543 542 eleq2d ⊢ ( 𝑥 = 𝑠 → ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
544 429 ssdifssd ⊢ ( ⊤ → ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℂ )
545 544 145 idcncfg ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ 𝑠 ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
546 eqid ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
547 2cnd ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 2 ∈ ℂ )
548 eldifi ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 𝑠 ∈ ( - π [,] π ) )
549 517 548 sselid ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 𝑠 ∈ ℂ )
550 549 halfcld ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 𝑠 / 2 ) ∈ ℂ )
551 550 sincld ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
552 547 551 mulcld ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
553 81 a1i ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 2 ≠ 0 )
554 eldifsni ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 𝑠 ≠ 0 )
555 548 554 489 syl2anc ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
556 547 551 553 555 mulne0d ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
557 556 neneqd ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 )
558 elsng ⊢ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
559 552 558 syl ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
560 557 559 mtbird ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } )
561 552 560 eldifd ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
562 546 561 fmpti ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ( ℂ ∖ { 0 } )
563 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
564 eqid ⊢ ( 𝑠 ∈ ℂ ↦ 2 ) = ( 𝑠 ∈ ℂ ↦ 2 )
565 175 176 175 constcncfg ⊢ ( 2 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ 2 ) ∈ ( ℂ –cn→ ℂ ) )
566 102 565 mp1i ⊢ ( ⊤ → ( 𝑠 ∈ ℂ ↦ 2 ) ∈ ( ℂ –cn→ ℂ ) )
567 2cnd ⊢ ( ( ⊤ ∧ 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ) → 2 ∈ ℂ )
568 564 566 544 145 567 cncfmptssg ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ 2 ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
569 549 547 553 divrecd ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 𝑠 / 2 ) = ( 𝑠 · ( 1 / 2 ) ) )
570 569 mpteq2ia ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 · ( 1 / 2 ) ) )
571 eqid ⊢ ( 𝑠 ∈ ℂ ↦ ( 1 / 2 ) ) = ( 𝑠 ∈ ℂ ↦ ( 1 / 2 ) )
572 144 a1i ⊢ ( ( 1 / 2 ) ∈ ℂ → ℂ ⊆ ℂ )
573 id ⊢ ( ( 1 / 2 ) ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
574 572 573 572 constcncfg ⊢ ( ( 1 / 2 ) ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 1 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
575 94 574 mp1i ⊢ ( ⊤ → ( 𝑠 ∈ ℂ ↦ ( 1 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
576 94 a1i ⊢ ( ( ⊤ ∧ 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ) → ( 1 / 2 ) ∈ ℂ )
577 571 575 544 145 576 cncfmptssg ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 1 / 2 ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
578 545 577 mulcncf ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 · ( 1 / 2 ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
579 570 578 eqeltrid ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / 2 ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
580 182 579 cncfmpt1f ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
581 568 580 mulcncf ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
582 581 mptru ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ )
583 cncfcdm ⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) ) → ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ( ℂ ∖ { 0 } ) ) )
584 563 582 583 mp2an ⊢ ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ( ℂ ∖ { 0 } ) )
585 562 584 mpbir ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ( ℂ ∖ { 0 } ) )
586 585 a1i ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ( ℂ ∖ { 0 } ) ) )
587 545 586 divcncf ⊢ ( ⊤ → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) )
588 587 mptru ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ )
589 428 ssdifssd ⊢ ( ⊤ → ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ )
590 589 mptru ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ
591 590 12 sstri ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℂ
592 56 oveq1i ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( - π [,] π ) ∖ { 0 } ) )
593 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) )
594 528 590 529 593 mp3an ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∖ { 0 } ) )
595 592 594 eqtri ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( - π [,] π ) ∖ { 0 } ) )
596 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
597 596 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
598 528 597 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
599 598 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
600 57 595 599 cncfcn ⊢ ( ( ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
601 591 144 600 mp2an ⊢ ( ( ( - π [,] π ) ∖ { 0 } ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) )
602 588 601 eleqtri ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) )
603 resttopon ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ( - π [,] π ) ∖ { 0 } ) ) )
604 60 590 603 mp2an ⊢ ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ( - π [,] π ) ∖ { 0 } ) )
605 57 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
606 cncnp ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ( - π [,] π ) ∖ { 0 } ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ( - π [,] π ) ∖ { 0 } ) ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
607 604 605 606 mp2an ⊢ ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ( - π [,] π ) ∖ { 0 } ) ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
608 602 607 mpbi ⊢ ( ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) : ( ( - π [,] π ) ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ( - π [,] π ) ∖ { 0 } ) ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
609 608 simpri ⊢ ∀ 𝑥 ∈ ( ( - π [,] π ) ∖ { 0 } ) ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 )
610 543 609 vtoclri ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
611 541 610 syl ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
612 10 reseq1i ⊢ ( 𝐾 ↾ ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π [,] π ) ∖ { 0 } ) )
613 difss ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π )
614 resmpt ⊢ ( ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π [,] π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
615 613 614 ax-mp ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( - π [,] π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
616 eldifn ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ¬ 𝑠 ∈ { 0 } )
617 616 502 sylnib ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ¬ 𝑠 = 0 )
618 617 479 syl ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
619 618 mpteq2ia ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ if ( 𝑠 = 0 , 1 , ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
620 612 615 619 3eqtri ⊢ ( 𝐾 ↾ ( ( - π [,] π ) ∖ { 0 } ) ) = ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
621 restabs ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) ∧ ( - π [,] π ) ∈ V ) → ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) )
622 453 613 454 621 mp3an ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) )
623 622 oveq1i ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) )
624 623 fveq1i ⊢ ( ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( topGen ‘ ran (,) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 )
625 611 620 624 3eltr4g ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 𝐾 ↾ ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
626 452 613 pm3.2i ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ Top ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) )
627 626 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ Top ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) ) )
628 ssdif ⊢ ( ( - π [,] π ) ⊆ ℝ → ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) )
629 427 628 ax-mp ⊢ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } )
630 629 541 sselid ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( ℝ ∖ { 0 } ) )
631 sscon ⊢ ( { 0 } ⊆ ( - π [,] π ) → ( ℝ ∖ ( - π [,] π ) ) ⊆ ( ℝ ∖ { 0 } ) )
632 436 631 ax-mp ⊢ ( ℝ ∖ ( - π [,] π ) ) ⊆ ( ℝ ∖ { 0 } )
633 629 632 unssi ⊢ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ⊆ ( ℝ ∖ { 0 } )
634 simpr ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( - π [,] π ) )
635 eldifn ⊢ ( 𝑠 ∈ ( ℝ ∖ { 0 } ) → ¬ 𝑠 ∈ { 0 } )
636 635 adantr ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ 𝑠 ∈ ( - π [,] π ) ) → ¬ 𝑠 ∈ { 0 } )
637 634 636 eldifd ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) )
638 elun1 ⊢ ( 𝑠 ∈ ( ( - π [,] π ) ∖ { 0 } ) → 𝑠 ∈ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) )
639 637 638 syl ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) )
640 eldifi ⊢ ( 𝑠 ∈ ( ℝ ∖ { 0 } ) → 𝑠 ∈ ℝ )
641 640 adantr ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ ¬ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ℝ )
642 simpr ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ ¬ 𝑠 ∈ ( - π [,] π ) ) → ¬ 𝑠 ∈ ( - π [,] π ) )
643 641 642 eldifd ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ ¬ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( ℝ ∖ ( - π [,] π ) ) )
644 elun2 ⊢ ( 𝑠 ∈ ( ℝ ∖ ( - π [,] π ) ) → 𝑠 ∈ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) )
645 643 644 syl ⊢ ( ( 𝑠 ∈ ( ℝ ∖ { 0 } ) ∧ ¬ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) )
646 639 645 pm2.61dan ⊢ ( 𝑠 ∈ ( ℝ ∖ { 0 } ) → 𝑠 ∈ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) )
647 646 ssriv ⊢ ( ℝ ∖ { 0 } ) ⊆ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) )
648 633 647 eqssi ⊢ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) = ( ℝ ∖ { 0 } )
649 648 fveq2i ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ℝ ∖ { 0 } ) )
650 61 cldopn ⊢ ( { 0 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) → ( ℝ ∖ { 0 } ) ∈ ( topGen ‘ ran (,) ) )
651 59 650 ax-mp ⊢ ( ℝ ∖ { 0 } ) ∈ ( topGen ‘ ran (,) )
652 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ℝ ∖ { 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ℝ ∖ { 0 } ) ) = ( ℝ ∖ { 0 } ) )
653 453 651 652 mp2an ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ℝ ∖ { 0 } ) ) = ( ℝ ∖ { 0 } )
654 649 653 eqtri ⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) = ( ℝ ∖ { 0 } )
655 630 654 eleqtrrdi ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) )
656 655 537 elind ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) ∩ ( - π [,] π ) ) )
657 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) )
658 61 657 restntr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( - π [,] π ) ⊆ ℝ ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) ∩ ( - π [,] π ) ) )
659 453 427 613 658 mp3an ⊢ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( ( - π [,] π ) ∖ { 0 } ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( ( - π [,] π ) ∖ { 0 } ) ∪ ( ℝ ∖ ( - π [,] π ) ) ) ) ∩ ( - π [,] π ) )
660 656 659 eleqtrrdi ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( ( - π [,] π ) ∖ { 0 } ) ) )
661 14 a1i ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝐾 : ( - π [,] π ) ⟶ ℂ )
662 451 toponunii ⊢ ( - π [,] π ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) )
663 662 596 cnprest ⊢ ( ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ Top ∧ ( ( - π [,] π ) ∖ { 0 } ) ⊆ ( - π [,] π ) ) ∧ ( 𝑠 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ) ‘ ( ( - π [,] π ) ∖ { 0 } ) ) ∧ 𝐾 : ( - π [,] π ) ⟶ ℂ ) ) → ( 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝐾 ↾ ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
664 627 660 661 663 syl12anc ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → ( 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝐾 ↾ ( ( - π [,] π ) ∖ { 0 } ) ) ∈ ( ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ↾t ( ( - π [,] π ) ∖ { 0 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
665 625 664 mpbird ⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ ¬ 𝑠 = 0 ) → 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
666 536 665 pm2.61dan ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
667 666 rgen ⊢ ∀ 𝑠 ∈ ( - π [,] π ) 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 )
668 cncnp ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) ∈ ( TopOn ‘ ( - π [,] π ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐾 ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐾 : ( - π [,] π ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( - π [,] π ) 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
669 451 605 668 mp2an ⊢ ( 𝐾 ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐾 : ( - π [,] π ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( - π [,] π ) 𝐾 ∈ ( ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
670 14 667 669 mpbir2an ⊢ 𝐾 ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) )
671 57 532 599 cncfcn ⊢ ( ( ( - π [,] π ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( - π [,] π ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) ) )
672 517 144 671 mp2an ⊢ ( ( - π [,] π ) –cn→ ℂ ) = ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) )
673 672 eqcomi ⊢ ( ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( - π [,] π ) –cn→ ℂ )
674 670 673 eleqtri ⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ )
675 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ ) ) → ( 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) ↔ 𝐾 : ( - π [,] π ) ⟶ ℝ ) )
676 12 674 675 mp2an ⊢ ( 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) ↔ 𝐾 : ( - π [,] π ) ⟶ ℝ )
677 11 676 mpbir ⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ )