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 )