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