cos01gt0

Description: The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008)

		Ref	Expression
	Assertion	cos01gt0	$⊢ A \in (0, 1] \to 0 < \cos A$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		1re	$⊢ 1 \in ℝ$
3		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (A \in (0, 1] \leftrightarrow (A \in ℝ \land 0 < A \land A \leq 1))$
4	1 2 3	mp2an	$⊢ A \in (0, 1] \leftrightarrow (A \in ℝ \land 0 < A \land A \leq 1)$
5	4	simp1bi	$⊢ A \in (0, 1] \to A \in ℝ$
6	5	resqcld	$⊢ A \in (0, 1] \to A^{2} \in ℝ$
7	6	recnd	$⊢ A \in (0, 1] \to A^{2} \in ℂ$
8		2cn	$⊢ 2 \in ℂ$
9		3cn	$⊢ 3 \in ℂ$
10		3ne0	$⊢ 3 \neq 0$
11	9 10	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
12		div12	$⊢ (2 \in ℂ \land A^{2} \in ℂ \land (3 \in ℂ \land 3 \neq 0)) \to 2 (\frac{A^{2}}{3}) = A^{2} (\frac{2}{3})$
13	8 11 12	mp3an13	$⊢ A^{2} \in ℂ \to 2 (\frac{A^{2}}{3}) = A^{2} (\frac{2}{3})$
14	7 13	syl	$⊢ A \in (0, 1] \to 2 (\frac{A^{2}}{3}) = A^{2} (\frac{2}{3})$
15		2z	$⊢ 2 \in ℤ$
16		expgt0	$⊢ (A \in ℝ \land 2 \in ℤ \land 0 < A) \to 0 < A^{2}$
17	15 16	mp3an2	$⊢ (A \in ℝ \land 0 < A) \to 0 < A^{2}$
18	17	3adant3	$⊢ (A \in ℝ \land 0 < A \land A \leq 1) \to 0 < A^{2}$
19	4 18	sylbi	$⊢ A \in (0, 1] \to 0 < A^{2}$
20		2lt3	$⊢ 2 < 3$
21		2re	$⊢ 2 \in ℝ$
22		3re	$⊢ 3 \in ℝ$
23		3pos	$⊢ 0 < 3$
24	21 22 22 23	ltdiv1ii	$⊢ 2 < 3 \leftrightarrow \frac{2}{3} < \frac{3}{3}$
25	20 24	mpbi	$⊢ \frac{2}{3} < \frac{3}{3}$
26	9 10	dividi	$⊢ \frac{3}{3} = 1$
27	25 26	breqtri	$⊢ \frac{2}{3} < 1$
28	21 22 10	redivcli	$⊢ \frac{2}{3} \in ℝ$
29		ltmul2	$⊢ (\frac{2}{3} \in ℝ \land 1 \in ℝ \land (A^{2} \in ℝ \land 0 < A^{2})) \to (\frac{2}{3} < 1 \leftrightarrow A^{2} (\frac{2}{3}) < A^{2} \cdot 1)$
30	28 2 29	mp3an12	$⊢ (A^{2} \in ℝ \land 0 < A^{2}) \to (\frac{2}{3} < 1 \leftrightarrow A^{2} (\frac{2}{3}) < A^{2} \cdot 1)$
31	27 30	mpbii	$⊢ (A^{2} \in ℝ \land 0 < A^{2}) \to A^{2} (\frac{2}{3}) < A^{2} \cdot 1$
32	6 19 31	syl2anc	$⊢ A \in (0, 1] \to A^{2} (\frac{2}{3}) < A^{2} \cdot 1$
33	7	mulid1d	$⊢ A \in (0, 1] \to A^{2} \cdot 1 = A^{2}$
34	32 33	breqtrd	$⊢ A \in (0, 1] \to A^{2} (\frac{2}{3}) < A^{2}$
35	14 34	eqbrtrd	$⊢ A \in (0, 1] \to 2 (\frac{A^{2}}{3}) < A^{2}$
36		0re	$⊢ 0 \in ℝ$
37		ltle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \to 0 \leq A)$
38	36 37	mpan	$⊢ A \in ℝ \to (0 < A \to 0 \leq A)$
39	38	imdistani	$⊢ (A \in ℝ \land 0 < A) \to (A \in ℝ \land 0 \leq A)$
40		le2sq2	$⊢ ((A \in ℝ \land 0 \leq A) \land (1 \in ℝ \land A \leq 1)) \to A^{2} \leq 1^{2}$
41	2 40	mpanr1	$⊢ ((A \in ℝ \land 0 \leq A) \land A \leq 1) \to A^{2} \leq 1^{2}$
42	39 41	stoic3	$⊢ (A \in ℝ \land 0 < A \land A \leq 1) \to A^{2} \leq 1^{2}$
43	4 42	sylbi	$⊢ A \in (0, 1] \to A^{2} \leq 1^{2}$
44		sq1	$⊢ 1^{2} = 1$
45	43 44	breqtrdi	$⊢ A \in (0, 1] \to A^{2} \leq 1$
46		redivcl	$⊢ (A^{2} \in ℝ \land 3 \in ℝ \land 3 \neq 0) \to \frac{A^{2}}{3} \in ℝ$
47	22 10 46	mp3an23	$⊢ A^{2} \in ℝ \to \frac{A^{2}}{3} \in ℝ$
48	6 47	syl	$⊢ A \in (0, 1] \to \frac{A^{2}}{3} \in ℝ$
49		remulcl	$⊢ (2 \in ℝ \land \frac{A^{2}}{3} \in ℝ) \to 2 (\frac{A^{2}}{3}) \in ℝ$
50	21 48 49	sylancr	$⊢ A \in (0, 1] \to 2 (\frac{A^{2}}{3}) \in ℝ$
51		ltletr	$⊢ (2 (\frac{A^{2}}{3}) \in ℝ \land A^{2} \in ℝ \land 1 \in ℝ) \to ((2 (\frac{A^{2}}{3}) < A^{2} \land A^{2} \leq 1) \to 2 (\frac{A^{2}}{3}) < 1)$
52	2 51	mp3an3	$⊢ (2 (\frac{A^{2}}{3}) \in ℝ \land A^{2} \in ℝ) \to ((2 (\frac{A^{2}}{3}) < A^{2} \land A^{2} \leq 1) \to 2 (\frac{A^{2}}{3}) < 1)$
53	50 6 52	syl2anc	$⊢ A \in (0, 1] \to ((2 (\frac{A^{2}}{3}) < A^{2} \land A^{2} \leq 1) \to 2 (\frac{A^{2}}{3}) < 1)$
54	35 45 53	mp2and	$⊢ A \in (0, 1] \to 2 (\frac{A^{2}}{3}) < 1$
55		posdif	$⊢ (2 (\frac{A^{2}}{3}) \in ℝ \land 1 \in ℝ) \to (2 (\frac{A^{2}}{3}) < 1 \leftrightarrow 0 < 1 - 2 (\frac{A^{2}}{3}))$
56	50 2 55	sylancl	$⊢ A \in (0, 1] \to (2 (\frac{A^{2}}{3}) < 1 \leftrightarrow 0 < 1 - 2 (\frac{A^{2}}{3}))$
57	54 56	mpbid	$⊢ A \in (0, 1] \to 0 < 1 - 2 (\frac{A^{2}}{3})$
58		cos01bnd	$⊢ A \in (0, 1] \to (1 - 2 (\frac{A^{2}}{3}) < \cos A \land \cos A < 1 - (\frac{A^{2}}{3}))$
59	58	simpld	$⊢ A \in (0, 1] \to 1 - 2 (\frac{A^{2}}{3}) < \cos A$
60		resubcl	$⊢ (1 \in ℝ \land 2 (\frac{A^{2}}{3}) \in ℝ) \to 1 - 2 (\frac{A^{2}}{3}) \in ℝ$
61	2 50 60	sylancr	$⊢ A \in (0, 1] \to 1 - 2 (\frac{A^{2}}{3}) \in ℝ$
62	5	recoscld	$⊢ A \in (0, 1] \to \cos A \in ℝ$
63		lttr	$⊢ (0 \in ℝ \land 1 - 2 (\frac{A^{2}}{3}) \in ℝ \land \cos A \in ℝ) \to ((0 < 1 - 2 (\frac{A^{2}}{3}) \land 1 - 2 (\frac{A^{2}}{3}) < \cos A) \to 0 < \cos A)$
64	36 61 62 63	mp3an2i	$⊢ A \in (0, 1] \to ((0 < 1 - 2 (\frac{A^{2}}{3}) \land 1 - 2 (\frac{A^{2}}{3}) < \cos A) \to 0 < \cos A)$
65	57 59 64	mp2and	$⊢ A \in (0, 1] \to 0 < \cos A$

Metamath Proof Explorer

Theorem cos01gt0

Proof