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