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 ⊢ A ∈ 0 π → cos ⁡ A ∈ − 1 1

Proof

Step Hyp Ref Expression
1 elioore ⊢ A ∈ 0 π → A ∈ ℝ
2 1 recoscld ⊢ A ∈ 0 π → cos ⁡ A ∈ ℝ
3 cospi ⊢ cos ⁡ π = − 1
4 ioossicc ⊢ 0 π ⊆ 0 π
5 4 sseli ⊢ A ∈ 0 π → A ∈ 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 ⊢ A ∈ 0 π → π ∈ 0 π
13 eliooord ⊢ A ∈ 0 π → 0 < A ∧ A < π
14 13 simprd ⊢ A ∈ 0 π → A < π
15 5 12 14 cosordlem ⊢ A ∈ 0 π → cos ⁡ π < cos ⁡ A
16 3 15 eqbrtrrid ⊢ A ∈ 0 π → − 1 < cos ⁡ A
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 ⊢ A ∈ 0 π → A ∈ 0 2 ⁢ π
26 cos02pilt1 ⊢ A ∈ 0 2 ⁢ π → cos ⁡ A < 1
27 25 26 syl ⊢ A ∈ 0 π → cos ⁡ A < 1
28 neg1rr ⊢ − 1 ∈ ℝ
29 28 rexri ⊢ − 1 ∈ ℝ *
30 1xr ⊢ 1 ∈ ℝ *
31 elioo2 ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * → cos ⁡ A ∈ − 1 1 ↔ cos ⁡ A ∈ ℝ ∧ − 1 < cos ⁡ A ∧ cos ⁡ A < 1
32 29 30 31 mp2an ⊢ cos ⁡ A ∈ − 1 1 ↔ cos ⁡ A ∈ ℝ ∧ − 1 < cos ⁡ A ∧ cos ⁡ A < 1
33 2 16 27 32 syl3anbrc ⊢ A ∈ 0 π → cos ⁡ A ∈ − 1 1