2efiatan

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

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

Proof

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

Metamath Proof Explorer

Theorem 2efiatan

Proof