Theorem tanatan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	tanatan	$$⊢A\in \mathrm{dom}arctan\to \tan arctan\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		atancl	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)\in ℂ$$
2		2efiatan	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1$$
3	2	oveq1d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1+1$$
4		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
5	4	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\in ℂ$$
6		atandm	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A\ne -\mathrm{i}\wedge A\ne \mathrm{i}\right)$$
7	6	simp1bi	$$⊢A\in \mathrm{dom}arctan\to A\in ℂ$$
8		ax-icn	$$⊢\mathrm{i}\in ℂ$$
9		addcl	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\right)\to A+\mathrm{i}\in ℂ$$
10	7 8 9	sylancl	$$⊢A\in \mathrm{dom}arctan\to A+\mathrm{i}\in ℂ$$
11		subneg	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\right)\to A-\left(-\mathrm{i}\right)=A+\mathrm{i}$$
12	7 8 11	sylancl	$$⊢A\in \mathrm{dom}arctan\to A-\left(-\mathrm{i}\right)=A+\mathrm{i}$$
13	6	simp2bi	$$⊢A\in \mathrm{dom}arctan\to A\ne -\mathrm{i}$$
14	8	negcli	$$⊢-\mathrm{i}\in ℂ$$
15		subeq0	$$⊢\left(A\in ℂ\wedge -\mathrm{i}\in ℂ\right)\to \left(A-\left(-\mathrm{i}\right)=0\leftrightarrow A=-\mathrm{i}\right)$$
16	15	necon3bid	$$⊢\left(A\in ℂ\wedge -\mathrm{i}\in ℂ\right)\to \left(A-\left(-\mathrm{i}\right)\ne 0\leftrightarrow A\ne -\mathrm{i}\right)$$
17	7 14 16	sylancl	$$⊢A\in \mathrm{dom}arctan\to \left(A-\left(-\mathrm{i}\right)\ne 0\leftrightarrow A\ne -\mathrm{i}\right)$$
18	13 17	mpbird	$$⊢A\in \mathrm{dom}arctan\to A-\left(-\mathrm{i}\right)\ne 0$$
19	12 18	eqnetrrd	$$⊢A\in \mathrm{dom}arctan\to A+\mathrm{i}\ne 0$$
20	5 10 19	divcld	$$⊢A\in \mathrm{dom}arctan\to \frac{2\mathrm{i}}{A+\mathrm{i}}\in ℂ$$
21		ax-1cn	$$⊢1\in ℂ$$
22		npcan	$$⊢\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\in ℂ\wedge 1\in ℂ\right)\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1+1=\frac{2\mathrm{i}}{A+\mathrm{i}}$$
23	20 21 22	sylancl	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1+1=\frac{2\mathrm{i}}{A+\mathrm{i}}$$
24	3 23	eqtrd	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1=\frac{2\mathrm{i}}{A+\mathrm{i}}$$
25		2muline0	$$⊢2\mathrm{i}\ne 0$$
26	25	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\ne 0$$
27	5 10 26 19	divne0d	$$⊢A\in \mathrm{dom}arctan\to \frac{2\mathrm{i}}{A+\mathrm{i}}\ne 0$$
28	24 27	eqnetrd	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\ne 0$$
29		tanval3	$$⊢\left(arctan\left(A\right)\in ℂ\wedge {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\ne 0\right)\to \tan arctan\left(A\right)=\frac{{\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)}$$
30	1 28 29	syl2anc	$$⊢A\in \mathrm{dom}arctan\to \tan arctan\left(A\right)=\frac{{\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)}$$
31	2	oveq1d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1-1$$
32	21	a1i	$$⊢A\in \mathrm{dom}arctan\to 1\in ℂ$$
33	20 32 32	subsub4d	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1-1=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(1+1\right)$$
34		df-2	$$⊢2=1+1$$
35	34	oveq2i	$$⊢\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-2=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(1+1\right)$$
36	33 35	syl6eqr	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1-1=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-2$$
37	31 36	eqtrd	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-2$$
38		2cn	$$⊢2\in ℂ$$
39		mulcl	$$⊢\left(2\in ℂ\wedge A+\mathrm{i}\in ℂ\right)\to 2\left(A+\mathrm{i}\right)\in ℂ$$
40	38 10 39	sylancr	$$⊢A\in \mathrm{dom}arctan\to 2\left(A+\mathrm{i}\right)\in ℂ$$
41	5 40 10 19	divsubdird	$$⊢A\in \mathrm{dom}arctan\to \frac{2\mathrm{i}-2\left(A+\mathrm{i}\right)}{A+\mathrm{i}}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(\frac{2\left(A+\mathrm{i}\right)}{A+\mathrm{i}}\right)$$
42		mulneg12	$$⊢\left(2\in ℂ\wedge A\in ℂ\right)\to -2A=2\left(-A\right)$$
43	38 7 42	sylancr	$$⊢A\in \mathrm{dom}arctan\to -2A=2\left(-A\right)$$
44		negsub	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}+\left(-A\right)=\mathrm{i}-A$$
45	8 7 44	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+\left(-A\right)=\mathrm{i}-A$$
46	45	oveq1d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+\left(-A\right)-\mathrm{i}=\mathrm{i}-A-\mathrm{i}$$
47	7	negcld	$$⊢A\in \mathrm{dom}arctan\to -A\in ℂ$$
48		pncan2	$$⊢\left(\mathrm{i}\in ℂ\wedge -A\in ℂ\right)\to \mathrm{i}+\left(-A\right)-\mathrm{i}=-A$$
49	8 47 48	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+\left(-A\right)-\mathrm{i}=-A$$
50	8	a1i	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\in ℂ$$
51	50 7 50	subsub4d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}-A-\mathrm{i}=\mathrm{i}-\left(A+\mathrm{i}\right)$$
52	46 49 51	3eqtr3rd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}-\left(A+\mathrm{i}\right)=-A$$
53	52	oveq2d	$$⊢A\in \mathrm{dom}arctan\to 2\left(\mathrm{i}-\left(A+\mathrm{i}\right)\right)=2\left(-A\right)$$
54	38	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\in ℂ$$
55	54 50 10	subdid	$$⊢A\in \mathrm{dom}arctan\to 2\left(\mathrm{i}-\left(A+\mathrm{i}\right)\right)=2\mathrm{i}-2\left(A+\mathrm{i}\right)$$
56	43 53 55	3eqtr2rd	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}-2\left(A+\mathrm{i}\right)=-2A$$
57	56	oveq1d	$$⊢A\in \mathrm{dom}arctan\to \frac{2\mathrm{i}-2\left(A+\mathrm{i}\right)}{A+\mathrm{i}}=\frac{-2A}{A+\mathrm{i}}$$
58	54 10 19	divcan4d	$$⊢A\in \mathrm{dom}arctan\to \frac{2\left(A+\mathrm{i}\right)}{A+\mathrm{i}}=2$$
59	58	oveq2d	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(\frac{2\left(A+\mathrm{i}\right)}{A+\mathrm{i}}\right)=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-2$$
60	41 57 59	3eqtr3d	$$⊢A\in \mathrm{dom}arctan\to \frac{-2A}{A+\mathrm{i}}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-2$$
61	37 60	eqtr4d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1=\frac{-2A}{A+\mathrm{i}}$$
62	24	oveq2d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)=\mathrm{i}\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)$$
63	8 38 8	mul12i	$$⊢\mathrm{i}2\mathrm{i}=2\mathrm{i}\mathrm{i}$$
64		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
65	64	oveq2i	$$⊢2\mathrm{i}\mathrm{i}=2-1$$
66	21	negcli	$$⊢-1\in ℂ$$
67	38	mulm1i	$$⊢-1\cdot 2=-2$$
68	66 38 67	mulcomli	$$⊢2-1=-2$$
69	63 65 68	3eqtri	$$⊢\mathrm{i}2\mathrm{i}=-2$$
70	69	oveq1i	$$⊢\frac{\mathrm{i}2\mathrm{i}}{A+\mathrm{i}}=\frac{-2}{A+\mathrm{i}}$$
71	50 5 10 19	divassd	$$⊢A\in \mathrm{dom}arctan\to \frac{\mathrm{i}2\mathrm{i}}{A+\mathrm{i}}=\mathrm{i}\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)$$
72	70 71	syl5eqr	$$⊢A\in \mathrm{dom}arctan\to \frac{-2}{A+\mathrm{i}}=\mathrm{i}\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)$$
73	62 72	eqtr4d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)=\frac{-2}{A+\mathrm{i}}$$
74	61 73	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)}=\frac{\frac{-2A}{A+\mathrm{i}}}{\frac{-2}{A+\mathrm{i}}}$$
75	38	negcli	$$⊢-2\in ℂ$$
76		mulcl	$$⊢\left(-2\in ℂ\wedge A\in ℂ\right)\to -2A\in ℂ$$
77	75 7 76	sylancr	$$⊢A\in \mathrm{dom}arctan\to -2A\in ℂ$$
78	75	a1i	$$⊢A\in \mathrm{dom}arctan\to -2\in ℂ$$
79		2ne0	$$⊢2\ne 0$$
80	38 79	negne0i	$$⊢-2\ne 0$$
81	80	a1i	$$⊢A\in \mathrm{dom}arctan\to -2\ne 0$$
82	77 78 10 81 19	divcan7d	$$⊢A\in \mathrm{dom}arctan\to \frac{\frac{-2A}{A+\mathrm{i}}}{\frac{-2}{A+\mathrm{i}}}=\frac{-2A}{-2}$$
83	7 78 81	divcan3d	$$⊢A\in \mathrm{dom}arctan\to \frac{-2A}{-2}=A$$
84	82 83	eqtrd	$$⊢A\in \mathrm{dom}arctan\to \frac{\frac{-2A}{A+\mathrm{i}}}{\frac{-2}{A+\mathrm{i}}}=A$$
85	74 84	eqtrd	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}+1\right)}=A$$
86	30 85	eqtrd	$$⊢A\in \mathrm{dom}arctan\to \tan arctan\left(A\right)=A$$