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

Metamath Proof Explorer

Theorem coseq00topi

Proof