Theorem atancj

Description: The arctangent function distributes under conjugation. (The condition that Re ( A ) =/= 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -u 1 and 1 , though.) (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atancj	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
2		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
3		fveq2	⊢ ( 𝐴 = - i → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ - i ) )
4		ax-icn	⊢ i ∈ ℂ
5	4	renegi	⊢ ( ℜ ‘ - i ) = - ( ℜ ‘ i )
6		rei	⊢ ( ℜ ‘ i ) = 0
7	6	negeqi	⊢ - ( ℜ ‘ i ) = - 0
8		neg0	⊢ - 0 = 0
9	5 7 8	3eqtri	⊢ ( ℜ ‘ - i ) = 0
10	3 9	eqtrdi	⊢ ( 𝐴 = - i → ( ℜ ‘ 𝐴 ) = 0 )
11	10	necon3i	⊢ ( ( ℜ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ - i )
12	2 11	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ≠ - i )
13		fveq2	⊢ ( 𝐴 = i → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ i ) )
14	13 6	eqtrdi	⊢ ( 𝐴 = i → ( ℜ ‘ 𝐴 ) = 0 )
15	14	necon3i	⊢ ( ( ℜ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ i )
16	2 15	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ≠ i )
17		atandm	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ - i ∧ 𝐴 ≠ i ) )
18	1 12 16 17	syl3anbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ dom arctan )
19		halfcl	⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
20	4 19	ax-mp	⊢ ( i / 2 ) ∈ ℂ
21		ax-1cn	⊢ 1 ∈ ℂ
22		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
23	4 1 22	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
24		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
25	21 23 24	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
26		atandm2	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
27	18 26	sylib	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
28	27	simp2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
29	25 28	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
30		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
31	21 23 30	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
32	27	simp3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
33	31 32	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
34	29 33	subcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
35		cjmul	⊢ ( ( ( i / 2 ) ∈ ℂ ∧ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
36	20 34 35	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
37		2ne0	⊢ 2 ≠ 0
38		2cn	⊢ 2 ∈ ℂ
39	4 38	cjdivi	⊢ ( 2 ≠ 0 → ( ∗ ‘ ( i / 2 ) ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) ) )
40	37 39	ax-mp	⊢ ( ∗ ‘ ( i / 2 ) ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) )
41		divneg	⊢ ( ( i ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( i / 2 ) = ( - i / 2 ) )
42	4 38 37 41	mp3an	⊢ - ( i / 2 ) = ( - i / 2 )
43		cji	⊢ ( ∗ ‘ i ) = - i
44		2re	⊢ 2 ∈ ℝ
45		cjre	⊢ ( 2 ∈ ℝ → ( ∗ ‘ 2 ) = 2 )
46	44 45	ax-mp	⊢ ( ∗ ‘ 2 ) = 2
47	43 46	oveq12i	⊢ ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) ) = ( - i / 2 )
48	42 47	eqtr4i	⊢ - ( i / 2 ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) )
49	40 48	eqtr4i	⊢ ( ∗ ‘ ( i / 2 ) ) = - ( i / 2 )
50	49	oveq1i	⊢ ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
51	34	cjcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ∈ ℂ )
52		mulneg12	⊢ ( ( ( i / 2 ) ∈ ℂ ∧ ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ∈ ℂ ) → ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
53	20 51 52	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
54	50 53	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
55		cjsub	⊢ ( ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ ∧ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
56	29 33 55	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
57		imsub	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
58	21 23 57	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
59		reim	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
60	59	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
61	60	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
62	58 61	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) )
63		df-neg	⊢ - ( ℜ ‘ 𝐴 ) = ( 0 − ( ℜ ‘ 𝐴 ) )
64		im1	⊢ ( ℑ ‘ 1 ) = 0
65	64	oveq1i	⊢ ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( 0 − ( ℜ ‘ 𝐴 ) )
66	63 65	eqtr4i	⊢ - ( ℜ ‘ 𝐴 ) = ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) )
67	62 66	eqtr4di	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = - ( ℜ ‘ 𝐴 ) )
68		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
69	68	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
70	69	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
71	70 2	negne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ℜ ‘ 𝐴 ) ≠ 0 )
72	67 71	eqnetrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) ≠ 0 )
73		logcj	⊢ ( ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ ∧ ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
74	25 72 73	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
75		cjsub	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) )
76	21 23 75	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) )
77		1re	⊢ 1 ∈ ℝ
78		cjre	⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
79	77 78	mp1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 1 ) = 1 )
80		cjmul	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
81	4 1 80	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
82	43	oveq1i	⊢ ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = ( - i · ( ∗ ‘ 𝐴 ) )
83		cjcl	⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
84	83	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
85		mulneg1	⊢ ( ( i ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( - i · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
86	4 84 85	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - i · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
87	82 86	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
88	81 87	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( i · 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
89	79 88	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) = ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) )
90		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
91	4 84 90	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
92		subneg	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
93	21 91 92	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
94	76 89 93	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
95	94	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
96	74 95	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
97		imadd	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
98	21 23 97	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
99	60	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( 0 + ( ℑ ‘ ( i · 𝐴 ) ) ) )
100	64	oveq1i	⊢ ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) = ( 0 + ( ℑ ‘ ( i · 𝐴 ) ) )
101	99 100	eqtr4di	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
102	70	addlidd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
103	98 101 102	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) )
104	103 2	eqnetrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) ≠ 0 )
105		logcj	⊢ ( ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ ∧ ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
106	31 104 105	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
107		cjadd	⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) )
108	21 23 107	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) )
109	79 88	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) = ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) )
110		negsub	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
111	21 91 110	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
112	108 109 111	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
113	112	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
114	106 113	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
115	96 114	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
116	56 115	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
117	116	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
118		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
119	21 91 118	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
120		atandmcj	⊢ ( 𝐴 ∈ dom arctan → ( ∗ ‘ 𝐴 ) ∈ dom arctan )
121	18 120	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ dom arctan )
122		atandm2	⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan ↔ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 ∧ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 ) )
123	122	simp3bi	⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
124	121 123	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
125	119 124	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ∈ ℂ )
126		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
127	21 91 126	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
128	122	simp2bi	⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
129	121 128	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
130	127 129	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ∈ ℂ )
131	125 130	negsubdi2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
132	117 131	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
133	132	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
134	36 54 133	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
135		atanval	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
136	18 135	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
137	136	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
138		atanval	⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( arctan ‘ ( ∗ ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
139	121 138	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( arctan ‘ ( ∗ ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
140	134 137 139	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) )
141	18 140	jca	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )