Metamath Proof Explorer

Theorem 2efiatan

Description: Value of the exponential of an arctangent. (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 eqtrid ⊢ ( 𝐴 ∈ 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 mulridd ⊢ ( 𝐴 ∈ 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 ) )