Theorem onetansqsecsq

Description: Prove the tangent squared secant squared identity ( 1 + ( ( tan A ) ^ 2 ) ) = ( ( sec A ) ^ 2 ) ) . (Contributed by David A. Wheeler, 25-May-2015)

	Ref	Expression
Assertion	onetansqsecsq	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1+{\tan A}^2={\sec \left(A\right)}^2$$

Proof

Step	Hyp	Ref	Expression
1		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
2		sqeq0	$$⊢\cos A\in ℂ\to \left({\cos A}^2=0\leftrightarrow \cos A=0\right)$$
3	1 2	syl	$$⊢A\in ℂ\to \left({\cos A}^2=0\leftrightarrow \cos A=0\right)$$
4	3	necon3bid	$$⊢A\in ℂ\to \left({\cos A}^2\ne 0\leftrightarrow \cos A\ne 0\right)$$
5	4	biimpar	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\cos A}^2\ne 0$$
6	1	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
7		divid	$$⊢\left({\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\to \frac{{\cos A}^2}{{\cos A}^2}=1$$
8	6 7	sylan	$$⊢\left(A\in ℂ\wedge {\cos A}^2\ne 0\right)\to \frac{{\cos A}^2}{{\cos A}^2}=1$$
9	5 8	syldan	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{{\cos A}^2}{{\cos A}^2}=1$$
10	9	eqcomd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1=\frac{{\cos A}^2}{{\cos A}^2}$$
11		tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
12	11	oveq1d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\tan A}^2={\left(\frac{\sin A}{\cos A}\right)}^2$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
15		expdiv	$$⊢\left(\sin A\in ℂ\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
16	14 15	syl3an1	$$⊢\left(A\in ℂ\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
17	13 16	mp3an3	$$⊢\left(A\in ℂ\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
18	17	3impb	$$⊢\left(A\in ℂ\wedge \cos A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
19	1 18	syl3an2	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{\sin A}{\cos A}\right)}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
20	19	3anidm12	$$⊢\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}$$
21	12 20	eqtrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\tan A}^2=\frac{{\sin A}^2}{{\cos A}^2}$$
22	10 21	oveq12d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1+{\tan A}^2=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
23	14	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
24		divdir	$$⊢\left({\cos A}^2\in ℂ\wedge {\sin A}^2\in ℂ\wedge \left({\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
25	6 24	syl3an1	$$⊢\left(A\in ℂ\wedge {\sin A}^2\in ℂ\wedge \left({\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
26	23 25	syl3an2	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge \left({\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
27	26	3anidm12	$$⊢\left(A\in ℂ\wedge \left({\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
28	27	3impb	$$⊢\left(A\in ℂ\wedge {\cos A}^2\in ℂ\wedge {\cos A}^2\ne 0\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
29	6 28	syl3an2	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge {\cos A}^2\ne 0\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
30	29	3anidm12	$$⊢\left(A\in ℂ\wedge {\cos A}^2\ne 0\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
31	5 30	syldan	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\left(\frac{{\cos A}^2}{{\cos A}^2}\right)+\left(\frac{{\sin A}^2}{{\cos A}^2}\right)$$
32	22 31	eqtr4d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1+{\tan A}^2=\frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}$$
33	23 6	addcomd	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2={\cos A}^2+{\sin A}^2$$
34		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
35	33 34	eqtr3d	$$⊢A\in ℂ\to {\cos A}^2+{\sin A}^2=1$$
36	35	oveq1d	$$⊢A\in ℂ\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\frac{1}{{\cos A}^2}$$
37	36	adantr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{{\cos A}^2+{\sin A}^2}{{\cos A}^2}=\frac{1}{{\cos A}^2}$$
38	32 37	eqtrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1+{\tan A}^2=\frac{1}{{\cos A}^2}$$
39		secval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \sec \left(A\right)=\frac{1}{\cos A}$$
40	39	oveq1d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sec \left(A\right)}^2={\left(\frac{1}{\cos A}\right)}^2$$
41		ax-1cn	$$⊢1\in ℂ$$
42		expdiv	$$⊢\left(1\in ℂ\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{\cos A}\right)}^2=\frac{1^2}{{\cos A}^2}$$
43	41 13 42	mp3an13	$$⊢\left(\cos A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{1}{\cos A}\right)}^2=\frac{1^2}{{\cos A}^2}$$
44	1 43	sylan	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{1}{\cos A}\right)}^2=\frac{1^2}{{\cos A}^2}$$
45		sq1	$$⊢1^2=1$$
46	45	oveq1i	$$⊢\frac{1^2}{{\cos A}^2}=\frac{1}{{\cos A}^2}$$
47	44 46	eqtrdi	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\left(\frac{1}{\cos A}\right)}^2=\frac{1}{{\cos A}^2}$$
48	40 47	eqtrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to {\sec \left(A\right)}^2=\frac{1}{{\cos A}^2}$$
49	38 48	eqtr4d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to 1+{\tan A}^2={\sec \left(A\right)}^2$$