Metamath Proof Explorer

Theorem coseq0negpitopi

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

Ref Expression
Assertion coseq0negpitopi ( 𝐴 ∈ ( - π (,] π ) → ( ( cos ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } ) )

Proof

Step Hyp Ref Expression
1 pire ⊢ π ∈ ℝ
2 1 renegcli ⊢ - π ∈ ℝ
3 2 rexri ⊢ - π ∈ ℝ*
4 elioc2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( 𝐴 ∈ ( - π (,] π ) ↔ ( 𝐴 ∈ ℝ ∧ - π < 𝐴 ∧ 𝐴 ≤ π ) ) )
5 3 1 4 mp2an ⊢ ( 𝐴 ∈ ( - π (,] π ) ↔ ( 𝐴 ∈ ℝ ∧ - π < 𝐴 ∧ 𝐴 ≤ π ) )
6 5 birani ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → ( 𝐴 ∈ ℝ ∧ - π < 𝐴 ∧ 𝐴 ≤ π ) )
7 6 simp1d ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℝ )
8 0re ⊢ 0 ∈ ℝ
9 8 a1i ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → 0 ∈ ℝ )
10 7 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℝ )
11 10 recnd ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℂ )
12 7 recnd ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
13 12 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℂ )
14 cosneg ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
15 13 14 syl ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
16 simplr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → ( cos ‘ 𝐴 ) = 0 )
17 15 16 eqtrd ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → ( cos ‘ - 𝐴 ) = 0 )
18 7 renegcld ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → - 𝐴 ∈ ℝ )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → - 𝐴 ∈ ℝ )
20 simpr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ≤ 0 )
21 10 le0neg1d ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 ≤ 0 ↔ 0 ≤ - 𝐴 ) )
22 20 21 mpbid ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 0 ≤ - 𝐴 )
23 1 a1i ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → π ∈ ℝ )
24 6 simp2d ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → - π < 𝐴 )
25 23 7 24 ltnegcon1d ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → - 𝐴 < π )
26 18 23 25 ltled ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → - 𝐴 ≤ π )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → - 𝐴 ≤ π )
28 8 1 elicc2i ⊢ ( - 𝐴 ∈ ( 0 [,] π ) ↔ ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ∧ - 𝐴 ≤ π ) )
29 19 22 27 28 syl3anbrc ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → - 𝐴 ∈ ( 0 [,] π ) )
30 coseq00topi ⊢ ( - 𝐴 ∈ ( 0 [,] π ) → ( ( cos ‘ - 𝐴 ) = 0 ↔ - 𝐴 = ( π / 2 ) ) )
31 29 30 syl ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → ( ( cos ‘ - 𝐴 ) = 0 ↔ - 𝐴 = ( π / 2 ) ) )
32 17 31 mpbid ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → - 𝐴 = ( π / 2 ) )
33 11 32 negcon1ad ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → - ( π / 2 ) = 𝐴 )
34 33 eqcomd ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 = - ( π / 2 ) )
35 halfpire ⊢ ( π / 2 ) ∈ ℝ
36 35 renegcli ⊢ - ( π / 2 ) ∈ ℝ
37 prid2g ⊢ ( - ( π / 2 ) ∈ ℝ → - ( π / 2 ) ∈ { ( π / 2 ) , - ( π / 2 ) } )
38 eleq1a ⊢ ( - ( π / 2 ) ∈ { ( π / 2 ) , - ( π / 2 ) } → ( 𝐴 = - ( π / 2 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
39 36 37 38 mp2b ⊢ ( 𝐴 = - ( π / 2 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } )
40 34 39 syl ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } )
41 simplr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → ( cos ‘ 𝐴 ) = 0 )
42 7 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
43 simpr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 0 ≤ 𝐴 )
44 6 simp3d ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → 𝐴 ≤ π )
45 44 adantr ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ≤ π )
46 8 1 elicc2i ⊢ ( 𝐴 ∈ ( 0 [,] π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ π ) )
47 42 43 45 46 syl3anbrc ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] π ) )
48 coseq00topi ⊢ ( 𝐴 ∈ ( 0 [,] π ) → ( ( cos ‘ 𝐴 ) = 0 ↔ 𝐴 = ( π / 2 ) ) )
49 47 48 syl ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → ( ( cos ‘ 𝐴 ) = 0 ↔ 𝐴 = ( π / 2 ) ) )
50 41 49 mpbid ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 = ( π / 2 ) )
51 prid1g ⊢ ( ( π / 2 ) ∈ ℝ → ( π / 2 ) ∈ { ( π / 2 ) , - ( π / 2 ) } )
52 eleq1a ⊢ ( ( π / 2 ) ∈ { ( π / 2 ) , - ( π / 2 ) } → ( 𝐴 = ( π / 2 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
53 35 51 52 mp2b ⊢ ( 𝐴 = ( π / 2 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } )
54 50 53 syl ⊢ ( ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } )
55 7 9 40 54 lecasei ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ ( cos ‘ 𝐴 ) = 0 ) → 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } )
56 elpri ⊢ ( 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } → ( 𝐴 = ( π / 2 ) ∨ 𝐴 = - ( π / 2 ) ) )
57 fveq2 ⊢ ( 𝐴 = ( π / 2 ) → ( cos ‘ 𝐴 ) = ( cos ‘ ( π / 2 ) ) )
58 coshalfpi ⊢ ( cos ‘ ( π / 2 ) ) = 0
59 57 58 eqtrdi ⊢ ( 𝐴 = ( π / 2 ) → ( cos ‘ 𝐴 ) = 0 )
60 fveq2 ⊢ ( 𝐴 = - ( π / 2 ) → ( cos ‘ 𝐴 ) = ( cos ‘ - ( π / 2 ) ) )
61 cosneghalfpi ⊢ ( cos ‘ - ( π / 2 ) ) = 0
62 60 61 eqtrdi ⊢ ( 𝐴 = - ( π / 2 ) → ( cos ‘ 𝐴 ) = 0 )
63 59 62 jaoi ⊢ ( ( 𝐴 = ( π / 2 ) ∨ 𝐴 = - ( π / 2 ) ) → ( cos ‘ 𝐴 ) = 0 )
64 56 63 syl ⊢ ( 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } → ( cos ‘ 𝐴 ) = 0 )
65 64 adantl ⊢ ( ( 𝐴 ∈ ( - π (,] π ) ∧ 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( cos ‘ 𝐴 ) = 0 )
66 55 65 impbida ⊢ ( 𝐴 ∈ ( - π (,] π ) → ( ( cos ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ { ( π / 2 ) , - ( π / 2 ) } ) )