This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )