Metamath Proof Explorer

Theorem fourierdlem18

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

Ref Expression
Hypotheses fourierdlem18.n 
|- ( ph -> N e. RR )
fourierdlem18.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
Assertion fourierdlem18 
|- ( ph -> S e. ( ( -u _pi [,] _pi ) -cn-> RR ) )

Proof

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 ) )