| Step |
Hyp |
Ref |
Expression |
| 1 |
|
halfpire |
|- ( _pi / 2 ) e. RR |
| 2 |
|
ltle |
|- ( ( A e. RR /\ ( _pi / 2 ) e. RR ) -> ( A < ( _pi / 2 ) -> A <_ ( _pi / 2 ) ) ) |
| 3 |
1 2
|
mpan2 |
|- ( A e. RR -> ( A < ( _pi / 2 ) -> A <_ ( _pi / 2 ) ) ) |
| 4 |
|
pire |
|- _pi e. RR |
| 5 |
|
4re |
|- 4 e. RR |
| 6 |
|
pigt2lt4 |
|- ( 2 < _pi /\ _pi < 4 ) |
| 7 |
6
|
simpri |
|- _pi < 4 |
| 8 |
4 5 7
|
ltleii |
|- _pi <_ 4 |
| 9 |
|
2re |
|- 2 e. RR |
| 10 |
|
2pos |
|- 0 < 2 |
| 11 |
9 10
|
pm3.2i |
|- ( 2 e. RR /\ 0 < 2 ) |
| 12 |
|
ledivmul |
|- ( ( _pi e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( _pi / 2 ) <_ 2 <-> _pi <_ ( 2 x. 2 ) ) ) |
| 13 |
4 9 11 12
|
mp3an |
|- ( ( _pi / 2 ) <_ 2 <-> _pi <_ ( 2 x. 2 ) ) |
| 14 |
|
2t2e4 |
|- ( 2 x. 2 ) = 4 |
| 15 |
14
|
breq2i |
|- ( _pi <_ ( 2 x. 2 ) <-> _pi <_ 4 ) |
| 16 |
13 15
|
bitri |
|- ( ( _pi / 2 ) <_ 2 <-> _pi <_ 4 ) |
| 17 |
8 16
|
mpbir |
|- ( _pi / 2 ) <_ 2 |
| 18 |
|
letr |
|- ( ( A e. RR /\ ( _pi / 2 ) e. RR /\ 2 e. RR ) -> ( ( A <_ ( _pi / 2 ) /\ ( _pi / 2 ) <_ 2 ) -> A <_ 2 ) ) |
| 19 |
1 9 18
|
mp3an23 |
|- ( A e. RR -> ( ( A <_ ( _pi / 2 ) /\ ( _pi / 2 ) <_ 2 ) -> A <_ 2 ) ) |
| 20 |
17 19
|
mpan2i |
|- ( A e. RR -> ( A <_ ( _pi / 2 ) -> A <_ 2 ) ) |
| 21 |
3 20
|
syld |
|- ( A e. RR -> ( A < ( _pi / 2 ) -> A <_ 2 ) ) |
| 22 |
21
|
adantr |
|- ( ( A e. RR /\ 0 < A ) -> ( A < ( _pi / 2 ) -> A <_ 2 ) ) |
| 23 |
22
|
3impia |
|- ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> A <_ 2 ) |
| 24 |
|
0xr |
|- 0 e. RR* |
| 25 |
|
elioc2 |
|- ( ( 0 e. RR* /\ 2 e. RR ) -> ( A e. ( 0 (,] 2 ) <-> ( A e. RR /\ 0 < A /\ A <_ 2 ) ) ) |
| 26 |
24 9 25
|
mp2an |
|- ( A e. ( 0 (,] 2 ) <-> ( A e. RR /\ 0 < A /\ A <_ 2 ) ) |
| 27 |
|
sin02gt0 |
|- ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) ) |
| 28 |
26 27
|
sylbir |
|- ( ( A e. RR /\ 0 < A /\ A <_ 2 ) -> 0 < ( sin ` A ) ) |
| 29 |
23 28
|
syld3an3 |
|- ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> 0 < ( sin ` A ) ) |