Theorem cosatan

Description: The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	cosatan	$$⊢A\in \mathrm{dom}arctan\to \cos arctan\left(A\right)=\frac{1}{\sqrt{1+A^2}}$$

Proof

Step	Hyp	Ref	Expression
1		atancl	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)\in ℂ$$
2		cosval	$$⊢arctan\left(A\right)\in ℂ\to \cos arctan\left(A\right)=\frac{{\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}}{2}$$
3	1 2	syl	$$⊢A\in \mathrm{dom}arctan\to \cos arctan\left(A\right)=\frac{{\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}}{2}$$
4		efiatan2	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}=\frac{1+\mathrm{i}A}{\sqrt{1+A^2}}$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6		mulneg12	$$⊢\left(\mathrm{i}\in ℂ\wedge arctan\left(A\right)\in ℂ\right)\to \left(-\mathrm{i}\right)arctan\left(A\right)=\mathrm{i}\left(-arctan\left(A\right)\right)$$
7	5 1 6	sylancr	$$⊢A\in \mathrm{dom}arctan\to \left(-\mathrm{i}\right)arctan\left(A\right)=\mathrm{i}\left(-arctan\left(A\right)\right)$$
8		atanneg	$$⊢A\in \mathrm{dom}arctan\to arctan\left(-A\right)=-arctan\left(A\right)$$
9	8	oveq2d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}arctan\left(-A\right)=\mathrm{i}\left(-arctan\left(A\right)\right)$$
10	7 9	eqtr4d	$$⊢A\in \mathrm{dom}arctan\to \left(-\mathrm{i}\right)arctan\left(A\right)=\mathrm{i}arctan\left(-A\right)$$
11	10	fveq2d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}={\mathrm{e}}^{\mathrm{i}arctan\left(-A\right)}$$
12		atandmneg	$$⊢A\in \mathrm{dom}arctan\to -A\in \mathrm{dom}arctan$$
13		efiatan2	$$⊢-A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(-A\right)}=\frac{1+\mathrm{i}\left(-A\right)}{\sqrt{1+{\left(-A\right)}^2}}$$
14	12 13	syl	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(-A\right)}=\frac{1+\mathrm{i}\left(-A\right)}{\sqrt{1+{\left(-A\right)}^2}}$$
15		atandm4	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge 1+A^2\ne 0\right)$$
16	15	simplbi	$$⊢A\in \mathrm{dom}arctan\to A\in ℂ$$
17		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
18	5 16 17	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
19	18	oveq2d	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}\left(-A\right)=1+\left(-\mathrm{i}A\right)$$
20		ax-1cn	$$⊢1\in ℂ$$
21		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
22	5 16 21	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}A\in ℂ$$
23		negsub	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1+\left(-\mathrm{i}A\right)=1-\mathrm{i}A$$
24	20 22 23	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1+\left(-\mathrm{i}A\right)=1-\mathrm{i}A$$
25	19 24	eqtrd	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}\left(-A\right)=1-\mathrm{i}A$$
26		sqneg	$$⊢A\in ℂ\to {\left(-A\right)}^2=A^2$$
27	16 26	syl	$$⊢A\in \mathrm{dom}arctan\to {\left(-A\right)}^2=A^2$$
28	27	oveq2d	$$⊢A\in \mathrm{dom}arctan\to 1+{\left(-A\right)}^2=1+A^2$$
29	28	fveq2d	$$⊢A\in \mathrm{dom}arctan\to \sqrt{1+{\left(-A\right)}^2}=\sqrt{1+A^2}$$
30	25 29	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \frac{1+\mathrm{i}\left(-A\right)}{\sqrt{1+{\left(-A\right)}^2}}=\frac{1-\mathrm{i}A}{\sqrt{1+A^2}}$$
31	11 14 30	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}=\frac{1-\mathrm{i}A}{\sqrt{1+A^2}}$$
32	4 31	oveq12d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}=\left(\frac{1+\mathrm{i}A}{\sqrt{1+A^2}}\right)+\left(\frac{1-\mathrm{i}A}{\sqrt{1+A^2}}\right)$$
33		addcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1+\mathrm{i}A\in ℂ$$
34	20 22 33	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A\in ℂ$$
35		subcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1-\mathrm{i}A\in ℂ$$
36	20 22 35	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1-\mathrm{i}A\in ℂ$$
37	16	sqcld	$$⊢A\in \mathrm{dom}arctan\to A^2\in ℂ$$
38		addcl	$$⊢\left(1\in ℂ\wedge A^2\in ℂ\right)\to 1+A^2\in ℂ$$
39	20 37 38	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1+A^2\in ℂ$$
40	39	sqrtcld	$$⊢A\in \mathrm{dom}arctan\to \sqrt{1+A^2}\in ℂ$$
41	39	sqsqrtd	$$⊢A\in \mathrm{dom}arctan\to {\sqrt{1+A^2}}^2=1+A^2$$
42	15	simprbi	$$⊢A\in \mathrm{dom}arctan\to 1+A^2\ne 0$$
43	41 42	eqnetrd	$$⊢A\in \mathrm{dom}arctan\to {\sqrt{1+A^2}}^2\ne 0$$
44		sqne0	$$⊢\sqrt{1+A^2}\in ℂ\to \left({\sqrt{1+A^2}}^2\ne 0\leftrightarrow \sqrt{1+A^2}\ne 0\right)$$
45	40 44	syl	$$⊢A\in \mathrm{dom}arctan\to \left({\sqrt{1+A^2}}^2\ne 0\leftrightarrow \sqrt{1+A^2}\ne 0\right)$$
46	43 45	mpbid	$$⊢A\in \mathrm{dom}arctan\to \sqrt{1+A^2}\ne 0$$
47	34 36 40 46	divdird	$$⊢A\in \mathrm{dom}arctan\to \frac{1+\mathrm{i}A+\left(1-\mathrm{i}A\right)}{\sqrt{1+A^2}}=\left(\frac{1+\mathrm{i}A}{\sqrt{1+A^2}}\right)+\left(\frac{1-\mathrm{i}A}{\sqrt{1+A^2}}\right)$$
48	20	a1i	$$⊢A\in \mathrm{dom}arctan\to 1\in ℂ$$
49	48 22 48	ppncand	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A+\left(1-\mathrm{i}A\right)=1+1$$
50		df-2	$$⊢2=1+1$$
51	49 50	eqtr4di	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A+\left(1-\mathrm{i}A\right)=2$$
52	51	oveq1d	$$⊢A\in \mathrm{dom}arctan\to \frac{1+\mathrm{i}A+\left(1-\mathrm{i}A\right)}{\sqrt{1+A^2}}=\frac{2}{\sqrt{1+A^2}}$$
53	32 47 52	3eqtr2d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}=\frac{2}{\sqrt{1+A^2}}$$
54	53	oveq1d	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)arctan\left(A\right)}}{2}=\frac{\frac{2}{\sqrt{1+A^2}}}{2}$$
55		2cnd	$$⊢A\in \mathrm{dom}arctan\to 2\in ℂ$$
56		2ne0	$$⊢2\ne 0$$
57	56	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\ne 0$$
58	55 40 55 46 57	divdiv32d	$$⊢A\in \mathrm{dom}arctan\to \frac{\frac{2}{\sqrt{1+A^2}}}{2}=\frac{\frac{2}{2}}{\sqrt{1+A^2}}$$
59		2div2e1	$$⊢\frac{2}{2}=1$$
60	59	oveq1i	$$⊢\frac{\frac{2}{2}}{\sqrt{1+A^2}}=\frac{1}{\sqrt{1+A^2}}$$
61	58 60	eqtrdi	$$⊢A\in \mathrm{dom}arctan\to \frac{\frac{2}{\sqrt{1+A^2}}}{2}=\frac{1}{\sqrt{1+A^2}}$$
62	3 54 61	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to \cos arctan\left(A\right)=\frac{1}{\sqrt{1+A^2}}$$