efiatan2

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

		Ref	Expression
	Assertion	efiatan2	$⊢ A \in dom arctan \to e^{i arctan (A)} = \frac{1 + i A}{\sqrt{1 + A^{2}}}$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		atancl	$⊢ A \in dom arctan \to arctan (A) \in ℂ$
3		mulcl	$⊢ (i \in ℂ \land arctan (A) \in ℂ) \to i arctan (A) \in ℂ$
4	1 2 3	sylancr	$⊢ A \in dom arctan \to i arctan (A) \in ℂ$
5		efcl	$⊢ i arctan (A) \in ℂ \to e^{i arctan (A)} \in ℂ$
6	4 5	syl	$⊢ A \in dom arctan \to e^{i arctan (A)} \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		atandm2	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
9	8	simp1bi	$⊢ A \in dom arctan \to A \in ℂ$
10	9	sqcld	$⊢ A \in dom arctan \to A^{2} \in ℂ$
11		addcl	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 + A^{2} \in ℂ$
12	7 10 11	sylancr	$⊢ A \in dom arctan \to 1 + A^{2} \in ℂ$
13	12	sqrtcld	$⊢ A \in dom arctan \to \sqrt{1 + A^{2}} \in ℂ$
14	12	sqsqrtd	$⊢ A \in dom arctan \to {\sqrt{1 + A^{2}}}^{2} = 1 + A^{2}$
15		atandm4	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 + A^{2} \neq 0)$
16	15	simprbi	$⊢ A \in dom arctan \to 1 + A^{2} \neq 0$
17	14 16	eqnetrd	$⊢ A \in dom arctan \to {\sqrt{1 + A^{2}}}^{2} \neq 0$
18		sqne0	$⊢ \sqrt{1 + A^{2}} \in ℂ \to ({\sqrt{1 + A^{2}}}^{2} \neq 0 \leftrightarrow \sqrt{1 + A^{2}} \neq 0)$
19	13 18	syl	$⊢ A \in dom arctan \to ({\sqrt{1 + A^{2}}}^{2} \neq 0 \leftrightarrow \sqrt{1 + A^{2}} \neq 0)$
20	17 19	mpbid	$⊢ A \in dom arctan \to \sqrt{1 + A^{2}} \neq 0$
21	6 13 20	divcan4d	$⊢ A \in dom arctan \to \frac{e^{i arctan (A)} \sqrt{1 + A^{2}}}{\sqrt{1 + A^{2}}} = e^{i arctan (A)}$
22		halfcn	$⊢ \frac{1}{2} \in ℂ$
23	12 16	logcld	$⊢ A \in dom arctan \to \log (1 + A^{2}) \in ℂ$
24		mulcl	$⊢ (\frac{1}{2} \in ℂ \land \log (1 + A^{2}) \in ℂ) \to (\frac{1}{2}) \log (1 + A^{2}) \in ℂ$
25	22 23 24	sylancr	$⊢ A \in dom arctan \to (\frac{1}{2}) \log (1 + A^{2}) \in ℂ$
26		efadd	$⊢ (i arctan (A) \in ℂ \land (\frac{1}{2}) \log (1 + A^{2}) \in ℂ) \to e^{i arctan (A) + (\frac{1}{2}) \log (1 + A^{2})} = e^{i arctan (A)} e^{(\frac{1}{2}) \log (1 + A^{2})}$
27	4 25 26	syl2anc	$⊢ A \in dom arctan \to e^{i arctan (A) + (\frac{1}{2}) \log (1 + A^{2})} = e^{i arctan (A)} e^{(\frac{1}{2}) \log (1 + A^{2})}$
28		2cn	$⊢ 2 \in ℂ$
29	28	a1i	$⊢ A \in dom arctan \to 2 \in ℂ$
30		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
31	1 9 30	sylancr	$⊢ A \in dom arctan \to i A \in ℂ$
32		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
33	7 31 32	sylancr	$⊢ A \in dom arctan \to 1 + i A \in ℂ$
34	8	simp3bi	$⊢ A \in dom arctan \to 1 + i A \neq 0$
35	33 34	logcld	$⊢ A \in dom arctan \to \log (1 + i A) \in ℂ$
36	29 35 4	subdid	$⊢ A \in dom arctan \to 2 (\log (1 + i A) - i arctan (A)) = 2 \log (1 + i A) - 2 i arctan (A)$
37		atanval	$⊢ A \in dom arctan \to arctan (A) = (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
38	37	oveq2d	$⊢ A \in dom arctan \to 2 i arctan (A) = 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
39	1	a1i	$⊢ A \in dom arctan \to i \in ℂ$
40	29 39 2	mulassd	$⊢ A \in dom arctan \to 2 i arctan (A) = 2 i arctan (A)$
41		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
42	1 41	ax-mp	$⊢ \frac{i}{2} \in ℂ$
43	28 1 42	mulassi	$⊢ 2 i (\frac{i}{2}) = 2 i (\frac{i}{2})$
44	28 1 42	mul12i	$⊢ 2 i (\frac{i}{2}) = i 2 (\frac{i}{2})$
45		2ne0	$⊢ 2 \neq 0$
46	1 28 45	divcan2i	$⊢ 2 (\frac{i}{2}) = i$
47	46	oveq2i	$⊢ i 2 (\frac{i}{2}) = i i$
48		ixi	$⊢ i i = - 1$
49	47 48	eqtri	$⊢ i 2 (\frac{i}{2}) = - 1$
50	43 44 49	3eqtri	$⊢ 2 i (\frac{i}{2}) = - 1$
51	50	oveq1i	$⊢ 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A)) = -1 (\log (1 - i A) - \log (1 + i A))$
52		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
53	7 31 52	sylancr	$⊢ A \in dom arctan \to 1 - i A \in ℂ$
54	8	simp2bi	$⊢ A \in dom arctan \to 1 - i A \neq 0$
55	53 54	logcld	$⊢ A \in dom arctan \to \log (1 - i A) \in ℂ$
56	55 35	subcld	$⊢ A \in dom arctan \to \log (1 - i A) - \log (1 + i A) \in ℂ$
57	56	mulm1d	$⊢ A \in dom arctan \to -1 (\log (1 - i A) - \log (1 + i A)) = - (\log (1 - i A) - \log (1 + i A))$
58	51 57	eqtrid	$⊢ A \in dom arctan \to 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A)) = - (\log (1 - i A) - \log (1 + i A))$
59		2mulicn	$⊢ 2 i \in ℂ$
60	59	a1i	$⊢ A \in dom arctan \to 2 i \in ℂ$
61	42	a1i	$⊢ A \in dom arctan \to \frac{i}{2} \in ℂ$
62	60 61 56	mulassd	$⊢ A \in dom arctan \to 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A)) = 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
63	55 35	negsubdi2d	$⊢ A \in dom arctan \to - (\log (1 - i A) - \log (1 + i A)) = \log (1 + i A) - \log (1 - i A)$
64	58 62 63	3eqtr3d	$⊢ A \in dom arctan \to 2 i (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A)) = \log (1 + i A) - \log (1 - i A)$
65	38 40 64	3eqtr3d	$⊢ A \in dom arctan \to 2 i arctan (A) = \log (1 + i A) - \log (1 - i A)$
66	65	oveq2d	$⊢ A \in dom arctan \to 2 \log (1 + i A) - 2 i arctan (A) = 2 \log (1 + i A) - (\log (1 + i A) - \log (1 - i A))$
67		mulcl	$⊢ (2 \in ℂ \land \log (1 + i A) \in ℂ) \to 2 \log (1 + i A) \in ℂ$
68	28 35 67	sylancr	$⊢ A \in dom arctan \to 2 \log (1 + i A) \in ℂ$
69	68 35 55	subsubd	$⊢ A \in dom arctan \to 2 \log (1 + i A) - (\log (1 + i A) - \log (1 - i A)) = 2 \log (1 + i A) - \log (1 + i A) + \log (1 - i A)$
70	35	2timesd	$⊢ A \in dom arctan \to 2 \log (1 + i A) = \log (1 + i A) + \log (1 + i A)$
71	35 35 70	mvrladdd	$⊢ A \in dom arctan \to 2 \log (1 + i A) - \log (1 + i A) = \log (1 + i A)$
72	71	oveq1d	$⊢ A \in dom arctan \to 2 \log (1 + i A) - \log (1 + i A) + \log (1 - i A) = \log (1 + i A) + \log (1 - i A)$
73		atanlogadd	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) \in ran log$
74		logef	$⊢ \log (1 + i A) + \log (1 - i A) \in ran log \to \log e^{\log (1 + i A) + \log (1 - i A)} = \log (1 + i A) + \log (1 - i A)$
75	73 74	syl	$⊢ A \in dom arctan \to \log e^{\log (1 + i A) + \log (1 - i A)} = \log (1 + i A) + \log (1 - i A)$
76		efadd	$⊢ (\log (1 + i A) \in ℂ \land \log (1 - i A) \in ℂ) \to e^{\log (1 + i A) + \log (1 - i A)} = e^{\log (1 + i A)} e^{\log (1 - i A)}$
77	35 55 76	syl2anc	$⊢ A \in dom arctan \to e^{\log (1 + i A) + \log (1 - i A)} = e^{\log (1 + i A)} e^{\log (1 - i A)}$
78		eflog	$⊢ (1 + i A \in ℂ \land 1 + i A \neq 0) \to e^{\log (1 + i A)} = 1 + i A$
79	33 34 78	syl2anc	$⊢ A \in dom arctan \to e^{\log (1 + i A)} = 1 + i A$
80		eflog	$⊢ (1 - i A \in ℂ \land 1 - i A \neq 0) \to e^{\log (1 - i A)} = 1 - i A$
81	53 54 80	syl2anc	$⊢ A \in dom arctan \to e^{\log (1 - i A)} = 1 - i A$
82	79 81	oveq12d	$⊢ A \in dom arctan \to e^{\log (1 + i A)} e^{\log (1 - i A)} = (1 + i A) (1 - i A)$
83		sq1	$⊢ 1^{2} = 1$
84	83	a1i	$⊢ A \in dom arctan \to 1^{2} = 1$
85		sqmul	$⊢ (i \in ℂ \land A \in ℂ) \to {i A}^{2} = i^{2} A^{2}$
86	1 9 85	sylancr	$⊢ A \in dom arctan \to {i A}^{2} = i^{2} A^{2}$
87		i2	$⊢ i^{2} = - 1$
88	87	oveq1i	$⊢ i^{2} A^{2} = -1 A^{2}$
89	10	mulm1d	$⊢ A \in dom arctan \to -1 A^{2} = - A^{2}$
90	88 89	eqtrid	$⊢ A \in dom arctan \to i^{2} A^{2} = - A^{2}$
91	86 90	eqtrd	$⊢ A \in dom arctan \to {i A}^{2} = - A^{2}$
92	84 91	oveq12d	$⊢ A \in dom arctan \to 1^{2} - {i A}^{2} = 1 - (- A^{2})$
93		subsq	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1^{2} - {i A}^{2} = (1 + i A) (1 - i A)$
94	7 31 93	sylancr	$⊢ A \in dom arctan \to 1^{2} - {i A}^{2} = (1 + i A) (1 - i A)$
95		subneg	$⊢ (1 \in ℂ \land A^{2} \in ℂ) \to 1 - (- A^{2}) = 1 + A^{2}$
96	7 10 95	sylancr	$⊢ A \in dom arctan \to 1 - (- A^{2}) = 1 + A^{2}$
97	92 94 96	3eqtr3d	$⊢ A \in dom arctan \to (1 + i A) (1 - i A) = 1 + A^{2}$
98	77 82 97	3eqtrd	$⊢ A \in dom arctan \to e^{\log (1 + i A) + \log (1 - i A)} = 1 + A^{2}$
99	98	fveq2d	$⊢ A \in dom arctan \to \log e^{\log (1 + i A) + \log (1 - i A)} = \log (1 + A^{2})$
100	75 99	eqtr3d	$⊢ A \in dom arctan \to \log (1 + i A) + \log (1 - i A) = \log (1 + A^{2})$
101	69 72 100	3eqtrd	$⊢ A \in dom arctan \to 2 \log (1 + i A) - (\log (1 + i A) - \log (1 - i A)) = \log (1 + A^{2})$
102	36 66 101	3eqtrd	$⊢ A \in dom arctan \to 2 (\log (1 + i A) - i arctan (A)) = \log (1 + A^{2})$
103	102	oveq1d	$⊢ A \in dom arctan \to \frac{2 (\log (1 + i A) - i arctan (A))}{2} = \frac{\log (1 + A^{2})}{2}$
104	35 4	subcld	$⊢ A \in dom arctan \to \log (1 + i A) - i arctan (A) \in ℂ$
105	45	a1i	$⊢ A \in dom arctan \to 2 \neq 0$
106	104 29 105	divcan3d	$⊢ A \in dom arctan \to \frac{2 (\log (1 + i A) - i arctan (A))}{2} = \log (1 + i A) - i arctan (A)$
107	23 29 105	divrec2d	$⊢ A \in dom arctan \to \frac{\log (1 + A^{2})}{2} = (\frac{1}{2}) \log (1 + A^{2})$
108	103 106 107	3eqtr3d	$⊢ A \in dom arctan \to \log (1 + i A) - i arctan (A) = (\frac{1}{2}) \log (1 + A^{2})$
109	35 4 25	subaddd	$⊢ A \in dom arctan \to (\log (1 + i A) - i arctan (A) = (\frac{1}{2}) \log (1 + A^{2}) \leftrightarrow i arctan (A) + (\frac{1}{2}) \log (1 + A^{2}) = \log (1 + i A))$
110	108 109	mpbid	$⊢ A \in dom arctan \to i arctan (A) + (\frac{1}{2}) \log (1 + A^{2}) = \log (1 + i A)$
111	110	fveq2d	$⊢ A \in dom arctan \to e^{i arctan (A) + (\frac{1}{2}) \log (1 + A^{2})} = e^{\log (1 + i A)}$
112	27 111	eqtr3d	$⊢ A \in dom arctan \to e^{i arctan (A)} e^{(\frac{1}{2}) \log (1 + A^{2})} = e^{\log (1 + i A)}$
113	22	a1i	$⊢ A \in dom arctan \to \frac{1}{2} \in ℂ$
114	12 16 113	cxpefd	$⊢ A \in dom arctan \to {(1 + A^{2})}^{\frac{1}{2}} = e^{(\frac{1}{2}) \log (1 + A^{2})}$
115		cxpsqrt	$⊢ 1 + A^{2} \in ℂ \to {(1 + A^{2})}^{\frac{1}{2}} = \sqrt{1 + A^{2}}$
116	12 115	syl	$⊢ A \in dom arctan \to {(1 + A^{2})}^{\frac{1}{2}} = \sqrt{1 + A^{2}}$
117	114 116	eqtr3d	$⊢ A \in dom arctan \to e^{(\frac{1}{2}) \log (1 + A^{2})} = \sqrt{1 + A^{2}}$
118	117	oveq2d	$⊢ A \in dom arctan \to e^{i arctan (A)} e^{(\frac{1}{2}) \log (1 + A^{2})} = e^{i arctan (A)} \sqrt{1 + A^{2}}$
119	112 118 79	3eqtr3d	$⊢ A \in dom arctan \to e^{i arctan (A)} \sqrt{1 + A^{2}} = 1 + i A$
120	119	oveq1d	$⊢ A \in dom arctan \to \frac{e^{i arctan (A)} \sqrt{1 + A^{2}}}{\sqrt{1 + A^{2}}} = \frac{1 + i A}{\sqrt{1 + A^{2}}}$
121	21 120	eqtr3d	$⊢ A \in dom arctan \to e^{i arctan (A)} = \frac{1 + i A}{\sqrt{1 + A^{2}}}$

Metamath Proof Explorer

Theorem efiatan2

Proof