Metamath Proof Explorer

Theorem fourierdlem43

Description: K is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem43.1 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
Assertion fourierdlem43 
|- K : ( -u _pi [,] _pi ) --> RR

Proof

Step Hyp Ref Expression
1 fourierdlem43.1 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
2 1red 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s = 0 ) -> 1 e. RR )
3 pire 
 |-  _pi e. RR
4 3 a1i 
 |-  ( s e. ( -u _pi [,] _pi ) -> _pi e. RR )
5 4 renegcld 
 |-  ( s e. ( -u _pi [,] _pi ) -> -u _pi e. RR )
6 id 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. ( -u _pi [,] _pi ) )
7 eliccre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ s e. ( -u _pi [,] _pi ) ) -> s e. RR )
8 5 4 6 7 syl3anc 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. RR )
9 8 adantr 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. RR )
10 2re 
 |-  2 e. RR
11 10 a1i 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> 2 e. RR )
12 9 rehalfcld 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( s / 2 ) e. RR )
13 12 resincld 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) e. RR )
14 11 13 remulcld 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
15 2cnd 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> 2 e. CC )
16 13 recnd 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) e. CC )
17 2ne0 
 |-  2 =/= 0
18 17 a1i 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> 2 =/= 0 )
19 0xr 
 |-  0 e. RR*
20 19 a1i 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> 0 e. RR* )
21 10 3 remulcli 
 |-  ( 2 x. _pi ) e. RR
22 21 rexri 
 |-  ( 2 x. _pi ) e. RR*
23 22 a1i 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> ( 2 x. _pi ) e. RR* )
24 8 adantr 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> s e. RR )
25 simpr 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> 0 < s )
26 21 a1i 
 |-  ( s e. ( -u _pi [,] _pi ) -> ( 2 x. _pi ) e. RR )
27 5 rexrd 
 |-  ( s e. ( -u _pi [,] _pi ) -> -u _pi e. RR* )
28 4 rexrd 
 |-  ( s e. ( -u _pi [,] _pi ) -> _pi e. RR* )
29 iccleub 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi [,] _pi ) ) -> s <_ _pi )
30 27 28 6 29 syl3anc 
 |-  ( s e. ( -u _pi [,] _pi ) -> s <_ _pi )
31 pirp 
 |-  _pi e. RR+
32 2timesgt 
 |-  ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
33 31 32 ax-mp 
 |-  _pi < ( 2 x. _pi )
34 33 a1i 
 |-  ( s e. ( -u _pi [,] _pi ) -> _pi < ( 2 x. _pi ) )
35 8 4 26 30 34 lelttrd 
 |-  ( s e. ( -u _pi [,] _pi ) -> s < ( 2 x. _pi ) )
36 35 adantr 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> s < ( 2 x. _pi ) )
37 20 23 24 25 36 eliood 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> s e. ( 0 (,) ( 2 x. _pi ) ) )
38 sinaover2ne0 
 |-  ( s e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
39 37 38 syl 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ 0 < s ) -> ( sin ` ( s / 2 ) ) =/= 0 )
40 39 adantlr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ 0 < s ) -> ( sin ` ( s / 2 ) ) =/= 0 )
41 8 ad2antrr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> s e. RR )
42 iccgelb 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi [,] _pi ) ) -> -u _pi <_ s )
43 27 28 6 42 syl3anc 
 |-  ( s e. ( -u _pi [,] _pi ) -> -u _pi <_ s )
44 43 ad2antrr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> -u _pi <_ s )
45 0red 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> 0 e. RR )
46 neqne 
 |-  ( -. s = 0 -> s =/= 0 )
47 46 ad2antlr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> s =/= 0 )
48 simpr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> -. 0 < s )
49 41 45 47 48 lttri5d 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> s < 0 )
50 5 ad2antrr 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> -u _pi e. RR )
51 elico2 
 |-  ( ( -u _pi e. RR /\ 0 e. RR* ) -> ( s e. ( -u _pi [,) 0 ) <-> ( s e. RR /\ -u _pi <_ s /\ s < 0 ) ) )
52 50 19 51 sylancl 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> ( s e. ( -u _pi [,) 0 ) <-> ( s e. RR /\ -u _pi <_ s /\ s < 0 ) ) )
53 41 44 49 52 mpbir3and 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> s e. ( -u _pi [,) 0 ) )
54 3 renegcli 
 |-  -u _pi e. RR
