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 · 𝐴 ) ) ) ) )