Theorem tanrpcl

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

	Ref	Expression
Assertion	tanrpcl	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		elioore	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 𝐴 ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 𝐴 ∈ ℂ )
3	1	recoscld	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( cos ‘ 𝐴 ) ∈ ℝ )
4		sincosq1sgn	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ 𝐴 ) ∧ 0 < ( cos ‘ 𝐴 ) ) )
5	4	simprd	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝐴 ) )
6	3 5	elrpd	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( cos ‘ 𝐴 ) ∈ ℝ+ )
7	6	rpne0d	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
8		tanval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
9	2 7 8	syl2anc	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
10	1	resincld	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( sin ‘ 𝐴 ) ∈ ℝ )
11	4	simpld	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 0 < ( sin ‘ 𝐴 ) )
12	10 11	elrpd	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( sin ‘ 𝐴 ) ∈ ℝ+ )
13	12 6	rpdivcld	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ∈ ℝ+ )
14	9 13	eqeltrd	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ 𝐴 ) ∈ ℝ+ )