Metamath Proof Explorer


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 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 ) )