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