Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem56.k |
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
2 |
|
fourierdlem56.a |
|- ( ph -> ( A (,) B ) C_ ( ( -u _pi [,] _pi ) \ { 0 } ) ) |
3 |
|
fourierdlem56.r4 |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 ) |
4 |
2
|
difss2d |
|- ( ph -> ( A (,) B ) C_ ( -u _pi [,] _pi ) ) |
5 |
4
|
sselda |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( -u _pi [,] _pi ) ) |
6 |
|
1ex |
|- 1 e. _V |
7 |
|
ovex |
|- ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. _V |
8 |
6 7
|
ifex |
|- if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V |
9 |
8
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V ) |
10 |
1
|
fvmpt2 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. _V ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
11 |
5 9 10
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |
12 |
3
|
neneqd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 ) |
13 |
12
|
iffalsed |
|- ( ( ph /\ s e. ( A (,) B ) ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
14 |
|
elioore |
|- ( s e. ( A (,) B ) -> s e. RR ) |
15 |
14
|
adantl |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR ) |
16 |
15
|
recnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC ) |
17 |
16
|
halfcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. CC ) |
18 |
17
|
sincld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. CC ) |
19 |
|
2cnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. CC ) |
20 |
|
fourierdlem44 |
|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
21 |
5 3 20
|
syl2anc |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) =/= 0 ) |
22 |
|
2ne0 |
|- 2 =/= 0 |
23 |
22
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 =/= 0 ) |
24 |
16 18 19 21 23
|
divdiv1d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) = ( s / ( ( sin ` ( s / 2 ) ) x. 2 ) ) ) |
25 |
18 19
|
mulcomd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) x. 2 ) = ( 2 x. ( sin ` ( s / 2 ) ) ) ) |
26 |
25
|
oveq2d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( ( sin ` ( s / 2 ) ) x. 2 ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |
27 |
24 26
|
eqtr2d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) |
28 |
11 13 27
|
3eqtrd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( K ` s ) = ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) |
29 |
28
|
mpteq2dva |
|- ( ph -> ( s e. ( A (,) B ) |-> ( K ` s ) ) = ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) ) |
30 |
29
|
oveq2d |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( K ` s ) ) ) = ( RR _D ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) ) ) |
31 |
|
reelprrecn |
|- RR e. { RR , CC } |
32 |
31
|
a1i |
|- ( ph -> RR e. { RR , CC } ) |
33 |
16 18 21
|
divcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / ( sin ` ( s / 2 ) ) ) e. CC ) |
34 |
|
1red |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. RR ) |
35 |
15
|
rehalfcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( s / 2 ) e. RR ) |
36 |
35
|
resincld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. RR ) |
37 |
34 36
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 x. ( sin ` ( s / 2 ) ) ) e. RR ) |
38 |
35
|
recoscld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. RR ) |
39 |
34
|
rehalfcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / 2 ) e. RR ) |
40 |
38 39
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) e. RR ) |
41 |
40 15
|
remulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) e. RR ) |
42 |
37 41
|
resubcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) e. RR ) |
43 |
36
|
resqcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) ^ 2 ) e. RR ) |
44 |
|
2z |
|- 2 e. ZZ |
45 |
44
|
a1i |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 2 e. ZZ ) |
46 |
18 21 45
|
expne0d |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( sin ` ( s / 2 ) ) ^ 2 ) =/= 0 ) |
47 |
42 43 46
|
redivcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) e. RR ) |
48 |
|
1cnd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. CC ) |
49 |
|
recn |
|- ( s e. RR -> s e. CC ) |
50 |
49
|
adantl |
|- ( ( ph /\ s e. RR ) -> s e. CC ) |
51 |
|
1red |
|- ( ( ph /\ s e. RR ) -> 1 e. RR ) |
52 |
32
|
dvmptid |
|- ( ph -> ( RR _D ( s e. RR |-> s ) ) = ( s e. RR |-> 1 ) ) |
53 |
|
ioossre |
|- ( A (,) B ) C_ RR |
54 |
53
|
a1i |
|- ( ph -> ( A (,) B ) C_ RR ) |
55 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
56 |
55
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
57 |
|
iooretop |
|- ( A (,) B ) e. ( topGen ` ran (,) ) |
58 |
57
|
a1i |
|- ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) ) |
59 |
32 50 51 52 54 56 55 58
|
dvmptres |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) ) |
60 |
|
elsni |
|- ( ( sin ` ( s / 2 ) ) e. { 0 } -> ( sin ` ( s / 2 ) ) = 0 ) |
61 |
60
|
necon3ai |
|- ( ( sin ` ( s / 2 ) ) =/= 0 -> -. ( sin ` ( s / 2 ) ) e. { 0 } ) |
62 |
21 61
|
syl |
|- ( ( ph /\ s e. ( A (,) B ) ) -> -. ( sin ` ( s / 2 ) ) e. { 0 } ) |
63 |
18 62
|
eldifd |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( sin ` ( s / 2 ) ) e. ( CC \ { 0 } ) ) |
64 |
17
|
coscld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( cos ` ( s / 2 ) ) e. CC ) |
65 |
48
|
halfcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 1 / 2 ) e. CC ) |
66 |
64 65
|
mulcld |
|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) e. CC ) |
67 |
|
cnelprrecn |
|- CC e. { RR , CC } |
68 |
67
|
a1i |
|- ( ph -> CC e. { RR , CC } ) |
69 |
|
sinf |
|- sin : CC --> CC |
70 |
69
|
a1i |
|- ( ph -> sin : CC --> CC ) |
71 |
70
|
ffvelrnda |
|- ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC ) |
72 |
|
cosf |
|- cos : CC --> CC |
73 |
72
|
a1i |
|- ( ph -> cos : CC --> CC ) |
74 |
73
|
ffvelrnda |
|- ( ( ph /\ x e. CC ) -> ( cos ` x ) e. CC ) |
75 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
76 |
22
|
a1i |
|- ( ph -> 2 =/= 0 ) |
77 |
32 16 34 59 75 76
|
dvmptdivc |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( s / 2 ) ) ) = ( s e. ( A (,) B ) |-> ( 1 / 2 ) ) ) |
78 |
|
ffn |
|- ( sin : CC --> CC -> sin Fn CC ) |
79 |
69 78
|
ax-mp |
|- sin Fn CC |
80 |
|
dffn5 |
|- ( sin Fn CC <-> sin = ( x e. CC |-> ( sin ` x ) ) ) |
81 |
79 80
|
mpbi |
|- sin = ( x e. CC |-> ( sin ` x ) ) |
82 |
81
|
eqcomi |
|- ( x e. CC |-> ( sin ` x ) ) = sin |
83 |
82
|
oveq2i |
|- ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( CC _D sin ) |
84 |
|
dvsin |
|- ( CC _D sin ) = cos |
85 |
|
ffn |
|- ( cos : CC --> CC -> cos Fn CC ) |
86 |
72 85
|
ax-mp |
|- cos Fn CC |
87 |
|
dffn5 |
|- ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) ) |
88 |
86 87
|
mpbi |
|- cos = ( x e. CC |-> ( cos ` x ) ) |
89 |
83 84 88
|
3eqtri |
|- ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) |
90 |
89
|
a1i |
|- ( ph -> ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) ) |
91 |
|
fveq2 |
|- ( x = ( s / 2 ) -> ( sin ` x ) = ( sin ` ( s / 2 ) ) ) |
92 |
|
fveq2 |
|- ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) ) |
93 |
32 68 17 39 71 74 77 90 91 92
|
dvmptco |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( sin ` ( s / 2 ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) ) ) |
94 |
32 16 48 59 63 66 93
|
dvmptdiv |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( s / ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) ) ) |
95 |
32 33 47 94 75 76
|
dvmptdivc |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( s / ( sin ` ( s / 2 ) ) ) / 2 ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) ) |
96 |
14
|
recnd |
|- ( s e. ( A (,) B ) -> s e. CC ) |
97 |
96
|
halfcld |
|- ( s e. ( A (,) B ) -> ( s / 2 ) e. CC ) |
98 |
97
|
sincld |
|- ( s e. ( A (,) B ) -> ( sin ` ( s / 2 ) ) e. CC ) |
99 |
98
|
mulid2d |
|- ( s e. ( A (,) B ) -> ( 1 x. ( sin ` ( s / 2 ) ) ) = ( sin ` ( s / 2 ) ) ) |
100 |
97
|
coscld |
|- ( s e. ( A (,) B ) -> ( cos ` ( s / 2 ) ) e. CC ) |
101 |
|
2cnd |
|- ( s e. ( A (,) B ) -> 2 e. CC ) |
102 |
22
|
a1i |
|- ( s e. ( A (,) B ) -> 2 =/= 0 ) |
103 |
100 101 102
|
divrecd |
|- ( s e. ( A (,) B ) -> ( ( cos ` ( s / 2 ) ) / 2 ) = ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) ) |
104 |
103
|
eqcomd |
|- ( s e. ( A (,) B ) -> ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) = ( ( cos ` ( s / 2 ) ) / 2 ) ) |
105 |
104
|
oveq1d |
|- ( s e. ( A (,) B ) -> ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) = ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) |
106 |
99 105
|
oveq12d |
|- ( s e. ( A (,) B ) -> ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) = ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) ) |
107 |
106
|
oveq1d |
|- ( s e. ( A (,) B ) -> ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) = ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) ) |
108 |
107
|
oveq1d |
|- ( s e. ( A (,) B ) -> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) = ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) |
109 |
108
|
mpteq2ia |
|- ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) |
110 |
109
|
a1i |
|- ( ph -> ( s e. ( A (,) B ) |-> ( ( ( ( 1 x. ( sin ` ( s / 2 ) ) ) - ( ( ( cos ` ( s / 2 ) ) x. ( 1 / 2 ) ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) ) |
111 |
30 95 110
|
3eqtrd |
|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( K ` s ) ) ) = ( s e. ( A (,) B ) |-> ( ( ( ( sin ` ( s / 2 ) ) - ( ( ( cos ` ( s / 2 ) ) / 2 ) x. s ) ) / ( ( sin ` ( s / 2 ) ) ^ 2 ) ) / 2 ) ) ) |