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