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

Metamath Proof Explorer

Theorem cos02pilt1

Description: Cosine is less than one between zero and 2 x. _pi . (Contributed by Jim Kingdon, 23-Mar-2024)

Ref Expression
Assertion cos02pilt1 ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )

Proof

Step Hyp Ref Expression
1 elioore ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 𝐴 ∈ ℝ )
2 1 recoscld ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) ∈ ℝ )
3 1red ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 1 ∈ ℝ )
4 cosbnd ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) )
5 4 simprd ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ≤ 1 )
6 1 5 syl ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) ≤ 1 )
7 0zd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 0 ∈ ℤ )
8 2re ⊢ 2 ∈ ℝ
9 pire ⊢ π ∈ ℝ
10 8 9 remulcli ⊢ ( 2 · π ) ∈ ℝ
11 10 a1i ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 2 · π ) ∈ ℝ )
12 0xr ⊢ 0 ∈ ℝ*
13 10 rexri ⊢ ( 2 · π ) ∈ ℝ*
14 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 2 · π ) ∈ ℝ* ) → ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < ( 2 · π ) ) ) )
15 12 13 14 mp2an ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < ( 2 · π ) ) )
16 15 simp2bi ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 0 < 𝐴 )
17 2rp ⊢ 2 ∈ ℝ+
18 pirp ⊢ π ∈ ℝ+
19 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
20 17 18 19 mp2an ⊢ ( 2 · π ) ∈ ℝ+
21 rpgt0 ⊢ ( ( 2 · π ) ∈ ℝ+ → 0 < ( 2 · π ) )
22 20 21 mp1i ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 0 < ( 2 · π ) )
23 1 11 16 22 divgt0d ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 0 < ( 𝐴 / ( 2 · π ) ) )
24 20 a1i ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 2 · π ) ∈ ℝ+ )
25 15 simp3bi ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 𝐴 < ( 2 · π ) )
26 1 11 24 25 ltdiv1dd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 𝐴 / ( 2 · π ) ) < ( ( 2 · π ) / ( 2 · π ) ) )
27 11 recnd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 2 · π ) ∈ ℂ )
28 22 gt0ne0d ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 2 · π ) ≠ 0 )
29 27 28 dividd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( ( 2 · π ) / ( 2 · π ) ) = 1 )
30 26 29 breqtrd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 𝐴 / ( 2 · π ) ) < 1 )
31 0p1e1 ⊢ ( 0 + 1 ) = 1
32 30 31 breqtrrdi ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( 𝐴 / ( 2 · π ) ) < ( 0 + 1 ) )
33 btwnnz ⊢ ( ( 0 ∈ ℤ ∧ 0 < ( 𝐴 / ( 2 · π ) ) ∧ ( 𝐴 / ( 2 · π ) ) < ( 0 + 1 ) ) → ¬ ( 𝐴 / ( 2 · π ) ) ∈ ℤ )
34 7 23 32 33 syl3anc ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ¬ ( 𝐴 / ( 2 · π ) ) ∈ ℤ )
35 1 recnd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 𝐴 ∈ ℂ )
36 coseq1 ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )
37 35 36 syl ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )
38 34 37 mtbird ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ¬ ( cos ‘ 𝐴 ) = 1 )
39 38 neqned ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) ≠ 1 )
40 39 necomd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → 1 ≠ ( cos ‘ 𝐴 ) )
41 2 3 6 40 leneltd ⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )