tanval

Description: Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014)

		Ref	Expression
	Assertion	tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℂ \land \cos A \neq 0) \to A \in ℂ$
2		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
3	2	anim1i	$⊢ (A \in ℂ \land \cos A \neq 0) \to (\cos A \in ℂ \land \cos A \neq 0)$
4		eldifsn	$⊢ \cos A \in (ℂ ∖ \{0\}) \leftrightarrow (\cos A \in ℂ \land \cos A \neq 0)$
5	3 4	sylibr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \cos A \in (ℂ ∖ \{0\})$
6		cosf	$⊢ \cos : ℂ ⟶ ℂ$
7		ffn	$⊢ \cos : ℂ ⟶ ℂ \to \cos Fn ℂ$
8		elpreima	$⊢ \cos Fn ℂ \to (A \in \cos^{-1} [ℂ ∖ \{0\}] \leftrightarrow (A \in ℂ \land \cos A \in (ℂ ∖ \{0\})))$
9	6 7 8	mp2b	$⊢ A \in \cos^{-1} [ℂ ∖ \{0\}] \leftrightarrow (A \in ℂ \land \cos A \in (ℂ ∖ \{0\}))$
10	1 5 9	sylanbrc	$⊢ (A \in ℂ \land \cos A \neq 0) \to A \in \cos^{-1} [ℂ ∖ \{0\}]$
11		fveq2	$⊢ x = A \to \sin x = \sin A$
12		fveq2	$⊢ x = A \to \cos x = \cos A$
13	11 12	oveq12d	$⊢ x = A \to \frac{\sin x}{\cos x} = \frac{\sin A}{\cos A}$
14		df-tan	$⊢ \tan = (x \in \cos^{-1} [ℂ ∖ \{0\}] ⟼ \frac{\sin x}{\cos x})$
15		ovex	$⊢ \frac{\sin A}{\cos A} \in V$
16	13 14 15	fvmpt	$⊢ A \in \cos^{-1} [ℂ ∖ \{0\}] \to \tan A = \frac{\sin A}{\cos A}$
17	10 16	syl	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$

Metamath Proof Explorer