Step |
Hyp |
Ref |
Expression |
1 |
|
halfpire |
⊢ ( π / 2 ) ∈ ℝ |
2 |
|
elioore |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℝ ) |
3 |
|
resubcl |
⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ ) |
4 |
1 2 3
|
sylancr |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ ) |
5 |
|
neghalfpirx |
⊢ - ( π / 2 ) ∈ ℝ* |
6 |
1
|
rexri |
⊢ ( π / 2 ) ∈ ℝ* |
7 |
|
elioo2 |
⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ - ( π / 2 ) < 𝐴 ∧ 𝐴 < ( π / 2 ) ) ) ) |
8 |
5 6 7
|
mp2an |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ - ( π / 2 ) < 𝐴 ∧ 𝐴 < ( π / 2 ) ) ) |
9 |
8
|
simp3bi |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 < ( π / 2 ) ) |
10 |
|
posdif |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) ) |
11 |
2 1 10
|
sylancl |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) ) |
12 |
9 11
|
mpbid |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( ( π / 2 ) − 𝐴 ) ) |
13 |
|
picn |
⊢ π ∈ ℂ |
14 |
|
halfcl |
⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ ) |
15 |
13 14
|
ax-mp |
⊢ ( π / 2 ) ∈ ℂ |
16 |
15
|
negcli |
⊢ - ( π / 2 ) ∈ ℂ |
17 |
13 15
|
negsubi |
⊢ ( π + - ( π / 2 ) ) = ( π − ( π / 2 ) ) |
18 |
|
pidiv2halves |
⊢ ( ( π / 2 ) + ( π / 2 ) ) = π |
19 |
13 15 15 18
|
subaddrii |
⊢ ( π − ( π / 2 ) ) = ( π / 2 ) |
20 |
17 19
|
eqtri |
⊢ ( π + - ( π / 2 ) ) = ( π / 2 ) |
21 |
15 13 16 20
|
subaddrii |
⊢ ( ( π / 2 ) − π ) = - ( π / 2 ) |
22 |
8
|
simp2bi |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → - ( π / 2 ) < 𝐴 ) |
23 |
21 22
|
eqbrtrid |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − π ) < 𝐴 ) |
24 |
|
pire |
⊢ π ∈ ℝ |
25 |
|
ltsub23 |
⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) ) |
26 |
1 24 25
|
mp3an13 |
⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) ) |
27 |
2 26
|
syl |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) ) |
28 |
23 27
|
mpbird |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) < π ) |
29 |
|
0xr |
⊢ 0 ∈ ℝ* |
30 |
24
|
rexri |
⊢ π ∈ ℝ* |
31 |
|
elioo2 |
⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) ↔ ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 0 < ( ( π / 2 ) − 𝐴 ) ∧ ( ( π / 2 ) − 𝐴 ) < π ) ) ) |
32 |
29 30 31
|
mp2an |
⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) ↔ ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 0 < ( ( π / 2 ) − 𝐴 ) ∧ ( ( π / 2 ) − 𝐴 ) < π ) ) |
33 |
4 12 28 32
|
syl3anbrc |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) ) |
34 |
|
sinq12gt0 |
⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ) |
35 |
33 34
|
syl |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ) |
36 |
2
|
recnd |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℂ ) |
37 |
|
sinhalfpim |
⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) ) |
38 |
36 37
|
syl |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) ) |
39 |
35 38
|
breqtrd |
⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝐴 ) ) |