Theorem tanval

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

	Ref	Expression
Assertion	tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to A\in ℂ$$
2		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
3	2	anim1i	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \left(\cos A\in ℂ\wedge \cos A\ne 0\right)$$
4		eldifsn	$$⊢\cos A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\cos A\in ℂ\wedge \cos A\ne 0\right)$$
5	3 4	sylibr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A\in \left(ℂ\setminus \left\{0\right\}\right)$$
6		cosf	$$⊢\cos :ℂ⟶ℂ$$
7		ffn	$$⊢\cos :ℂ⟶ℂ\to \cos Fnℂ$$
8		elpreima	$$⊢\cos Fnℂ\to \left(A\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cos A\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
9	6 7 8	mp2b	$$⊢A\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cos A\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
10	1 5 9	sylanbrc	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to A\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
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 =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$
15		ovex	$$⊢\frac{\sin A}{\cos A}\in \mathrm{V}$$
16	13 14 15	fvmpt	$$⊢A\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \tan A=\frac{\sin A}{\cos A}$$
17	10 16	syl	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$