Theorem 2efiatan

Description: Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		atanval	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
2	1	oveq2d	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}arctan\left(A\right)=2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
3		2cn	$$⊢2\in ℂ$$
4	3	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\in ℂ$$
7		atancl	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)\in ℂ$$
8	4 6 7	mulassd	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}arctan\left(A\right)=2\mathrm{i}arctan\left(A\right)$$
9		halfcl	$$⊢\mathrm{i}\in ℂ\to \frac{\mathrm{i}}{2}\in ℂ$$
10	5 9	ax-mp	$$⊢\frac{\mathrm{i}}{2}\in ℂ$$
11	3 5 10	mulassi	$$⊢2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)=2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)$$
12	3 5 10	mul12i	$$⊢2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)=\mathrm{i}2\left(\frac{\mathrm{i}}{2}\right)$$
13		2ne0	$$⊢2\ne 0$$
14	5 3 13	divcan2i	$$⊢2\left(\frac{\mathrm{i}}{2}\right)=\mathrm{i}$$
15	14	oveq2i	$$⊢\mathrm{i}2\left(\frac{\mathrm{i}}{2}\right)=\mathrm{i}\mathrm{i}$$
16		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
17	15 16	eqtri	$$⊢\mathrm{i}2\left(\frac{\mathrm{i}}{2}\right)=-1$$
18	11 12 17	3eqtri	$$⊢2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)=-1$$
19	18	oveq1i	$$⊢2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=-1\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
20		ax-1cn	$$⊢1\in ℂ$$
21		atandm2	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge 1-\mathrm{i}A\ne 0\wedge 1+\mathrm{i}A\ne 0\right)$$
22	21	simp1bi	$$⊢A\in \mathrm{dom}arctan\to A\in ℂ$$
23		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
24	5 22 23	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}A\in ℂ$$
25		subcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1-\mathrm{i}A\in ℂ$$
26	20 24 25	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1-\mathrm{i}A\in ℂ$$
27	21	simp2bi	$$⊢A\in \mathrm{dom}arctan\to 1-\mathrm{i}A\ne 0$$
28	26 27	logcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1-\mathrm{i}A\right)\in ℂ$$
29		addcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1+\mathrm{i}A\in ℂ$$
30	20 24 29	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A\in ℂ$$
31	21	simp3bi	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A\ne 0$$
32	30 31	logcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1+\mathrm{i}A\right)\in ℂ$$
33	28 32	subcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\in ℂ$$
34	33	mulm1d	$$⊢A\in \mathrm{dom}arctan\to -1\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=-\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
35	19 34	eqtrid	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=-\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
36		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
37	36	a1i	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\in ℂ$$
38	10	a1i	$$⊢A\in \mathrm{dom}arctan\to \frac{\mathrm{i}}{2}\in ℂ$$
39	37 38 33	mulassd	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
40	28 32	negsubdi2d	$$⊢A\in \mathrm{dom}arctan\to -\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)$$
41	35 39 40	3eqtr3d	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)$$
42	2 8 41	3eqtr3d	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}arctan\left(A\right)=\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)$$
43	42	fveq2d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{2\mathrm{i}arctan\left(A\right)}={\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)}$$
44		efsub	$$⊢\left(\log \left(1+\mathrm{i}A\right)\in ℂ\wedge \log \left(1-\mathrm{i}A\right)\in ℂ\right)\to {\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)}=\frac{{\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}}$$
45	32 28 44	syl2anc	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)}=\frac{{\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}}$$
46		eflog	$$⊢\left(1+\mathrm{i}A\in ℂ\wedge 1+\mathrm{i}A\ne 0\right)\to {\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}=1+\mathrm{i}A$$
47	30 31 46	syl2anc	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}=1+\mathrm{i}A$$
48		eflog	$$⊢\left(1-\mathrm{i}A\in ℂ\wedge 1-\mathrm{i}A\ne 0\right)\to {\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}=1-\mathrm{i}A$$
49	26 27 48	syl2anc	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}=1-\mathrm{i}A$$
50	47 49	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}}=\frac{1+\mathrm{i}A}{1-\mathrm{i}A}$$
51		negsub	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}+\left(-A\right)=\mathrm{i}-A$$
52	5 22 51	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+\left(-A\right)=\mathrm{i}-A$$
53	6	mulridd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\cdot 1=\mathrm{i}$$
54	16	oveq1i	$$⊢\mathrm{i}\mathrm{i}A=-1A$$
55	6 6 22	mulassd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\mathrm{i}A=\mathrm{i}\mathrm{i}A$$
56	22	mulm1d	$$⊢A\in \mathrm{dom}arctan\to -1A=-A$$
57	54 55 56	3eqtr3a	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\mathrm{i}A=-A$$
58	53 57	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\cdot 1+\mathrm{i}\mathrm{i}A=\mathrm{i}+\left(-A\right)$$
59	6 22 6	pnpcan2d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+\mathrm{i}-\left(A+\mathrm{i}\right)=\mathrm{i}-A$$
60	52 58 59	3eqtr4d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\cdot 1+\mathrm{i}\mathrm{i}A=\mathrm{i}+\mathrm{i}-\left(A+\mathrm{i}\right)$$
61	20	a1i	$$⊢A\in \mathrm{dom}arctan\to 1\in ℂ$$
62	6 61 24	adddid	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(1+\mathrm{i}A\right)=\mathrm{i}\cdot 1+\mathrm{i}\mathrm{i}A$$
63	6	2timesd	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}=\mathrm{i}+\mathrm{i}$$
64	63	oveq1d	$$⊢A\in \mathrm{dom}arctan\to 2\mathrm{i}-\left(A+\mathrm{i}\right)=\mathrm{i}+\mathrm{i}-\left(A+\mathrm{i}\right)$$
65	60 62 64	3eqtr4d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(1+\mathrm{i}A\right)=2\mathrm{i}-\left(A+\mathrm{i}\right)$$
66	6 61 24	subdid	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(1-\mathrm{i}A\right)=\mathrm{i}\cdot 1-\mathrm{i}\mathrm{i}A$$
67	53 57	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\cdot 1-\mathrm{i}\mathrm{i}A=\mathrm{i}-\left(-A\right)$$
68		subneg	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}-\left(-A\right)=\mathrm{i}+A$$
69	5 22 68	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}-\left(-A\right)=\mathrm{i}+A$$
70	67 69	eqtrd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\cdot 1-\mathrm{i}\mathrm{i}A=\mathrm{i}+A$$
71		addcom	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}+A=A+\mathrm{i}$$
72	5 22 71	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}+A=A+\mathrm{i}$$
73	66 70 72	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(1-\mathrm{i}A\right)=A+\mathrm{i}$$
74	65 73	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \frac{\mathrm{i}\left(1+\mathrm{i}A\right)}{\mathrm{i}\left(1-\mathrm{i}A\right)}=\frac{2\mathrm{i}-\left(A+\mathrm{i}\right)}{A+\mathrm{i}}$$
75		ine0	$$⊢\mathrm{i}\ne 0$$
76	75	a1i	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\ne 0$$
77	30 26 6 27 76	divcan5d	$$⊢A\in \mathrm{dom}arctan\to \frac{\mathrm{i}\left(1+\mathrm{i}A\right)}{\mathrm{i}\left(1-\mathrm{i}A\right)}=\frac{1+\mathrm{i}A}{1-\mathrm{i}A}$$
78		addcl	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\right)\to A+\mathrm{i}\in ℂ$$
79	22 5 78	sylancl	$$⊢A\in \mathrm{dom}arctan\to A+\mathrm{i}\in ℂ$$
80		subneg	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\right)\to A-\left(-\mathrm{i}\right)=A+\mathrm{i}$$
81	22 5 80	sylancl	$$⊢A\in \mathrm{dom}arctan\to A-\left(-\mathrm{i}\right)=A+\mathrm{i}$$
82		atandm	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A\ne -\mathrm{i}\wedge A\ne \mathrm{i}\right)$$
83	82	simp2bi	$$⊢A\in \mathrm{dom}arctan\to A\ne -\mathrm{i}$$
84		negicn	$$⊢-\mathrm{i}\in ℂ$$
85		subeq0	$$⊢\left(A\in ℂ\wedge -\mathrm{i}\in ℂ\right)\to \left(A-\left(-\mathrm{i}\right)=0\leftrightarrow A=-\mathrm{i}\right)$$
86	85	necon3bid	$$⊢\left(A\in ℂ\wedge -\mathrm{i}\in ℂ\right)\to \left(A-\left(-\mathrm{i}\right)\ne 0\leftrightarrow A\ne -\mathrm{i}\right)$$
87	22 84 86	sylancl	$$⊢A\in \mathrm{dom}arctan\to \left(A-\left(-\mathrm{i}\right)\ne 0\leftrightarrow A\ne -\mathrm{i}\right)$$
88	83 87	mpbird	$$⊢A\in \mathrm{dom}arctan\to A-\left(-\mathrm{i}\right)\ne 0$$
89	81 88	eqnetrrd	$$⊢A\in \mathrm{dom}arctan\to A+\mathrm{i}\ne 0$$
90	37 79 79 89	divsubdird	$$⊢A\in \mathrm{dom}arctan\to \frac{2\mathrm{i}-\left(A+\mathrm{i}\right)}{A+\mathrm{i}}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(\frac{A+\mathrm{i}}{A+\mathrm{i}}\right)$$
91	74 77 90	3eqtr3d	$$⊢A\in \mathrm{dom}arctan\to \frac{1+\mathrm{i}A}{1-\mathrm{i}A}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(\frac{A+\mathrm{i}}{A+\mathrm{i}}\right)$$
92	79 89	dividd	$$⊢A\in \mathrm{dom}arctan\to \frac{A+\mathrm{i}}{A+\mathrm{i}}=1$$
93	92	oveq2d	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-\left(\frac{A+\mathrm{i}}{A+\mathrm{i}}\right)=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1$$
94	50 91 93	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\log \left(1-\mathrm{i}A\right)}}=\left(\frac{2\mathrm{i}}{A+\mathrm{i}}\right)-1$$
95	43 45 94	3eqtrd	$$⊢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$$