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