Metamath Proof Explorer


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 )