Metamath Proof Explorer

Theorem coseq0negpitopi

Description: Location of the zeroes of cosine in ( -upi (,] pi ) . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Assertion coseq0negpitopi 
|- ( A e. ( -u _pi (,] _pi ) -> ( ( cos ` A ) = 0 <-> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 1 renegcli 
 |-  -u _pi e. RR
3 2 rexri 
 |-  -u _pi e. RR*
4 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( A e. ( -u _pi (,] _pi ) <-> ( A e. RR /\ -u _pi < A /\ A <_ _pi ) ) )
5 3 1 4 mp2an 
 |-  ( A e. ( -u _pi (,] _pi ) <-> ( A e. RR /\ -u _pi < A /\ A <_ _pi ) )
6 5 birani 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> ( A e. RR /\ -u _pi < A /\ A <_ _pi ) )
7 6 simp1d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> A e. RR )
8 0re 
 |-  0 e. RR
9 8 a1i 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> 0 e. RR )
10 7 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A e. RR )
11 10 recnd 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A e. CC )
12 7 recnd 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> A e. CC )
13 12 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A e. CC )
14 cosneg 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
15 13 14 syl 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> ( cos ` -u A ) = ( cos ` A ) )
16 simplr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> ( cos ` A ) = 0 )
17 15 16 eqtrd 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> ( cos ` -u A ) = 0 )
18 7 renegcld 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> -u A e. RR )
19 18 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> -u A e. RR )
20 simpr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A <_ 0 )
21 10 le0neg1d 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> ( A <_ 0 <-> 0 <_ -u A ) )
22 20 21 mpbid 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> 0 <_ -u A )
23 1 a1i 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> _pi e. RR )
24 6 simp2d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> -u _pi < A )
25 23 7 24 ltnegcon1d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> -u A < _pi )
26 18 23 25 ltled 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> -u A <_ _pi )
27 26 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> -u A <_ _pi )
28 8 1 elicc2i 
 |-  ( -u A e. ( 0 [,] _pi ) <-> ( -u A e. RR /\ 0 <_ -u A /\ -u A <_ _pi ) )
29 19 22 27 28 syl3anbrc 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> -u A e. ( 0 [,] _pi ) )
30 coseq00topi 
 |-  ( -u A e. ( 0 [,] _pi ) -> ( ( cos ` -u A ) = 0 <-> -u A = ( _pi / 2 ) ) )
31 29 30 syl 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> ( ( cos ` -u A ) = 0 <-> -u A = ( _pi / 2 ) ) )
32 17 31 mpbid 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> -u A = ( _pi / 2 ) )
33 11 32 negcon1ad 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> -u ( _pi / 2 ) = A )
34 33 eqcomd 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A = -u ( _pi / 2 ) )
35 halfpire 
 |-  ( _pi / 2 ) e. RR
36 35 renegcli 
 |-  -u ( _pi / 2 ) e. RR
37 prid2g 
 |-  ( -u ( _pi / 2 ) e. RR -> -u ( _pi / 2 ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
38 eleq1a 
 |-  ( -u ( _pi / 2 ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( A = -u ( _pi / 2 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
39 36 37 38 mp2b 
 |-  ( A = -u ( _pi / 2 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
40 34 39 syl 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ A <_ 0 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
41 simplr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> ( cos ` A ) = 0 )
42 7 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> A e. RR )
43 simpr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> 0 <_ A )
44 6 simp3d 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> A <_ _pi )
45 44 adantr 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> A <_ _pi )
46 8 1 elicc2i 
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
47 42 43 45 46 syl3anbrc 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> A e. ( 0 [,] _pi ) )
48 coseq00topi 
 |-  ( A e. ( 0 [,] _pi ) -> ( ( cos ` A ) = 0 <-> A = ( _pi / 2 ) ) )
49 47 48 syl 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> ( ( cos ` A ) = 0 <-> A = ( _pi / 2 ) ) )
50 41 49 mpbid 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> A = ( _pi / 2 ) )
51 prid1g 
 |-  ( ( _pi / 2 ) e. RR -> ( _pi / 2 ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
52 eleq1a 
 |-  ( ( _pi / 2 ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( A = ( _pi / 2 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
53 35 51 52 mp2b 
 |-  ( A = ( _pi / 2 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
54 50 53 syl 
 |-  ( ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) /\ 0 <_ A ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
55 7 9 40 54 lecasei 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ ( cos ` A ) = 0 ) -> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
56 elpri 
 |-  ( A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( A = ( _pi / 2 ) \/ A = -u ( _pi / 2 ) ) )
57 fveq2 
 |-  ( A = ( _pi / 2 ) -> ( cos ` A ) = ( cos ` ( _pi / 2 ) ) )
58 coshalfpi 
 |-  ( cos ` ( _pi / 2 ) ) = 0
59 57 58 eqtrdi 
 |-  ( A = ( _pi / 2 ) -> ( cos ` A ) = 0 )
60 fveq2 
 |-  ( A = -u ( _pi / 2 ) -> ( cos ` A ) = ( cos ` -u ( _pi / 2 ) ) )
61 cosneghalfpi 
 |-  ( cos ` -u ( _pi / 2 ) ) = 0
62 60 61 eqtrdi 
 |-  ( A = -u ( _pi / 2 ) -> ( cos ` A ) = 0 )
63 59 62 jaoi 
 |-  ( ( A = ( _pi / 2 ) \/ A = -u ( _pi / 2 ) ) -> ( cos ` A ) = 0 )
64 56 63 syl 
 |-  ( A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( cos ` A ) = 0 )
65 64 adantl 
 |-  ( ( A e. ( -u _pi (,] _pi ) /\ A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( cos ` A ) = 0 )
66 55 65 impbida 
 |-  ( A e. ( -u _pi (,] _pi ) -> ( ( cos ` A ) = 0 <-> A e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )