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