This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem44

Description: A condition for having ( sin( A / 2 ) ) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fourierdlem44 
|- ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) -> ( sin ` ( A / 2 ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> 0 e. RR* )
3 2re 
 |-  2 e. RR
4 pire 
 |-  _pi e. RR
5 3 4 remulcli 
 |-  ( 2 x. _pi ) e. RR
6 5 rexri 
 |-  ( 2 x. _pi ) e. RR*
7 6 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> ( 2 x. _pi ) e. RR* )
8 4 renegcli 
 |-  -u _pi e. RR
9 8 a1i 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u _pi e. RR )
10 4 a1i 
 |-  ( A e. ( -u _pi [,] _pi ) -> _pi e. RR )
11 id 
 |-  ( A e. ( -u _pi [,] _pi ) -> A e. ( -u _pi [,] _pi ) )
12 eliccre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ A e. ( -u _pi [,] _pi ) ) -> A e. RR )
13 9 10 11 12 syl3anc 
 |-  ( A e. ( -u _pi [,] _pi ) -> A e. RR )
14 13 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> A e. RR )
15 simpr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> 0 < A )
16 5 a1i 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( 2 x. _pi ) e. RR )
17 9 rexrd 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u _pi e. RR* )
18 10 rexrd 
 |-  ( A e. ( -u _pi [,] _pi ) -> _pi e. RR* )
19 iccleub 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ A e. ( -u _pi [,] _pi ) ) -> A <_ _pi )
20 17 18 11 19 syl3anc 
 |-  ( A e. ( -u _pi [,] _pi ) -> A <_ _pi )
21 pirp 
 |-  _pi e. RR+
22 2timesgt 
 |-  ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
23 21 22 ax-mp 
 |-  _pi < ( 2 x. _pi )
24 23 a1i 
 |-  ( A e. ( -u _pi [,] _pi ) -> _pi < ( 2 x. _pi ) )
25 13 10 16 20 24 lelttrd 
 |-  ( A e. ( -u _pi [,] _pi ) -> A < ( 2 x. _pi ) )
26 25 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> A < ( 2 x. _pi ) )
27 2 7 14 15 26 eliood 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ 0 < A ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
28 27 adantlr 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ 0 < A ) -> A e. ( 0 (,) ( 2 x. _pi ) ) )
29 sinaover2ne0 
 |-  ( A e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( A / 2 ) ) =/= 0 )
30 28 29 syl 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ 0 < A ) -> ( sin ` ( A / 2 ) ) =/= 0 )
31 simpll 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> A e. ( -u _pi [,] _pi ) )
32 31 13 syl 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> A e. RR )
33 0red 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> 0 e. RR )
34 simplr 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> A =/= 0 )
35 simpr 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> -. 0 < A )
36 32 33 34 35 lttri5d 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> A < 0 )
37 13 recnd 
 |-  ( A e. ( -u _pi [,] _pi ) -> A e. CC )
38 37 halfcld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( A / 2 ) e. CC )
39 sinneg 
 |-  ( ( A / 2 ) e. CC -> ( sin ` -u ( A / 2 ) ) = -u ( sin ` ( A / 2 ) ) )
40 38 39 syl 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( sin ` -u ( A / 2 ) ) = -u ( sin ` ( A / 2 ) ) )
41 2cnd 
 |-  ( A e. ( -u _pi [,] _pi ) -> 2 e. CC )
42 2ne0 
 |-  2 =/= 0
43 42 a1i 
 |-  ( A e. ( -u _pi [,] _pi ) -> 2 =/= 0 )
44 37 41 43 divnegd 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u ( A / 2 ) = ( -u A / 2 ) )
45 44 fveq2d 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( sin ` -u ( A / 2 ) ) = ( sin ` ( -u A / 2 ) ) )
46 40 45 eqtr3d 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u ( sin ` ( A / 2 ) ) = ( sin ` ( -u A / 2 ) ) )
47 46 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u ( sin ` ( A / 2 ) ) = ( sin ` ( -u A / 2 ) ) )
48 1 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> 0 e. RR* )
49 6 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( 2 x. _pi ) e. RR* )
50 13 renegcld 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u A e. RR )
51 50 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u A e. RR )
52 simpr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> A < 0 )
53 13 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> A e. RR )
54 53 lt0neg1d 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( A < 0 <-> 0 < -u A ) )
55 52 54 mpbid 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> 0 < -u A )
56 5 renegcli 
 |-  -u ( 2 x. _pi ) e. RR
57 56 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u ( 2 x. _pi ) e. RR )
58 8 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u _pi e. RR )
59 4 5 ltnegi 
 |-  ( _pi < ( 2 x. _pi ) <-> -u ( 2 x. _pi ) < -u _pi )
60 23 59 mpbi 
 |-  -u ( 2 x. _pi ) < -u _pi
61 60 a1i 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u ( 2 x. _pi ) < -u _pi )
62 iccgelb 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ A e. ( -u _pi [,] _pi ) ) -> -u _pi <_ A )
63 17 18 11 62 syl3anc 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u _pi <_ A )
64 63 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u _pi <_ A )
65 57 58 53 61 64 ltletrd 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u ( 2 x. _pi ) < A )
66 57 53 ltnegd 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( -u ( 2 x. _pi ) < A <-> -u A < -u -u ( 2 x. _pi ) ) )
67 65 66 mpbid 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u A < -u -u ( 2 x. _pi ) )
68 16 recnd 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( 2 x. _pi ) e. CC )
69 68 negnegd 
 |-  ( A e. ( -u _pi [,] _pi ) -> -u -u ( 2 x. _pi ) = ( 2 x. _pi ) )
70 69 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u -u ( 2 x. _pi ) = ( 2 x. _pi ) )
71 67 70 breqtrd 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u A < ( 2 x. _pi ) )
72 48 49 51 55 71 eliood 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u A e. ( 0 (,) ( 2 x. _pi ) ) )
73 sinaover2ne0 
 |-  ( -u A e. ( 0 (,) ( 2 x. _pi ) ) -> ( sin ` ( -u A / 2 ) ) =/= 0 )
74 72 73 syl 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( sin ` ( -u A / 2 ) ) =/= 0 )
75 47 74 eqnetrd 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -u ( sin ` ( A / 2 ) ) =/= 0 )
76 75 neneqd 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -. -u ( sin ` ( A / 2 ) ) = 0 )
77 38 sincld 
 |-  ( A e. ( -u _pi [,] _pi ) -> ( sin ` ( A / 2 ) ) e. CC )
78 77 adantr 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( sin ` ( A / 2 ) ) e. CC )
79 78 negeq0d 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( ( sin ` ( A / 2 ) ) = 0 <-> -u ( sin ` ( A / 2 ) ) = 0 ) )
80 76 79 mtbird 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> -. ( sin ` ( A / 2 ) ) = 0 )
81 80 neqned 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A < 0 ) -> ( sin ` ( A / 2 ) ) =/= 0 )
82 31 36 81 syl2anc 
 |-  ( ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) /\ -. 0 < A ) -> ( sin ` ( A / 2 ) ) =/= 0 )
83 30 82 pm2.61dan 
 |-  ( ( A e. ( -u _pi [,] _pi ) /\ A =/= 0 ) -> ( sin ` ( A / 2 ) ) =/= 0 )