Metamath Proof Explorer

Theorem coseq00topi

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

Ref Expression
Assertion coseq00topi 
|- ( A e. ( 0 [,] _pi ) -> ( ( cos ` A ) = 0 <-> A = ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) -> ( cos ` A ) = 0 )
2 0re 
 |-  0 e. RR
3 pire 
 |-  _pi e. RR
4 2 3 elicc2i 
 |-  ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
5 4 birani 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) )
6 5 simp1d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> A e. RR )
7 6 ad2antrr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> A e. RR )
8 simpr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> 0 < A )
9 simplr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> A < ( _pi / 2 ) )
10 2 rexri 
 |-  0 e. RR*
11 halfpire 
 |-  ( _pi / 2 ) e. RR
12 11 rexri 
 |-  ( _pi / 2 ) e. RR*
13 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) ) )
14 10 12 13 mp2an 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) <-> ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) )
15 7 8 9 14 syl3anbrc 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> A e. ( 0 (,) ( _pi / 2 ) ) )
16 sincosq1sgn 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
17 15 16 syl 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
18 17 simprd 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> 0 < ( cos ` A ) )
19 18 gt0ne0d 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 < A ) -> ( cos ` A ) =/= 0 )
20 simpr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 = A ) -> 0 = A )
21 20 fveq2d 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 = A ) -> ( cos ` 0 ) = ( cos ` A ) )
22 cos0 
 |-  ( cos ` 0 ) = 1
23 21 22 eqtr3di 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 = A ) -> ( cos ` A ) = 1 )
24 ax-1ne0 
 |-  1 =/= 0
25 24 a1i 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 = A ) -> 1 =/= 0 )
26 23 25 eqnetrd 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) /\ 0 = A ) -> ( cos ` A ) =/= 0 )
27 5 simp2d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> 0 <_ A )
28 0red 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> 0 e. RR )
29 28 6 leloed 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
30 27 29 mpbid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( 0 < A \/ 0 = A ) )
31 30 adantr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) -> ( 0 < A \/ 0 = A ) )
32 19 26 31 mpjaodan 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) -> ( cos ` A ) =/= 0 )
33 1 32 pm2.21ddne 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A < ( _pi / 2 ) ) -> A = ( _pi / 2 ) )
34 simpr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ A = ( _pi / 2 ) ) -> A = ( _pi / 2 ) )
35 simplr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) -> ( cos ` A ) = 0 )
36 6 ad2antrr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> A e. RR )
37 simplr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> ( _pi / 2 ) < A )
38 simpr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> A < _pi )
39 3 rexri 
 |-  _pi e. RR*
40 elioo2 
 |-  ( ( ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( A e. ( ( _pi / 2 ) (,) _pi ) <-> ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) ) )
41 12 39 40 mp2an 
 |-  ( A e. ( ( _pi / 2 ) (,) _pi ) <-> ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) )
42 36 37 38 41 syl3anbrc 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> A e. ( ( _pi / 2 ) (,) _pi ) )
43 sincosq2sgn 
 |-  ( A e. ( ( _pi / 2 ) (,) _pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
44 42 43 syl 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
45 44 simprd 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> ( cos ` A ) < 0 )
46 45 lt0ne0d 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A < _pi ) -> ( cos ` A ) =/= 0 )
47 simpr 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A = _pi ) -> A = _pi )
48 47 fveq2d 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A = _pi ) -> ( cos ` A ) = ( cos ` _pi ) )
49 cospi 
 |-  ( cos ` _pi ) = -u 1
50 48 49 eqtrdi 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A = _pi ) -> ( cos ` A ) = -u 1 )
51 neg1ne0 
 |-  -u 1 =/= 0
52 51 a1i 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A = _pi ) -> -u 1 =/= 0 )
53 50 52 eqnetrd 
 |-  ( ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) /\ A = _pi ) -> ( cos ` A ) =/= 0 )
54 5 simp3d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> A <_ _pi )
55 3 a1i 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> _pi e. RR )
56 6 55 leloed 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( A <_ _pi <-> ( A < _pi \/ A = _pi ) ) )
57 54 56 mpbid 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( A < _pi \/ A = _pi ) )
58 57 adantr 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) -> ( A < _pi \/ A = _pi ) )
59 46 53 58 mpjaodan 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) -> ( cos ` A ) =/= 0 )
60 35 59 pm2.21ddne 
 |-  ( ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) /\ ( _pi / 2 ) < A ) -> A = ( _pi / 2 ) )
61 55 rehalfcld 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( _pi / 2 ) e. RR )
62 6 61 lttri4d 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> ( A < ( _pi / 2 ) \/ A = ( _pi / 2 ) \/ ( _pi / 2 ) < A ) )
63 33 34 60 62 mpjao3dan 
 |-  ( ( A e. ( 0 [,] _pi ) /\ ( cos ` A ) = 0 ) -> A = ( _pi / 2 ) )
64 fveq2 
 |-  ( A = ( _pi / 2 ) -> ( cos ` A ) = ( cos ` ( _pi / 2 ) ) )
65 coshalfpi 
 |-  ( cos ` ( _pi / 2 ) ) = 0
66 64 65 eqtrdi 
 |-  ( A = ( _pi / 2 ) -> ( cos ` A ) = 0 )
67 66 adantl 
 |-  ( ( A e. ( 0 [,] _pi ) /\ A = ( _pi / 2 ) ) -> ( cos ` A ) = 0 )
68 63 67 impbida 
 |-  ( A e. ( 0 [,] _pi ) -> ( ( cos ` A ) = 0 <-> A = ( _pi / 2 ) ) )