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