This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efiatan

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

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

Proof

Step Hyp Ref Expression
1 atanval ⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( i · ( arctan ‘ 𝐴 ) ) = ( i · ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
3 ax-icn ⊢ i ∈ ℂ
4 3 a1i ⊢ ( 𝐴 ∈ dom arctan → i ∈ ℂ )
5 halfcl ⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
6 3 5 mp1i ⊢ ( 𝐴 ∈ dom arctan → ( i / 2 ) ∈ ℂ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
9 8 simp1bi ⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
10 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
11 3 9 10 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
12 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
13 7 11 12 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
14 8 simp2bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
15 13 14 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
16 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
17 7 11 16 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
18 8 simp3bi ⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
19 17 18 logcld ⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
20 15 19 subcld ⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
21 4 6 20 mulassd ⊢ ( 𝐴 ∈ dom arctan → ( ( i · ( i / 2 ) ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( i · ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
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 · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( i · ( i / 2 ) ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
31 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
32 mulneg12 ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ ) → ( - ( 1 / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
33 31 20 32 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( - ( 1 / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
34 15 19 negsubdi2d ⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
35 34 oveq2d ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
36 31 a1i ⊢ ( 𝐴 ∈ dom arctan → ( 1 / 2 ) ∈ ℂ )
37 36 19 15 subdid ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 / 2 ) · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
38 33 35 37 3eqtrd ⊢ ( 𝐴 ∈ dom arctan → ( - ( 1 / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
39 30 38 eqtr3id ⊢ ( 𝐴 ∈ dom arctan → ( ( i · ( i / 2 ) ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
40 2 21 39 3eqtr2d ⊢ ( 𝐴 ∈ dom arctan → ( i · ( arctan ‘ 𝐴 ) ) = ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
41 40 fveq2d ⊢ ( 𝐴 ∈ dom arctan → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) = ( exp ‘ ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) )
42 mulcl ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ ) → ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
43 31 19 42 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
44 mulcl ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ ) → ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
45 31 15 44 sylancr ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ )
46 efsub ⊢ ( ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ ∧ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ) → ( exp ‘ ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) = ( ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) / ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) )
47 43 45 46 syl2anc ⊢ ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) = ( ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) / ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) )
48 17 18 36 cxpefd ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 + ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
49 cxpsqrt ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 + ( i · 𝐴 ) ) ) )
50 17 49 syl ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 + ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 + ( i · 𝐴 ) ) ) )
51 48 50 eqtr3d ⊢ ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( √ ‘ ( 1 + ( i · 𝐴 ) ) ) )
52 13 14 36 cxpefd ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 − ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
53 cxpsqrt ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ → ( ( 1 − ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 − ( i · 𝐴 ) ) ) )
54 13 53 syl ⊢ ( 𝐴 ∈ dom arctan → ( ( 1 − ( i · 𝐴 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 − ( i · 𝐴 ) ) ) )
55 52 54 eqtr3d ⊢ ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( √ ‘ ( 1 − ( i · 𝐴 ) ) ) )
56 51 55 oveq12d ⊢ ( 𝐴 ∈ dom arctan → ( ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) / ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) = ( ( √ ‘ ( 1 + ( i · 𝐴 ) ) ) / ( √ ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
57 41 47 56 3eqtrd ⊢ ( 𝐴 ∈ dom arctan → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) = ( ( √ ‘ ( 1 + ( i · 𝐴 ) ) ) / ( √ ‘ ( 1 − ( i · 𝐴 ) ) ) ) )