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