| 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 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
| 57 |
56
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
| 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 57 56 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
|
mulid2d |
⊢ ( 𝑥 ∈ ℝ → ( 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 57 56 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
|
ffvelrnda |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 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 |
56 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 56 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 |
57
|
oveq1i |
⊢ ( ( topGen ‘ ran (,) ) ↾t ( - π [,] π ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ↾t ( - π [,] π ) ) |
| 528 |
56
|
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 |
56 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 |
|
cncffvrn |
⊢ ( ( ( ℂ ∖ { 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 |
57
|
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 |
56 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 |
56
|
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 |
56 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 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℂ ) ) → ( 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) ↔ 𝐾 : ( - π [,] π ) ⟶ ℝ ) ) |
| 676 |
12 674 675
|
mp2an |
⊢ ( 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) ↔ 𝐾 : ( - π [,] π ) ⟶ ℝ ) |
| 677 |
11 676
|
mpbir |
⊢ 𝐾 ∈ ( ( - π [,] π ) –cn→ ℝ ) |