55 elicore 
 |-  ( ( -u _pi e. RR /\ s e. ( -u _pi [,) 0 ) ) -> s e. RR )
56 54 55 mpan 
 |-  ( s e. ( -u _pi [,) 0 ) -> s e. RR )
57 56 recnd 
 |-  ( s e. ( -u _pi [,) 0 ) -> s e. CC )
58 2cnd 
 |-  ( s e. ( -u _pi [,) 0 ) -> 2 e. CC )
59 17 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> 2 =/= 0 )
60 57 58 59 divnegd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u ( s / 2 ) = ( -u s / 2 ) )
61 60 eqcomd 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( -u s / 2 ) = -u ( s / 2 ) )
62 61 fveq2d 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` ( -u s / 2 ) ) = ( sin ` -u ( s / 2 ) ) )
63 62 negeqd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u ( sin ` ( -u s / 2 ) ) = -u ( sin ` -u ( s / 2 ) ) )
64 57 halfcld 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( s / 2 ) e. CC )
65 sinneg 
 |-  ( ( s / 2 ) e. CC -> ( sin ` -u ( s / 2 ) ) = -u ( sin ` ( s / 2 ) ) )
66 64 65 syl 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` -u ( s / 2 ) ) = -u ( sin ` ( s / 2 ) ) )
67 66 negeqd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u ( sin ` -u ( s / 2 ) ) = -u -u ( sin ` ( s / 2 ) ) )
68 64 sincld 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` ( s / 2 ) ) e. CC )
69 68 negnegd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u -u ( sin ` ( s / 2 ) ) = ( sin ` ( s / 2 ) ) )
70 63 67 69 3eqtrd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u ( sin ` ( -u s / 2 ) ) = ( sin ` ( s / 2 ) ) )
71 57 negcld 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u s e. CC )
72 71 halfcld 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( -u s / 2 ) e. CC )
73 72 sincld 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` ( -u s / 2 ) ) e. CC )
74 19 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> 0 e. RR* )
75 22 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( 2 x. _pi ) e. RR* )
76 56 renegcld 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u s e. RR )
77 54 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u _pi e. RR )
78 77 rexrd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u _pi e. RR* )
79 id 
 |-  ( s e. ( -u _pi [,) 0 ) -> s e. ( -u _pi [,) 0 ) )
80 icoltub 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ s e. ( -u _pi [,) 0 ) ) -> s < 0 )
81 78 74 79 80 syl3anc 
 |-  ( s e. ( -u _pi [,) 0 ) -> s < 0 )
82 56 lt0neg1d 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( s < 0 <-> 0 < -u s ) )
83 81 82 mpbid 
 |-  ( s e. ( -u _pi [,) 0 ) -> 0 < -u s )
84 3 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> _pi e. RR )
85 21 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( 2 x. _pi ) e. RR )
86 icogelb 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ s e. ( -u _pi [,) 0 ) ) -> -u _pi <_ s )
87 78 74 79 86 syl3anc 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u _pi <_ s )
88 84 56 87 lenegcon1d 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u s <_ _pi )
89 33 a1i 
 |-  ( s e. ( -u _pi [,) 0 ) -> _pi < ( 2 x. _pi ) )
90 76 84 85 88 89 lelttrd 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u s < ( 2 x. _pi ) )
91 74 75 76 83 90 eliood 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u s e. ( 0 (,) ( 2 x. _pi ) ) )
92 sinaover2ne0 
 |-  ( -u s e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( -u s / 2 ) ) =/= 0 )
93 91 92 syl 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` ( -u s / 2 ) ) =/= 0 )
94 73 93 negne0d 
 |-  ( s e. ( -u _pi [,) 0 ) -> -u ( sin ` ( -u s / 2 ) ) =/= 0 )
95 70 94 eqnetrrd 
 |-  ( s e. ( -u _pi [,) 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
96 53 95 syl 
 |-  ( ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) /\ -. 0 < s ) -> ( sin ` ( s / 2 ) ) =/= 0 )
97 40 96 pm2.61dan 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
98 15 16 18 97 mulne0d 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
99 9 14 98 redivcld 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
100 2 99 ifclda 
 |-  ( s e. ( -u _pi [,] _pi ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. RR )
101 1 100 fmpti 
 |-  K : ( -u _pi [,] _pi ) --> RR