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