Metamath Proof Explorer


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 ‘ 𝐴 ) ∈ ℝ+ )