Theorem atandmtan

Description: The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atandmtan	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A\in \mathrm{dom}arctan$$

Proof

Step	Hyp	Ref	Expression
1		tancl	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A\in ℂ$$
2		tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
3	2	oveq1d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\tan A}^2={\left(\frac{\sin A}{\cos A}\right)}^2$$
4		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
5	4	adantr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \sin A\in ℂ$$
6		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
7	6	adantr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A\in ℂ$$
8		simpr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A\ne 0$$
9	5 7 8	sqdivd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
10	3 9	eqtrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\tan A}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
11	5	sqcld	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2\in ℂ$$
12	7	sqcld	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\cos A}^2\in ℂ$$
13	12	negcld	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to -{\cos A}^2\in ℂ$$
14	11 12	subnegd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2-\left(-{\cos A}^2\right)={\sin A}^2+{\cos A}^2$$
15		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
16	15	adantr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2+{\cos A}^2=1$$
17	14 16	eqtrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2-\left(-{\cos A}^2\right)=1$$
18		ax-1ne0	$$⊢1\ne 0$$
19	18	a1i	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1\ne 0$$
20	17 19	eqnetrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2-\left(-{\cos A}^2\right)\ne 0$$
21	11 13 20	subne0ad	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2\ne -{\cos A}^2$$
22	12	mulm1d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to -1{\cos A}^2=-{\cos A}^2$$
23	21 22	neeqtrrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sin A}^2\ne -1{\cos A}^2$$
24		neg1cn	$$⊢-1\in ℂ$$
25	24	a1i	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to -1\in ℂ$$
26		sqne0	$$⊢\cos A\in ℂ\to \left({\cos A}^2\ne 0\leftrightarrow \cos A\ne 0\right)$$
27	6 26	syl	$$⊢A\in ℂ\to \left({\cos A}^2\ne 0\leftrightarrow \cos A\ne 0\right)$$
28	27	biimpar	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\cos A}^2\ne 0$$
29	11 25 12 28	divmul3d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \left(\frac{{\sin A}^2}{{\cos A}^2}=-1\leftrightarrow {\sin A}^2=-1{\cos A}^2\right)$$
30	29	necon3bid	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \left(\frac{{\sin A}^2}{{\cos A}^2}\ne -1\leftrightarrow {\sin A}^2\ne -1{\cos A}^2\right)$$
31	23 30	mpbird	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{{\sin A}^2}{{\cos A}^2}\ne -1$$
32	10 31	eqnetrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\tan A}^2\ne -1$$
33		atandm3	$$⊢\tan A\in \mathrm{dom}arctan\leftrightarrow \left(\tan A\in ℂ\wedge {\tan A}^2\ne -1\right)$$
34	1 32 33	sylanbrc	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A\in \mathrm{dom}arctan$$