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

Proof

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