Theorem cos0pilt1

Description: Cosine is between minus one and one on the open interval between zero and _pi . (Contributed by Jim Kingdon, 7-May-2024)

	Ref	Expression
Assertion	cos0pilt1	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) )

Proof

Step	Hyp	Ref	Expression
1		elioore	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 ∈ ℝ )
2	1	recoscld	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) ∈ ℝ )
3		cospi	⊢ ( cos ‘ π ) = - 1
4		ioossicc	⊢ ( 0 (,) π ) ⊆ ( 0 [,] π )
5	4	sseli	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 ∈ ( 0 [,] π ) )
6		0xr	⊢ 0 ∈ ℝ*
7		pire	⊢ π ∈ ℝ
8	7	rexri	⊢ π ∈ ℝ*
9		pige0	⊢ 0 ≤ π
10		ubicc2	⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 0 ≤ π ) → π ∈ ( 0 [,] π ) )
11	6 8 9 10	mp3an	⊢ π ∈ ( 0 [,] π )
12	11	a1i	⊢ ( 𝐴 ∈ ( 0 (,) π ) → π ∈ ( 0 [,] π ) )
13		eliooord	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( 0 < 𝐴 ∧ 𝐴 < π ) )
14	13	simprd	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 < π )
15	5 12 14	cosordlem	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ π ) < ( cos ‘ 𝐴 ) )
16	3 15	eqbrtrrid	⊢ ( 𝐴 ∈ ( 0 (,) π ) → - 1 < ( cos ‘ 𝐴 ) )
17		2pire	⊢ ( 2 · π ) ∈ ℝ
18	17	rexri	⊢ ( 2 · π ) ∈ ℝ*
19		2re	⊢ 2 ∈ ℝ
20		1le2	⊢ 1 ≤ 2
21		lemulge12	⊢ ( ( ( π ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 0 ≤ π ∧ 1 ≤ 2 ) ) → π ≤ ( 2 · π ) )
22	7 19 9 20 21	mp4an	⊢ π ≤ ( 2 · π )
23		iooss2	⊢ ( ( ( 2 · π ) ∈ ℝ* ∧ π ≤ ( 2 · π ) ) → ( 0 (,) π ) ⊆ ( 0 (,) ( 2 · π ) ) )
24	18 22 23	mp2an	⊢ ( 0 (,) π ) ⊆ ( 0 (,) ( 2 · π ) )
25	24	sseli	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 ∈ ( 0 (,) ( 2 · π ) ) )
26		cos02pilt1	⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )
27	25 26	syl	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) < 1 )
28		neg1rr	⊢ - 1 ∈ ℝ
29	28	rexri	⊢ - 1 ∈ ℝ*
30		1xr	⊢ 1 ∈ ℝ*
31		elioo2	⊢ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 1 ) ) )
32	29 30 31	mp2an	⊢ ( ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 1 ) )
33	2 16 27 32	syl3anbrc	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) )