Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem18.n |
|- ( ph -> N e. RR ) |
2 |
|
fourierdlem18.s |
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
3 |
|
resincncf |
|- ( sin |` RR ) e. ( RR -cn-> RR ) |
4 |
|
cncff |
|- ( ( sin |` RR ) e. ( RR -cn-> RR ) -> ( sin |` RR ) : RR --> RR ) |
5 |
3 4
|
ax-mp |
|- ( sin |` RR ) : RR --> RR |
6 |
|
halfre |
|- ( 1 / 2 ) e. RR |
7 |
6
|
a1i |
|- ( ph -> ( 1 / 2 ) e. RR ) |
8 |
1 7
|
readdcld |
|- ( ph -> ( N + ( 1 / 2 ) ) e. RR ) |
9 |
8
|
adantr |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( N + ( 1 / 2 ) ) e. RR ) |
10 |
|
pire |
|- _pi e. RR |
11 |
10
|
renegcli |
|- -u _pi e. RR |
12 |
|
iccssre |
|- ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR ) |
13 |
11 10 12
|
mp2an |
|- ( -u _pi [,] _pi ) C_ RR |
14 |
13
|
sseli |
|- ( s e. ( -u _pi [,] _pi ) -> s e. RR ) |
15 |
14
|
adantl |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> s e. RR ) |
16 |
9 15
|
remulcld |
|- ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( ( N + ( 1 / 2 ) ) x. s ) e. RR ) |
17 |
|
eqid |
|- ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) |
18 |
16 17
|
fmptd |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) : ( -u _pi [,] _pi ) --> RR ) |
19 |
|
fcompt |
|- ( ( ( sin |` RR ) : RR --> RR /\ ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) : ( -u _pi [,] _pi ) --> RR ) -> ( ( sin |` RR ) o. ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) ) ) ) |
20 |
5 18 19
|
sylancr |
|- ( ph -> ( ( sin |` RR ) o. ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) ) ) ) |
21 |
|
eqidd |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
22 |
|
oveq2 |
|- ( s = x -> ( ( N + ( 1 / 2 ) ) x. s ) = ( ( N + ( 1 / 2 ) ) x. x ) ) |
23 |
22
|
adantl |
|- ( ( ( ph /\ x e. ( -u _pi [,] _pi ) ) /\ s = x ) -> ( ( N + ( 1 / 2 ) ) x. s ) = ( ( N + ( 1 / 2 ) ) x. x ) ) |
24 |
|
simpr |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> x e. ( -u _pi [,] _pi ) ) |
25 |
8
|
adantr |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( N + ( 1 / 2 ) ) e. RR ) |
26 |
13 24
|
sseldi |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR ) |
27 |
25 26
|
remulcld |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( N + ( 1 / 2 ) ) x. x ) e. RR ) |
28 |
21 23 24 27
|
fvmptd |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) = ( ( N + ( 1 / 2 ) ) x. x ) ) |
29 |
28
|
fveq2d |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( sin |` RR ) ` ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) ) = ( ( sin |` RR ) ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) |
30 |
29
|
mpteq2dva |
|- ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) ) |
31 |
|
fvres |
|- ( ( ( N + ( 1 / 2 ) ) x. x ) e. RR -> ( ( sin |` RR ) ` ( ( N + ( 1 / 2 ) ) x. x ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) |
32 |
27 31
|
syl |
|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( ( sin |` RR ) ` ( ( N + ( 1 / 2 ) ) x. x ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) |
33 |
32
|
mpteq2dva |
|- ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) ) |
34 |
|
oveq2 |
|- ( x = s -> ( ( N + ( 1 / 2 ) ) x. x ) = ( ( N + ( 1 / 2 ) ) x. s ) ) |
35 |
34
|
fveq2d |
|- ( x = s -> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
36 |
35
|
cbvmptv |
|- ( x e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
37 |
36
|
a1i |
|- ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) ) |
38 |
30 33 37
|
3eqtrd |
|- ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( ( sin |` RR ) ` ( ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ` x ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) ) |
39 |
2
|
eqcomi |
|- ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) = S |
40 |
39
|
a1i |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) = S ) |
41 |
20 38 40
|
3eqtrrd |
|- ( ph -> S = ( ( sin |` RR ) o. ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ) ) |
42 |
|
ax-resscn |
|- RR C_ CC |
43 |
13 42
|
sstri |
|- ( -u _pi [,] _pi ) C_ CC |
44 |
43
|
a1i |
|- ( ph -> ( -u _pi [,] _pi ) C_ CC ) |
45 |
1
|
recnd |
|- ( ph -> N e. CC ) |
46 |
|
halfcn |
|- ( 1 / 2 ) e. CC |
47 |
46
|
a1i |
|- ( ph -> ( 1 / 2 ) e. CC ) |
48 |
45 47
|
addcld |
|- ( ph -> ( N + ( 1 / 2 ) ) e. CC ) |
49 |
|
ssid |
|- CC C_ CC |
50 |
49
|
a1i |
|- ( ph -> CC C_ CC ) |
51 |
44 48 50
|
constcncfg |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> ( N + ( 1 / 2 ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) |
52 |
44 50
|
idcncfg |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> s ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) |
53 |
51 52
|
mulcncf |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) |
54 |
|
ssid |
|- ( -u _pi [,] _pi ) C_ ( -u _pi [,] _pi ) |
55 |
54
|
a1i |
|- ( ph -> ( -u _pi [,] _pi ) C_ ( -u _pi [,] _pi ) ) |
56 |
42
|
a1i |
|- ( ph -> RR C_ CC ) |
57 |
17 53 55 56 16
|
cncfmptssg |
|- ( ph -> ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) ) |
58 |
3
|
a1i |
|- ( ph -> ( sin |` RR ) e. ( RR -cn-> RR ) ) |
59 |
57 58
|
cncfco |
|- ( ph -> ( ( sin |` RR ) o. ( s e. ( -u _pi [,] _pi ) |-> ( ( N + ( 1 / 2 ) ) x. s ) ) ) e. ( ( -u _pi [,] _pi ) -cn-> RR ) ) |
60 |
41 59
|
eqeltrd |
|- ( ph -> S e. ( ( -u _pi [,] _pi ) -cn-> RR ) ) |