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 0 π cos A = 0 A = π 2

Proof

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