Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
|- 0 e. RR |
2 |
|
pire |
|- _pi e. RR |
3 |
1 2
|
elicc2i |
|- ( A e. ( 0 [,] _pi ) <-> ( A e. RR /\ 0 <_ A /\ A <_ _pi ) ) |
4 |
3
|
simp1bi |
|- ( A e. ( 0 [,] _pi ) -> A e. RR ) |
5 |
|
rexr |
|- ( 0 e. RR -> 0 e. RR* ) |
6 |
|
rexr |
|- ( _pi e. RR -> _pi e. RR* ) |
7 |
|
elioo2 |
|- ( ( 0 e. RR* /\ _pi e. RR* ) -> ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) ) |
8 |
5 6 7
|
syl2an |
|- ( ( 0 e. RR /\ _pi e. RR ) -> ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) ) |
9 |
1 2 8
|
mp2an |
|- ( A e. ( 0 (,) _pi ) <-> ( A e. RR /\ 0 < A /\ A < _pi ) ) |
10 |
|
sinq12gt0 |
|- ( A e. ( 0 (,) _pi ) -> 0 < ( sin ` A ) ) |
11 |
9 10
|
sylbir |
|- ( ( A e. RR /\ 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) ) |
12 |
11
|
3expib |
|- ( A e. RR -> ( ( 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) ) ) |
13 |
4 12
|
syl |
|- ( A e. ( 0 [,] _pi ) -> ( ( 0 < A /\ A < _pi ) -> 0 < ( sin ` A ) ) ) |
14 |
4
|
resincld |
|- ( A e. ( 0 [,] _pi ) -> ( sin ` A ) e. RR ) |
15 |
|
ltle |
|- ( ( 0 e. RR /\ ( sin ` A ) e. RR ) -> ( 0 < ( sin ` A ) -> 0 <_ ( sin ` A ) ) ) |
16 |
1 14 15
|
sylancr |
|- ( A e. ( 0 [,] _pi ) -> ( 0 < ( sin ` A ) -> 0 <_ ( sin ` A ) ) ) |
17 |
13 16
|
syld |
|- ( A e. ( 0 [,] _pi ) -> ( ( 0 < A /\ A < _pi ) -> 0 <_ ( sin ` A ) ) ) |
18 |
17
|
expd |
|- ( A e. ( 0 [,] _pi ) -> ( 0 < A -> ( A < _pi -> 0 <_ ( sin ` A ) ) ) ) |
19 |
|
0le0 |
|- 0 <_ 0 |
20 |
|
sin0 |
|- ( sin ` 0 ) = 0 |
21 |
19 20
|
breqtrri |
|- 0 <_ ( sin ` 0 ) |
22 |
|
fveq2 |
|- ( 0 = A -> ( sin ` 0 ) = ( sin ` A ) ) |
23 |
21 22
|
breqtrid |
|- ( 0 = A -> 0 <_ ( sin ` A ) ) |
24 |
23
|
a1i13 |
|- ( A e. ( 0 [,] _pi ) -> ( 0 = A -> ( A < _pi -> 0 <_ ( sin ` A ) ) ) ) |
25 |
3
|
simp2bi |
|- ( A e. ( 0 [,] _pi ) -> 0 <_ A ) |
26 |
|
leloe |
|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) ) |
27 |
1 4 26
|
sylancr |
|- ( A e. ( 0 [,] _pi ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) ) |
28 |
25 27
|
mpbid |
|- ( A e. ( 0 [,] _pi ) -> ( 0 < A \/ 0 = A ) ) |
29 |
18 24 28
|
mpjaod |
|- ( A e. ( 0 [,] _pi ) -> ( A < _pi -> 0 <_ ( sin ` A ) ) ) |
30 |
|
sinpi |
|- ( sin ` _pi ) = 0 |
31 |
19 30
|
breqtrri |
|- 0 <_ ( sin ` _pi ) |
32 |
|
fveq2 |
|- ( A = _pi -> ( sin ` A ) = ( sin ` _pi ) ) |
33 |
31 32
|
breqtrrid |
|- ( A = _pi -> 0 <_ ( sin ` A ) ) |
34 |
33
|
a1i |
|- ( A e. ( 0 [,] _pi ) -> ( A = _pi -> 0 <_ ( sin ` A ) ) ) |
35 |
3
|
simp3bi |
|- ( A e. ( 0 [,] _pi ) -> A <_ _pi ) |
36 |
|
leloe |
|- ( ( A e. RR /\ _pi e. RR ) -> ( A <_ _pi <-> ( A < _pi \/ A = _pi ) ) ) |
37 |
4 2 36
|
sylancl |
|- ( A e. ( 0 [,] _pi ) -> ( A <_ _pi <-> ( A < _pi \/ A = _pi ) ) ) |
38 |
35 37
|
mpbid |
|- ( A e. ( 0 [,] _pi ) -> ( A < _pi \/ A = _pi ) ) |
39 |
29 34 38
|
mpjaod |
|- ( A e. ( 0 [,] _pi ) -> 0 <_ ( sin ` A ) ) |