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 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 ⊢ A ∈ 0 π → π ∈ 0 π
15 eliooord ⊢ A ∈ 0 π → 0 < A ∧ A < π
16 15 simprd ⊢ A ∈ 0 π → A < π
17 5 14 16 cosordlem ⊢ A ∈ 0 π → cos ⁡ π < cos ⁡ A
18 3 17 eqbrtrrid ⊢ A ∈ 0 π → − 1 < cos ⁡ A
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 ⊢ A ∈ 0 π → A ∈ 0 2 ⁢ π
28 cos02pilt1 ⊢ A ∈ 0 2 ⁢ π → cos ⁡ A < 1
29 27 28 syl ⊢ A ∈ 0 π → cos ⁡ A < 1
30 neg1rr ⊢ − 1 ∈ ℝ
31 30 rexri ⊢ − 1 ∈ ℝ *
32 1re ⊢ 1 ∈ ℝ
33 32 rexri ⊢ 1 ∈ ℝ *
34 elioo2 ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * → cos ⁡ A ∈ − 1 1 ↔ cos ⁡ A ∈ ℝ ∧ − 1 < cos ⁡ A ∧ cos ⁡ A < 1
35 31 33 34 mp2an ⊢ cos ⁡ A ∈ − 1 1 ↔ cos ⁡ A ∈ ℝ ∧ − 1 < cos ⁡ A ∧ cos ⁡ A < 1
36 2 18 29 35 syl3anbrc ⊢ A ∈ 0 π → cos ⁡ A ∈ − 1 1