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 ∈ 0 π 2 → tan ⁡ A ∈ ℝ +

Proof

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