This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sin4lt0

Description: The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion sin4lt0 
|- ( sin ` 4 ) < 0

Proof

Step Hyp Ref Expression
1 2t2e4 
 |-  ( 2 x. 2 ) = 4
2 1 fveq2i 
 |-  ( sin ` ( 2 x. 2 ) ) = ( sin ` 4 )
3 2cn 
 |-  2 e. CC
4 sin2t 
 |-  ( 2 e. CC -> ( sin ` ( 2 x. 2 ) ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) )
5 3 4 ax-mp 
 |-  ( sin ` ( 2 x. 2 ) ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) )
6 2 5 eqtr3i 
 |-  ( sin ` 4 ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) )
7 sincos2sgn 
 |-  ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
8 7 simpri 
 |-  ( cos ` 2 ) < 0
9 2re 
 |-  2 e. RR
10 recoscl 
 |-  ( 2 e. RR -> ( cos ` 2 ) e. RR )
11 9 10 ax-mp 
 |-  ( cos ` 2 ) e. RR
12 0re 
 |-  0 e. RR
13 resincl 
 |-  ( 2 e. RR -> ( sin ` 2 ) e. RR )
14 9 13 ax-mp 
 |-  ( sin ` 2 ) e. RR
15 7 simpli 
 |-  0 < ( sin ` 2 )
16 14 15 pm3.2i 
 |-  ( ( sin ` 2 ) e. RR /\ 0 < ( sin ` 2 ) )
17 ltmul2 
 |-  ( ( ( cos ` 2 ) e. RR /\ 0 e. RR /\ ( ( sin ` 2 ) e. RR /\ 0 < ( sin ` 2 ) ) ) -> ( ( cos ` 2 ) < 0 <-> ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 ) ) )
18 11 12 16 17 mp3an 
 |-  ( ( cos ` 2 ) < 0 <-> ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 ) )
19 8 18 mpbi 
 |-  ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 )
20 14 recni 
 |-  ( sin ` 2 ) e. CC
21 20 mul01i 
 |-  ( ( sin ` 2 ) x. 0 ) = 0
22 19 21 breqtri 
 |-  ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0
23 14 11 remulcli 
 |-  ( ( sin ` 2 ) x. ( cos ` 2 ) ) e. RR
24 2pos 
 |-  0 < 2
25 9 24 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
26 ltmul2 
 |-  ( ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) e. RR /\ 0 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0 <-> ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 ) ) )
27 23 12 25 26 mp3an 
 |-  ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0 <-> ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 ) )
28 22 27 mpbi 
 |-  ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 )
29 3 mul01i 
 |-  ( 2 x. 0 ) = 0
30 28 29 breqtri 
 |-  ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < 0
31 6 30 eqbrtri 
 |-  ( sin ` 4 ) < 0