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 ( 𝐴 ∈ ( 0 [,] π ) → ( ( cos ‘ 𝐴 ) = 0 ↔ 𝐴 = ( π / 2 ) ) )

Proof

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