Metamath Proof Explorer


Theorem efiatan

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

Ref Expression
Assertion efiatan A dom arctan e i arctan A = 1 + i A 1 i A

Proof

Step Hyp Ref Expression
1 atanval A dom arctan arctan A = i 2 log 1 i A log 1 + i A
2 1 oveq2d A dom arctan i arctan A = i i 2 log 1 i A log 1 + i A
3 ax-icn i
4 3 a1i A dom arctan i
5 halfcl i i 2
6 3 5 mp1i A dom arctan i 2
7 ax-1cn 1
8 atandm2 A dom arctan A 1 i A 0 1 + i A 0
9 8 simp1bi A dom arctan A
10 mulcl i A i A
11 3 9 10 sylancr A dom arctan i A
12 subcl 1 i A 1 i A
13 7 11 12 sylancr A dom arctan 1 i A
14 8 simp2bi A dom arctan 1 i A 0
15 13 14 logcld A dom arctan log 1 i A
16 addcl 1 i A 1 + i A
17 7 11 16 sylancr A dom arctan 1 + i A
18 8 simp3bi A dom arctan 1 + i A 0
19 17 18 logcld A dom arctan log 1 + i A
20 15 19 subcld A dom arctan log 1 i A log 1 + i A
21 4 6 20 mulassd A dom arctan i i 2 log 1 i A log 1 + i A = i i 2 log 1 i A log 1 + i A
22 2cn 2
23 2ne0 2 0
24 divneg 1 2 2 0 1 2 = 1 2
25 7 22 23 24 mp3an 1 2 = 1 2
26 ixi i i = 1
27 26 oveq1i i i 2 = 1 2
28 3 3 22 23 divassi i i 2 = i i 2
29 25 27 28 3eqtr2i 1 2 = i i 2
30 29 oveq1i 1 2 log 1 i A log 1 + i A = i i 2 log 1 i A log 1 + i A
31 halfcn 1 2
32 mulneg12 1 2 log 1 i A log 1 + i A 1 2 log 1 i A log 1 + i A = 1 2 log 1 i A log 1 + i A
33 31 20 32 sylancr A dom arctan 1 2 log 1 i A log 1 + i A = 1 2 log 1 i A log 1 + i A
34 15 19 negsubdi2d A dom arctan log 1 i A log 1 + i A = log 1 + i A log 1 i A
35 34 oveq2d A dom arctan 1 2 log 1 i A log 1 + i A = 1 2 log 1 + i A log 1 i A
36 31 a1i A dom arctan 1 2
37 36 19 15 subdid A dom arctan 1 2 log 1 + i A log 1 i A = 1 2 log 1 + i A 1 2 log 1 i A
38 33 35 37 3eqtrd A dom arctan 1 2 log 1 i A log 1 + i A = 1 2 log 1 + i A 1 2 log 1 i A
39 30 38 eqtr3id A dom arctan i i 2 log 1 i A log 1 + i A = 1 2 log 1 + i A 1 2 log 1 i A
40 2 21 39 3eqtr2d A dom arctan i arctan A = 1 2 log 1 + i A 1 2 log 1 i A
41 40 fveq2d A dom arctan e i arctan A = e 1 2 log 1 + i A 1 2 log 1 i A
42 mulcl 1 2 log 1 + i A 1 2 log 1 + i A
43 31 19 42 sylancr A dom arctan 1 2 log 1 + i A
44 mulcl 1 2 log 1 i A 1 2 log 1 i A
45 31 15 44 sylancr A dom arctan 1 2 log 1 i A
46 efsub 1 2 log 1 + i A 1 2 log 1 i A e 1 2 log 1 + i A 1 2 log 1 i A = e 1 2 log 1 + i A e 1 2 log 1 i A
47 43 45 46 syl2anc A dom arctan e 1 2 log 1 + i A 1 2 log 1 i A = e 1 2 log 1 + i A e 1 2 log 1 i A
48 17 18 36 cxpefd A dom arctan 1 + i A 1 2 = e 1 2 log 1 + i A
49 cxpsqrt 1 + i A 1 + i A 1 2 = 1 + i A
50 17 49 syl A dom arctan 1 + i A 1 2 = 1 + i A
51 48 50 eqtr3d A dom arctan e 1 2 log 1 + i A = 1 + i A
52 13 14 36 cxpefd A dom arctan 1 i A 1 2 = e 1 2 log 1 i A
53 cxpsqrt 1 i A 1 i A 1 2 = 1 i A
54 13 53 syl A dom arctan 1 i A 1 2 = 1 i A
55 52 54 eqtr3d A dom arctan e 1 2 log 1 i A = 1 i A
56 51 55 oveq12d A dom arctan e 1 2 log 1 + i A e 1 2 log 1 i A = 1 + i A 1 i A
57 41 47 56 3eqtrd A dom arctan e i arctan A = 1 + i A 1 i A