coseq00topi

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

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

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \to \cos A = 0$
2		0re	$⊢ 0 \in ℝ$
3		pire	$⊢ π \in ℝ$
4	2 3	elicc2i	$⊢ A \in [0, π] \leftrightarrow (A \in ℝ \land 0 \leq A \land A \leq π)$
5	4	birani	$⊢ (A \in [0, π] \land \cos A = 0) \to (A \in ℝ \land 0 \leq A \land A \leq π)$
6	5	simp1d	$⊢ (A \in [0, π] \land \cos A = 0) \to A \in ℝ$
7	6	ad2antrr	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to A \in ℝ$
8		simpr	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to 0 < A$
9		simplr	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to A < \frac{π}{2}$
10	2	rexri	$⊢ 0 \in ℝ^{*}$
11		halfpire	$⊢ \frac{π}{2} \in ℝ$
12	11	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
13		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (A \in (0, \frac{π}{2}) \leftrightarrow (A \in ℝ \land 0 < A \land A < \frac{π}{2}))$
14	10 12 13	mp2an	$⊢ A \in (0, \frac{π}{2}) \leftrightarrow (A \in ℝ \land 0 < A \land A < \frac{π}{2})$
15	7 8 9 14	syl3anbrc	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to A \in (0, \frac{π}{2})$
16		sincosq1sgn	$⊢ A \in (0, \frac{π}{2}) \to (0 < \sin A \land 0 < \cos A)$
17	15 16	syl	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to (0 < \sin A \land 0 < \cos A)$
18	17	simprd	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to 0 < \cos A$
19	18	gt0ne0d	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 < A) \to \cos A \neq 0$
20		simpr	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 = A) \to 0 = A$
21	20	fveq2d	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 = A) \to \cos 0 = \cos A$
22		cos0	$⊢ \cos 0 = 1$
23	21 22	eqtr3di	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 = A) \to \cos A = 1$
24		ax-1ne0	$⊢ 1 \neq 0$
25	24	a1i	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 = A) \to 1 \neq 0$
26	23 25	eqnetrd	$⊢ (((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \land 0 = A) \to \cos A \neq 0$
27	5	simp2d	$⊢ (A \in [0, π] \land \cos A = 0) \to 0 \leq A$
28		0red	$⊢ (A \in [0, π] \land \cos A = 0) \to 0 \in ℝ$
29	28 6	leloed	$⊢ (A \in [0, π] \land \cos A = 0) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
30	27 29	mpbid	$⊢ (A \in [0, π] \land \cos A = 0) \to (0 < A \lor 0 = A)$
31	30	adantr	$⊢ ((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \to (0 < A \lor 0 = A)$
32	19 26 31	mpjaodan	$⊢ ((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \to \cos A \neq 0$
33	1 32	pm2.21ddne	$⊢ ((A \in [0, π] \land \cos A = 0) \land A < \frac{π}{2}) \to A = \frac{π}{2}$
34		simpr	$⊢ ((A \in [0, π] \land \cos A = 0) \land A = \frac{π}{2}) \to A = \frac{π}{2}$
35		simplr	$⊢ ((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \to \cos A = 0$
36	6	ad2antrr	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to A \in ℝ$
37		simplr	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to \frac{π}{2} < A$
38		simpr	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to A < π$
39	3	rexri	$⊢ π \in ℝ^{*}$
40		elioo2	$⊢ (\frac{π}{2} \in ℝ^{} \land π \in ℝ^{}) \to (A \in (\frac{π}{2}, π) \leftrightarrow (A \in ℝ \land \frac{π}{2} < A \land A < π))$
41	12 39 40	mp2an	$⊢ A \in (\frac{π}{2}, π) \leftrightarrow (A \in ℝ \land \frac{π}{2} < A \land A < π)$
42	36 37 38 41	syl3anbrc	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to A \in (\frac{π}{2}, π)$
43		sincosq2sgn	$⊢ A \in (\frac{π}{2}, π) \to (0 < \sin A \land \cos A < 0)$
44	42 43	syl	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to (0 < \sin A \land \cos A < 0)$
45	44	simprd	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to \cos A < 0$
46	45	lt0ne0d	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A < π) \to \cos A \neq 0$
47		simpr	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A = π) \to A = π$
48	47	fveq2d	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A = π) \to \cos A = \cos π$
49		cospi	$⊢ \cos π = - 1$
50	48 49	eqtrdi	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A = π) \to \cos A = - 1$
51		neg1ne0	$⊢ - 1 \neq 0$
52	51	a1i	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A = π) \to - 1 \neq 0$
53	50 52	eqnetrd	$⊢ (((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \land A = π) \to \cos A \neq 0$
54	5	simp3d	$⊢ (A \in [0, π] \land \cos A = 0) \to A \leq π$
55	3	a1i	$⊢ (A \in [0, π] \land \cos A = 0) \to π \in ℝ$
56	6 55	leloed	$⊢ (A \in [0, π] \land \cos A = 0) \to (A \leq π \leftrightarrow (A < π \lor A = π))$
57	54 56	mpbid	$⊢ (A \in [0, π] \land \cos A = 0) \to (A < π \lor A = π)$
58	57	adantr	$⊢ ((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \to (A < π \lor A = π)$
59	46 53 58	mpjaodan	$⊢ ((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \to \cos A \neq 0$
60	35 59	pm2.21ddne	$⊢ ((A \in [0, π] \land \cos A = 0) \land \frac{π}{2} < A) \to A = \frac{π}{2}$
61	55	rehalfcld	$⊢ (A \in [0, π] \land \cos A = 0) \to \frac{π}{2} \in ℝ$
62	6 61	lttri4d	$⊢ (A \in [0, π] \land \cos A = 0) \to (A < \frac{π}{2} \lor A = \frac{π}{2} \lor \frac{π}{2} < A)$
63	33 34 60 62	mpjao3dan	$⊢ (A \in [0, π] \land \cos A = 0) \to A = \frac{π}{2}$
64		fveq2	$⊢ A = \frac{π}{2} \to \cos A = \cos (\frac{π}{2})$
65		coshalfpi	$⊢ \cos (\frac{π}{2}) = 0$
66	64 65	eqtrdi	$⊢ A = \frac{π}{2} \to \cos A = 0$
67	66	adantl	$⊢ (A \in [0, π] \land A = \frac{π}{2}) \to \cos A = 0$
68	63 67	impbida	$⊢ A \in [0, π] \to (\cos A = 0 \leftrightarrow A = \frac{π}{2})$

Metamath Proof Explorer

Theorem coseq00topi

Proof