tancl

Description: The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014)

		Ref	Expression
	Assertion	tancl	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A \in ℂ$

Step	Hyp	Ref	Expression
1		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
2		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
3	2	adantr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \sin A \in ℂ$
4		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
5	4	adantr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \cos A \in ℂ$
6		simpr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \cos A \neq 0$
7	3 5 6	divcld	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{\sin A}{\cos A} \in ℂ$
8	1 7	eqeltrd	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A \in ℂ$

Metamath Proof Explorer