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