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 ⊢ A ∈ 0 2 ⁢ π → cos ⁡ A < 1

Proof

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