cos0pilt1

Description: Cosine is between minus one and one on the open interval between zero and _pi . (Contributed by Jim Kingdon, 7-May-2024)

		Ref	Expression
	Assertion	cos0pilt1	$⊢ A \in (0, π) \to \cos A \in (- 1, 1)$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ A \in (0, π) \to A \in ℝ$
2	1	recoscld	$⊢ A \in (0, π) \to \cos A \in ℝ$
3		cospi	$⊢ \cos π = - 1$
4		ioossicc	$⊢ (0, π) \subseteq [0, π]$
5	4	sseli	$⊢ A \in (0, π) \to A \in [0, π]$
6		0xr	$⊢ 0 \in ℝ^{*}$
7		pire	$⊢ π \in ℝ$
8	7	rexri	$⊢ π \in ℝ^{*}$
9		0re	$⊢ 0 \in ℝ$
10		pipos	$⊢ 0 < π$
11	9 7 10	ltleii	$⊢ 0 \leq π$
12		ubicc2	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land 0 \leq π) \to π \in [0, π]$
13	6 8 11 12	mp3an	$⊢ π \in [0, π]$
14	13	a1i	$⊢ A \in (0, π) \to π \in [0, π]$
15		eliooord	$⊢ A \in (0, π) \to (0 < A \land A < π)$
16	15	simprd	$⊢ A \in (0, π) \to A < π$
17	5 14 16	cosordlem	$⊢ A \in (0, π) \to \cos π < \cos A$
18	3 17	eqbrtrrid	$⊢ A \in (0, π) \to - 1 < \cos A$
19		2re	$⊢ 2 \in ℝ$
20	19 7	remulcli	$⊢ 2 π \in ℝ$
21	20	rexri	$⊢ 2 π \in ℝ^{*}$
22		1le2	$⊢ 1 \leq 2$
23		lemulge12	$⊢ ((π \in ℝ \land 2 \in ℝ) \land (0 \leq π \land 1 \leq 2)) \to π \leq 2 π$
24	7 19 11 22 23	mp4an	$⊢ π \leq 2 π$
25		iooss2	$⊢ (2 π \in ℝ^{*} \land π \leq 2 π) \to (0, π) \subseteq (0, 2 π)$
26	21 24 25	mp2an	$⊢ (0, π) \subseteq (0, 2 π)$
27	26	sseli	$⊢ A \in (0, π) \to A \in (0, 2 π)$
28		cos02pilt1	$⊢ A \in (0, 2 π) \to \cos A < 1$
29	27 28	syl	$⊢ A \in (0, π) \to \cos A < 1$
30		neg1rr	$⊢ - 1 \in ℝ$
31	30	rexri	$⊢ - 1 \in ℝ^{*}$
32		1re	$⊢ 1 \in ℝ$
33	32	rexri	$⊢ 1 \in ℝ^{*}$
34		elioo2	$⊢ (- 1 \in ℝ^{} \land 1 \in ℝ^{}) \to (\cos A \in (- 1, 1) \leftrightarrow (\cos A \in ℝ \land - 1 < \cos A \land \cos A < 1))$
35	31 33 34	mp2an	$⊢ \cos A \in (- 1, 1) \leftrightarrow (\cos A \in ℝ \land - 1 < \cos A \land \cos A < 1)$
36	2 18 29 35	syl3anbrc	$⊢ A \in (0, π) \to \cos A \in (- 1, 1)$

Metamath Proof Explorer

Theorem cos0pilt1

Proof