Metamath Proof Explorer


Theorem 2efiatan

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

Ref Expression
Assertion 2efiatan ( 𝐴 ∈ dom arctan → ( exp ‘ ( 2 · ( i · ( arctan ‘ 𝐴 ) ) ) ) = ( ( ( 2 · i ) / ( 𝐴 + i ) ) − 1 ) )

Proof

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