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 ⊢ A ∈ − π π → cos ⁡ A = 0 ↔ A ∈ π 2 − π 2

Proof

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