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		0re	⊢ 0 ∈ ℝ
10		pipos	⊢ 0 < π
11	9 7 10	ltleii	⊢ 0 ≤ π
12		ubicc2	⊢ ( ( 0 ∈ ℝ^* ∧ π ∈ ℝ^* ∧ 0 ≤ π ) → π ∈ ( 0 [,] π ) )
13	6 8 11 12	mp3an	⊢ π ∈ ( 0 [,] π )
14	13	a1i	⊢ ( 𝐴 ∈ ( 0 (,) π ) → π ∈ ( 0 [,] π ) )
15		eliooord	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( 0 < 𝐴 ∧ 𝐴 < π ) )
16	15	simprd	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 < π )
17	5 14 16	cosordlem	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ π ) < ( cos ‘ 𝐴 ) )
18	3 17	eqbrtrrid	⊢ ( 𝐴 ∈ ( 0 (,) π ) → - 1 < ( cos ‘ 𝐴 ) )
19		2re	⊢ 2 ∈ ℝ
20	19 7	remulcli	⊢ ( 2 · π ) ∈ ℝ
21	20	rexri	⊢ ( 2 · π ) ∈ ℝ^*
22		1le2	⊢ 1 ≤ 2
23		lemulge12	⊢ ( ( ( π ∈ ℝ ∧ 2 ∈ ℝ ) ∧ ( 0 ≤ π ∧ 1 ≤ 2 ) ) → π ≤ ( 2 · π ) )
24	7 19 11 22 23	mp4an	⊢ π ≤ ( 2 · π )
25		iooss2	⊢ ( ( ( 2 · π ) ∈ ℝ^* ∧ π ≤ ( 2 · π ) ) → ( 0 (,) π ) ⊆ ( 0 (,) ( 2 · π ) ) )
26	21 24 25	mp2an	⊢ ( 0 (,) π ) ⊆ ( 0 (,) ( 2 · π ) )
27	26	sseli	⊢ ( 𝐴 ∈ ( 0 (,) π ) → 𝐴 ∈ ( 0 (,) ( 2 · π ) ) )
28		cos02pilt1	⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( cos ‘ 𝐴 ) < 1 )
29	27 28	syl	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) < 1 )
30		neg1rr	⊢ - 1 ∈ ℝ
31	30	rexri	⊢ - 1 ∈ ℝ^*
32		1re	⊢ 1 ∈ ℝ
33	32	rexri	⊢ 1 ∈ ℝ^*
34		elioo2	⊢ ( ( - 1 ∈ ℝ^* ∧ 1 ∈ ℝ^* ) → ( ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 1 ) ) )
35	31 33 34	mp2an	⊢ ( ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 < ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 1 ) )
36	2 18 29 35	syl3anbrc	⊢ ( 𝐴 ∈ ( 0 (,) π ) → ( cos ‘ 𝐴 ) ∈ ( - 1 (,) 1 ) )

Metamath Proof Explorer

Theorem cos0pilt1

Proof