tanrpcl

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

		Ref	Expression
	Assertion	tanrpcl	$⊢ A \in (0, \frac{π}{2}) \to \tan A \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		elioore	$⊢ A \in (0, \frac{π}{2}) \to A \in ℝ$
2	1	recnd	$⊢ A \in (0, \frac{π}{2}) \to A \in ℂ$
3	1	recoscld	$⊢ A \in (0, \frac{π}{2}) \to \cos A \in ℝ$
4		sincosq1sgn	$⊢ A \in (0, \frac{π}{2}) \to (0 < \sin A \land 0 < \cos A)$
5	4	simprd	$⊢ A \in (0, \frac{π}{2}) \to 0 < \cos A$
6	3 5	elrpd	$⊢ A \in (0, \frac{π}{2}) \to \cos A \in ℝ^{+}$
7	6	rpne0d	$⊢ A \in (0, \frac{π}{2}) \to \cos A \neq 0$
8		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
9	2 7 8	syl2anc	$⊢ A \in (0, \frac{π}{2}) \to \tan A = \frac{\sin A}{\cos A}$
10	1	resincld	$⊢ A \in (0, \frac{π}{2}) \to \sin A \in ℝ$
11	4	simpld	$⊢ A \in (0, \frac{π}{2}) \to 0 < \sin A$
12	10 11	elrpd	$⊢ A \in (0, \frac{π}{2}) \to \sin A \in ℝ^{+}$
13	12 6	rpdivcld	$⊢ A \in (0, \frac{π}{2}) \to \frac{\sin A}{\cos A} \in ℝ^{+}$
14	9 13	eqeltrd	$⊢ A \in (0, \frac{π}{2}) \to \tan A \in ℝ^{+}$

Metamath Proof Explorer