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