coseq0negpitopi

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

		Ref	Expression
	Assertion	coseq0negpitopi	$⊢ A \in (- π, π] \to (\cos A = 0 \leftrightarrow A \in \{\frac{π}{2}, - \frac{π}{2}\})$

Proof

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

Metamath Proof Explorer

Theorem coseq0negpitopi

Proof