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