Theorem efiatan

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

	Ref	Expression
Assertion	efiatan	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}=\frac{\sqrt{1+\mathrm{i}A}}{\sqrt{1-\mathrm{i}A}}$$

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 \mathrm{i}arctan\left(A\right)=\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		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4	3	a1i	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\in ℂ$$
5		halfcl	$$⊢\mathrm{i}\in ℂ\to \frac{\mathrm{i}}{2}\in ℂ$$
6	3 5	mp1i	$$⊢A\in \mathrm{dom}arctan\to \frac{\mathrm{i}}{2}\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
8		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)$$
9	8	simp1bi	$$⊢A\in \mathrm{dom}arctan\to A\in ℂ$$
10		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
11	3 9 10	sylancr	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}A\in ℂ$$
12		subcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1-\mathrm{i}A\in ℂ$$
13	7 11 12	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1-\mathrm{i}A\in ℂ$$
14	8	simp2bi	$$⊢A\in \mathrm{dom}arctan\to 1-\mathrm{i}A\ne 0$$
15	13 14	logcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1-\mathrm{i}A\right)\in ℂ$$
16		addcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1+\mathrm{i}A\in ℂ$$
17	7 11 16	sylancr	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A\in ℂ$$
18	8	simp3bi	$$⊢A\in \mathrm{dom}arctan\to 1+\mathrm{i}A\ne 0$$
19	17 18	logcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1+\mathrm{i}A\right)\in ℂ$$
20	15 19	subcld	$$⊢A\in \mathrm{dom}arctan\to \log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\in ℂ$$
21	4 6 20	mulassd	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
22		2cn	$$⊢2\in ℂ$$
23		2ne0	$$⊢2\ne 0$$
24		divneg	$$⊢\left(1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{1}{2}=\frac{-1}{2}$$
25	7 22 23 24	mp3an	$$⊢-\frac{1}{2}=\frac{-1}{2}$$
26		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
27	26	oveq1i	$$⊢\frac{\mathrm{i}\mathrm{i}}{2}=\frac{-1}{2}$$
28	3 3 22 23	divassi	$$⊢\frac{\mathrm{i}\mathrm{i}}{2}=\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)$$
29	25 27 28	3eqtr2i	$$⊢-\frac{1}{2}=\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)$$
30	29	oveq1i	$$⊢\left(-\frac{1}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\mathrm{i}\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
31		halfcn	$$⊢\frac{1}{2}\in ℂ$$
32		mulneg12	$$⊢\left(\frac{1}{2}\in ℂ\wedge \log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\in ℂ\right)\to \left(-\frac{1}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\left(\frac{1}{2}\right)\left(-\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)\right)$$
33	31 20 32	sylancr	$$⊢A\in \mathrm{dom}arctan\to \left(-\frac{1}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\left(\frac{1}{2}\right)\left(-\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)\right)$$
34	15 19	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)$$
35	34	oveq2d	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{1}{2}\right)\left(-\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)\right)=\left(\frac{1}{2}\right)\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)$$
36	31	a1i	$$⊢A\in \mathrm{dom}arctan\to \frac{1}{2}\in ℂ$$
37	36 19 15	subdid	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{1}{2}\right)\left(\log \left(1+\mathrm{i}A\right)-\log \left(1-\mathrm{i}A\right)\right)=\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)$$
38	33 35 37	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to \left(-\frac{1}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)=\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)$$
39	30 38	eqtr3id	$$⊢A\in \mathrm{dom}arctan\to \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(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)$$
40	2 21 39	3eqtr2d	$$⊢A\in \mathrm{dom}arctan\to \mathrm{i}arctan\left(A\right)=\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)$$
41	40	fveq2d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}={\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}$$
42		mulcl	$$⊢\left(\frac{1}{2}\in ℂ\wedge \log \left(1+\mathrm{i}A\right)\in ℂ\right)\to \left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)\in ℂ$$
43	31 19 42	sylancr	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)\in ℂ$$
44		mulcl	$$⊢\left(\frac{1}{2}\in ℂ\wedge \log \left(1-\mathrm{i}A\right)\in ℂ\right)\to \left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)\in ℂ$$
45	31 15 44	sylancr	$$⊢A\in \mathrm{dom}arctan\to \left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)\in ℂ$$
46		efsub	$$⊢\left(\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)\in ℂ\wedge \left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)\in ℂ\right)\to {\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}=\frac{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}}$$
47	43 45 46	syl2anc	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)-\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}=\frac{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}}$$
48	17 18 36	cxpefd	$$⊢A\in \mathrm{dom}arctan\to {\left(1+\mathrm{i}A\right)}^{\frac{1}{2}}={\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)}$$
49		cxpsqrt	$$⊢1+\mathrm{i}A\in ℂ\to {\left(1+\mathrm{i}A\right)}^{\frac{1}{2}}=\sqrt{1+\mathrm{i}A}$$
50	17 49	syl	$$⊢A\in \mathrm{dom}arctan\to {\left(1+\mathrm{i}A\right)}^{\frac{1}{2}}=\sqrt{1+\mathrm{i}A}$$
51	48 50	eqtr3d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)}=\sqrt{1+\mathrm{i}A}$$
52	13 14 36	cxpefd	$$⊢A\in \mathrm{dom}arctan\to {\left(1-\mathrm{i}A\right)}^{\frac{1}{2}}={\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}$$
53		cxpsqrt	$$⊢1-\mathrm{i}A\in ℂ\to {\left(1-\mathrm{i}A\right)}^{\frac{1}{2}}=\sqrt{1-\mathrm{i}A}$$
54	13 53	syl	$$⊢A\in \mathrm{dom}arctan\to {\left(1-\mathrm{i}A\right)}^{\frac{1}{2}}=\sqrt{1-\mathrm{i}A}$$
55	52 54	eqtr3d	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}=\sqrt{1-\mathrm{i}A}$$
56	51 55	oveq12d	$$⊢A\in \mathrm{dom}arctan\to \frac{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1+\mathrm{i}A\right)}}{{\mathrm{e}}^{\left(\frac{1}{2}\right)\log \left(1-\mathrm{i}A\right)}}=\frac{\sqrt{1+\mathrm{i}A}}{\sqrt{1-\mathrm{i}A}}$$
57	41 47 56	3eqtrd	$$⊢A\in \mathrm{dom}arctan\to {\mathrm{e}}^{\mathrm{i}arctan\left(A\right)}=\frac{\sqrt{1+\mathrm{i}A}}{\sqrt{1-\mathrm{i}A}}$$