cosq34lt1

Description: Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024)

		Ref	Expression
	Assertion	cosq34lt1	$⊢ A \in [π, 2 π) \to \cos A < 1$

Step	Hyp	Ref	Expression
1		pire	$⊢ π \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3	2 1	remulcli	$⊢ 2 π \in ℝ$
4	3	rexri	$⊢ 2 π \in ℝ^{*}$
5		elico2	$⊢ (π \in ℝ \land 2 π \in ℝ^{*}) \to (A \in [π, 2 π) \leftrightarrow (A \in ℝ \land π \leq A \land A < 2 π))$
6	1 4 5	mp2an	$⊢ A \in [π, 2 π) \leftrightarrow (A \in ℝ \land π \leq A \land A < 2 π)$
7	6	simp1bi	$⊢ A \in [π, 2 π) \to A \in ℝ$
8		0red	$⊢ A \in [π, 2 π) \to 0 \in ℝ$
9	1	a1i	$⊢ A \in [π, 2 π) \to π \in ℝ$
10		pipos	$⊢ 0 < π$
11	10	a1i	$⊢ A \in [π, 2 π) \to 0 < π$
12	6	simp2bi	$⊢ A \in [π, 2 π) \to π \leq A$
13	8 9 7 11 12	ltletrd	$⊢ A \in [π, 2 π) \to 0 < A$
14	6	simp3bi	$⊢ A \in [π, 2 π) \to A < 2 π$
15		0xr	$⊢ 0 \in ℝ^{*}$
16		elioo2	$⊢ (0 \in ℝ^{} \land 2 π \in ℝ^{}) \to (A \in (0, 2 π) \leftrightarrow (A \in ℝ \land 0 < A \land A < 2 π))$
17	15 4 16	mp2an	$⊢ A \in (0, 2 π) \leftrightarrow (A \in ℝ \land 0 < A \land A < 2 π)$
18	7 13 14 17	syl3anbrc	$⊢ A \in [π, 2 π) \to A \in (0, 2 π)$
19		cos02pilt1	$⊢ A \in (0, 2 π) \to \cos A < 1$
20	18 19	syl	$⊢ A \in [π, 2 π) \to \cos A < 1$

Metamath Proof Explorer