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

Metamath Proof Explorer

Theorem tanrpcl

Description: Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Assertion tanrpcl 
|- ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` A ) e. RR+ )

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> A e. RR )
2 1 recnd 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> A e. CC )
3 1 recoscld 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( cos ` A ) e. RR )
4 sincosq1sgn 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
5 4 simprd 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> 0 < ( cos ` A ) )
6 3 5 elrpd 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( cos ` A ) e. RR+ )
7 6 rpne0d 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( cos ` A ) =/= 0 )
8 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
9 2 7 8 syl2anc 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
10 1 resincld 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( sin ` A ) e. RR )
11 4 simpld 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> 0 < ( sin ` A ) )
12 10 11 elrpd 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( sin ` A ) e. RR+ )
13 12 6 rpdivcld 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( ( sin ` A ) / ( cos ` A ) ) e. RR+ )
14 9 13 eqeltrd 
 |-  ( A e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` A ) e. RR+ )