Theorem cosq34lt1

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

	Ref	Expression
Assertion	cosq34lt1	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )

Proof

Step	Hyp	Ref	Expression
1		pire	⊢ π ∈ ℝ
2		2re	⊢ 2 ∈ ℝ
3	2 1	remulcli	⊢ ( 2 · π ) ∈ ℝ
4	3	rexri	⊢ ( 2 · π ) ∈ ℝ*
5		elico2	⊢ ( ( π ∈ ℝ ∧ ( 2 · π ) ∈ ℝ* ) → ( 𝐴 ∈ ( π [,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ π ≤ 𝐴 ∧ 𝐴 < ( 2 · π ) ) ) )
6	1 4 5	mp2an	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ π ≤ 𝐴 ∧ 𝐴 < ( 2 · π ) ) )
7	6	simp1bi	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 𝐴 ∈ ℝ )
8		0red	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 0 ∈ ℝ )
9	1	a1i	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → π ∈ ℝ )
10		pipos	⊢ 0 < π
11	10	a1i	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 0 < π )
12	6	simp2bi	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → π ≤ 𝐴 )
13	8 9 7 11 12	ltletrd	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 0 < 𝐴 )
14	6	simp3bi	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 𝐴 < ( 2 · π ) )
15		0xr	⊢ 0 ∈ ℝ*
16		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ ( 2 · π ) ∈ ℝ* ) → ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < ( 2 · π ) ) ) )
17	15 4 16	mp2an	⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < ( 2 · π ) ) )
18	7 13 14 17	syl3anbrc	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → 𝐴 ∈ ( 0 (,) ( 2 · π ) ) )
19		cos02pilt1	⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )
20	18 19	syl	⊢ ( 𝐴 ∈ ( π [,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )