Metamath Proof Explorer


Theorem sincosq1lem

Description: Lemma for sincosq1sgn . (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq1lem
|- ( ( A e. RR /\ 0 < A /\ A < ( _pi / 2 ) ) -> 0 < ( sin ` A ) )

Proof

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