Theorem atantan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 5-Apr-2015)

	Ref	Expression
Assertion	atantan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arctan ‘ ( tan ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cosne0	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
2		atandmtan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) ∈ dom arctan )
3	1 2	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) ∈ dom arctan )
4		atanval	⊢ ( ( tan ‘ 𝐴 ) ∈ dom arctan → ( arctan ‘ ( tan ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arctan ‘ ( tan ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) )
6		ax-1cn	⊢ 1 ∈ ℂ
7		ax-icn	⊢ i ∈ ℂ
8		tancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) ∈ ℂ )
9	1 8	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) ∈ ℂ )
10		mulcl	⊢ ( ( i ∈ ℂ ∧ ( tan ‘ 𝐴 ) ∈ ℂ ) → ( i · ( tan ‘ 𝐴 ) ) ∈ ℂ )
11	7 9 10	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( tan ‘ 𝐴 ) ) ∈ ℂ )
12		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( tan ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ )
13	6 11 12	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ )
14		atandm2	⊢ ( ( tan ‘ 𝐴 ) ∈ dom arctan ↔ ( ( tan ‘ 𝐴 ) ∈ ℂ ∧ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ∧ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ) )
15	3 14	sylib	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( tan ‘ 𝐴 ) ∈ ℂ ∧ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ∧ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ) )
16	15	simp3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 )
17	13 16	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℂ )
18		subcl	⊢ ( ( 1 ∈ ℂ ∧ ( i · ( tan ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ )
19	6 11 18	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ )
20	15	simp2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 )
21	19 20	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℂ )
22	17 21	negsubdi2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) )
23		efsub	⊢ ( ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℂ ∧ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) = ( ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) / ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) )
24	17 21 23	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) = ( ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) / ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) )
25		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
26	25	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ∈ ℂ )
27		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
28	27	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ 𝐴 ) ∈ ℂ )
29		mulcl	⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
30	7 28 29	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
31	26 30 26 1	divdird	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) + ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) )
32	26 1	dividd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) = 1 )
33	7	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → i ∈ ℂ )
34	33 28 26 1	divassd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( i · ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ) )
35		tanval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
36	1 35	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
37	36	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( tan ‘ 𝐴 ) ) = ( i · ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ) )
38	34 37	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( i · ( tan ‘ 𝐴 ) ) )
39	32 38	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) + ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) = ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) )
40	31 39	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) = ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) )
41		efival	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
42	41	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
43	42	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) )
44		eflog	⊢ ( ( ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ ∧ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) )
45	13 16 44	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) )
46	40 43 45	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) )
47	26 30 26 1	divsubdird	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) − ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) )
48	32 38	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) − ( ( i · ( sin ‘ 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) = ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) )
49	47 48	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) = ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) )
50		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
51	50	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - 𝐴 ∈ ℂ )
52		efival	⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) )
53	51 52	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) )
54		cosneg	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
55	54	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
56		sinneg	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )
57	56	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )
58	57	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ - 𝐴 ) ) = ( i · - ( sin ‘ 𝐴 ) ) )
59		mulneg2	⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
60	7 28 59	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
61	58 60	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ - 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
62	55 61	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ - 𝐴 ) + ( i · ( sin ‘ - 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) )
63	53 62	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · - 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) )
64		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 𝐴 ∈ ℂ )
65		mulneg2	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
66	7 64 65	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
67	66	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · - 𝐴 ) ) = ( exp ‘ - ( i · 𝐴 ) ) )
68	26 30	negsubd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
69	63 67 68	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ - ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
70	69	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ - ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) / ( cos ‘ 𝐴 ) ) )
71		eflog	⊢ ( ( ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℂ ∧ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) )
72	19 20 71	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) )
73	49 70 72	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ - ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) = ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) )
74	46 73	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) / ( ( exp ‘ - ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) = ( ( exp ‘ ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) / ( exp ‘ ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) )
75		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
76	7 64 75	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ℂ )
77		efcl	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
78	76 77	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
79	76	negcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( i · 𝐴 ) ∈ ℂ )
80		efcl	⊢ ( - ( i · 𝐴 ) ∈ ℂ → ( exp ‘ - ( i · 𝐴 ) ) ∈ ℂ )
81	79 80	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ - ( i · 𝐴 ) ) ∈ ℂ )
82		efne0	⊢ ( - ( i · 𝐴 ) ∈ ℂ → ( exp ‘ - ( i · 𝐴 ) ) ≠ 0 )
83	79 82	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ - ( i · 𝐴 ) ) ≠ 0 )
84	78 81 26 83 1	divcan7d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) / ( ( exp ‘ - ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) / ( exp ‘ - ( i · 𝐴 ) ) ) )
85		efsub	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ - ( i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) / ( exp ‘ - ( i · 𝐴 ) ) ) )
86	76 79 85	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) / ( exp ‘ - ( i · 𝐴 ) ) ) )
87	76 76	subnegd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
88	76	2timesd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
89	87 88	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) = ( 2 · ( i · 𝐴 ) ) )
90	89	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( ( i · 𝐴 ) − - ( i · 𝐴 ) ) ) = ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) )
91	84 86 90	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) / ( ( exp ‘ - ( i · 𝐴 ) ) / ( cos ‘ 𝐴 ) ) ) = ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) )
92	24 74 91	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) = ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) )
93	92	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) ) = ( log ‘ ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ) )
94	64	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
95	94	renegd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
96	94	recld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
97	96	renegcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℜ ‘ 𝐴 ) ∈ ℝ )
98		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ 𝐴 ) < 0 )
99	96	lt0neg1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( ℜ ‘ 𝐴 ) < 0 ↔ 0 < - ( ℜ ‘ 𝐴 ) ) )
100	98 99	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < - ( ℜ ‘ 𝐴 ) )
101		eliooord	⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
102	101	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
103	102	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( π / 2 ) < ( ℜ ‘ 𝐴 ) )
104	103	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( π / 2 ) < ( ℜ ‘ 𝐴 ) )
105		halfpire	⊢ ( π / 2 ) ∈ ℝ
106		ltnegcon1	⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ↔ - ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
107	105 96 106	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ↔ - ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
108	104 107	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℜ ‘ 𝐴 ) < ( π / 2 ) )
109		0xr	⊢ 0 ∈ ℝ*
110	105	rexri	⊢ ( π / 2 ) ∈ ℝ*
111		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( - ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( ℜ ‘ 𝐴 ) ∧ - ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) ) )
112	109 110 111	mp2an	⊢ ( - ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( - ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( ℜ ‘ 𝐴 ) ∧ - ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
113	97 100 108 112	syl3anbrc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) )
114	95 113	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) )
115		tanregt0	⊢ ( ( - 𝐴 ∈ ℂ ∧ ( ℜ ‘ - 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( tan ‘ - 𝐴 ) ) )
116	51 114 115	syl2an2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < ( ℜ ‘ ( tan ‘ - 𝐴 ) ) )
117		tanneg	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ - 𝐴 ) = - ( tan ‘ 𝐴 ) )
118	1 117	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( tan ‘ - 𝐴 ) = - ( tan ‘ 𝐴 ) )
119	118	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( tan ‘ - 𝐴 ) = - ( tan ‘ 𝐴 ) )
120	119	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ ( tan ‘ - 𝐴 ) ) = ( ℜ ‘ - ( tan ‘ 𝐴 ) ) )
121	9	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( tan ‘ 𝐴 ) ∈ ℂ )
122	121	renegd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - ( tan ‘ 𝐴 ) ) = - ( ℜ ‘ ( tan ‘ 𝐴 ) ) )
123	120 122	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ ( tan ‘ - 𝐴 ) ) = - ( ℜ ‘ ( tan ‘ 𝐴 ) ) )
124	116 123	breqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < - ( ℜ ‘ ( tan ‘ 𝐴 ) ) )
125	9	recld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) ∈ ℝ )
126	125	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) ∈ ℝ )
127	126	lt0neg1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( ℜ ‘ ( tan ‘ 𝐴 ) ) < 0 ↔ 0 < - ( ℜ ‘ ( tan ‘ 𝐴 ) ) ) )
128	124 127	mpbird	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) < 0 )
129	128	lt0ne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) ≠ 0 )
130		atanlogsub	⊢ ( ( ( tan ‘ 𝐴 ) ∈ dom arctan ∧ ( ℜ ‘ ( tan ‘ 𝐴 ) ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
131	3 129 130	syl2an2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
132		1re	⊢ 1 ∈ ℝ
133		ioossre	⊢ ( - 1 (,) 1 ) ⊆ ℝ
134	7	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → i ∈ ℂ )
135	11	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( tan ‘ 𝐴 ) ) ∈ ℂ )
136		ine0	⊢ i ≠ 0
137	136	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → i ≠ 0 )
138		ixi	⊢ ( i · i ) = - 1
139	138	oveq1i	⊢ ( ( i · i ) · ( tan ‘ 𝐴 ) ) = ( - 1 · ( tan ‘ 𝐴 ) )
140	9	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( tan ‘ 𝐴 ) ∈ ℂ )
141	140	mulm1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - 1 · ( tan ‘ 𝐴 ) ) = - ( tan ‘ 𝐴 ) )
142	118	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( tan ‘ - 𝐴 ) = - ( tan ‘ 𝐴 ) )
143	141 142	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - 1 · ( tan ‘ 𝐴 ) ) = ( tan ‘ - 𝐴 ) )
144	139 143	eqtrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · i ) · ( tan ‘ 𝐴 ) ) = ( tan ‘ - 𝐴 ) )
145	134 134 140	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · i ) · ( tan ‘ 𝐴 ) ) = ( i · ( i · ( tan ‘ 𝐴 ) ) ) )
146	138	oveq1i	⊢ ( ( i · i ) · 𝐴 ) = ( - 1 · 𝐴 )
147	64	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
148	147	mulm1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - 1 · 𝐴 ) = - 𝐴 )
149	146 148	eqtrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · i ) · 𝐴 ) = - 𝐴 )
150	134 134 147	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · i ) · 𝐴 ) = ( i · ( i · 𝐴 ) ) )
151	149 150	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → - 𝐴 = ( i · ( i · 𝐴 ) ) )
152	151	fveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( tan ‘ - 𝐴 ) = ( tan ‘ ( i · ( i · 𝐴 ) ) ) )
153	144 145 152	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( i · ( tan ‘ 𝐴 ) ) ) = ( tan ‘ ( i · ( i · 𝐴 ) ) ) )
154	134 135 137 153	mvllmuld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( tan ‘ 𝐴 ) ) = ( ( tan ‘ ( i · ( i · 𝐴 ) ) ) / i ) )
155	76	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · 𝐴 ) ∈ ℂ )
156		reim	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
157	156	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
158	157	eqeq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ℜ ‘ 𝐴 ) = 0 ↔ ( ℑ ‘ ( i · 𝐴 ) ) = 0 ) )
159	158	biimpa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ℑ ‘ ( i · 𝐴 ) ) = 0 )
160	155 159	reim0bd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · 𝐴 ) ∈ ℝ )
161		tanhbnd	⊢ ( ( i · 𝐴 ) ∈ ℝ → ( ( tan ‘ ( i · ( i · 𝐴 ) ) ) / i ) ∈ ( - 1 (,) 1 ) )
162	160 161	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( tan ‘ ( i · ( i · 𝐴 ) ) ) / i ) ∈ ( - 1 (,) 1 ) )
163	154 162	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( tan ‘ 𝐴 ) ) ∈ ( - 1 (,) 1 ) )
164	133 163	sselid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( tan ‘ 𝐴 ) ) ∈ ℝ )
165		readdcl	⊢ ( ( 1 ∈ ℝ ∧ ( i · ( tan ‘ 𝐴 ) ) ∈ ℝ ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ )
166	132 164 165	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ )
167		df-neg	⊢ - 1 = ( 0 − 1 )
168		eliooord	⊢ ( ( i · ( tan ‘ 𝐴 ) ) ∈ ( - 1 (,) 1 ) → ( - 1 < ( i · ( tan ‘ 𝐴 ) ) ∧ ( i · ( tan ‘ 𝐴 ) ) < 1 ) )
169	163 168	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( - 1 < ( i · ( tan ‘ 𝐴 ) ) ∧ ( i · ( tan ‘ 𝐴 ) ) < 1 ) )
170	169	simpld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → - 1 < ( i · ( tan ‘ 𝐴 ) ) )
171	167 170	eqbrtrrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( 0 − 1 ) < ( i · ( tan ‘ 𝐴 ) ) )
172		0red	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → 0 ∈ ℝ )
173	132	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → 1 ∈ ℝ )
174	172 173 164	ltsubadd2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( 0 − 1 ) < ( i · ( tan ‘ 𝐴 ) ) ↔ 0 < ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) )
175	171 174	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → 0 < ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) )
176	166 175	elrpd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ+ )
177	176	relogcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℝ )
178	169	simprd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( i · ( tan ‘ 𝐴 ) ) < 1 )
179		difrp	⊢ ( ( ( i · ( tan ‘ 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( i · ( tan ‘ 𝐴 ) ) < 1 ↔ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ+ ) )
180	164 132 179	sylancl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( i · ( tan ‘ 𝐴 ) ) < 1 ↔ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ+ ) )
181	178 180	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ∈ ℝ+ )
182	181	relogcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ∈ ℝ )
183	177 182	resubcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ℝ )
184		relogrn	⊢ ( ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ℝ → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
185	183 184	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ℜ ‘ 𝐴 ) = 0 ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
186	64	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
187	186	recld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
188		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ 𝐴 ) )
189	102	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) < ( π / 2 ) )
190	189	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) < ( π / 2 ) )
191		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) ) )
192	109 110 191	mp2an	⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
193	187 188 190 192	syl3anbrc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) )
194		tanregt0	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( tan ‘ 𝐴 ) ) )
195	64 193 194	syl2an2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ ( tan ‘ 𝐴 ) ) )
196	195	gt0ne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) ≠ 0 )
197	3 196 130	syl2an2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
198		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
199	198	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
200		0re	⊢ 0 ∈ ℝ
201		lttri4	⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) < 0 ∨ ( ℜ ‘ 𝐴 ) = 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) )
202	199 200 201	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ℜ ‘ 𝐴 ) < 0 ∨ ( ℜ ‘ 𝐴 ) = 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) )
203	131 185 197 202	mpjao3dan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log )
204		logef	⊢ ( ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ∈ ran log → ( log ‘ ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) )
205	203 204	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) )
206		2cn	⊢ 2 ∈ ℂ
207		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 2 · ( i · 𝐴 ) ) ∈ ℂ )
208	206 76 207	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · 𝐴 ) ) ∈ ℂ )
209		picn	⊢ π ∈ ℂ
210		2ne0	⊢ 2 ≠ 0
211		divneg	⊢ ( ( π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( π / 2 ) = ( - π / 2 ) )
212	209 206 210 211	mp3an	⊢ - ( π / 2 ) = ( - π / 2 )
213	212 103	eqbrtrrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - π / 2 ) < ( ℜ ‘ 𝐴 ) )
214		pire	⊢ π ∈ ℝ
215	214	renegcli	⊢ - π ∈ ℝ
216	215	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π ∈ ℝ )
217		2re	⊢ 2 ∈ ℝ
218	217	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ∈ ℝ )
219		2pos	⊢ 0 < 2
220	219	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < 2 )
221		ltdivmul	⊢ ( ( - π ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( - π / 2 ) < ( ℜ ‘ 𝐴 ) ↔ - π < ( 2 · ( ℜ ‘ 𝐴 ) ) ) )
222	216 199 218 220 221	syl112anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( - π / 2 ) < ( ℜ ‘ 𝐴 ) ↔ - π < ( 2 · ( ℜ ‘ 𝐴 ) ) ) )
223	213 222	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( 2 · ( ℜ ‘ 𝐴 ) ) )
224		immul2	⊢ ( ( 2 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) = ( 2 · ( ℑ ‘ ( i · 𝐴 ) ) ) )
225	217 76 224	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) = ( 2 · ( ℑ ‘ ( i · 𝐴 ) ) ) )
226	157	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ℜ ‘ 𝐴 ) ) = ( 2 · ( ℑ ‘ ( i · 𝐴 ) ) ) )
227	225 226	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) = ( 2 · ( ℜ ‘ 𝐴 ) ) )
228	223 227	breqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) )
229		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 2 · ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
230	217 199 229	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
231	214	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → π ∈ ℝ )
232		ltmuldiv2	⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · ( ℜ ‘ 𝐴 ) ) < π ↔ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
233	199 231 218 220 232	syl112anc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( 2 · ( ℜ ‘ 𝐴 ) ) < π ↔ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
234	189 233	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ℜ ‘ 𝐴 ) ) < π )
235	230 231 234	ltled	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ℜ ‘ 𝐴 ) ) ≤ π )
236	227 235	eqbrtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) ≤ π )
237		ellogrn	⊢ ( ( 2 · ( i · 𝐴 ) ) ∈ ran log ↔ ( ( 2 · ( i · 𝐴 ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) ∧ ( ℑ ‘ ( 2 · ( i · 𝐴 ) ) ) ≤ π ) )
238	208 228 236 237	syl3anbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · 𝐴 ) ) ∈ ran log )
239		logef	⊢ ( ( 2 · ( i · 𝐴 ) ) ∈ ran log → ( log ‘ ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ) = ( 2 · ( i · 𝐴 ) ) )
240	238 239	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ) = ( 2 · ( i · 𝐴 ) ) )
241	93 205 240	3eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) = ( 2 · ( i · 𝐴 ) ) )
242	241	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) ) = - ( 2 · ( i · 𝐴 ) ) )
243	22 242	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) = - ( 2 · ( i · 𝐴 ) ) )
244	243	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( tan ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( tan ‘ 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( 2 · ( i · 𝐴 ) ) ) )
245		halfcl	⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
246	7 245	mp1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i / 2 ) ∈ ℂ )
247	206	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ∈ ℂ )
248	246 247 79	mulassd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( i / 2 ) · 2 ) · - ( i · 𝐴 ) ) = ( ( i / 2 ) · ( 2 · - ( i · 𝐴 ) ) ) )
249	7 206 210	divcan1i	⊢ ( ( i / 2 ) · 2 ) = i
250	249	oveq1i	⊢ ( ( ( i / 2 ) · 2 ) · - ( i · 𝐴 ) ) = ( i · - ( i · 𝐴 ) )
251	33 33 51	mulassd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · i ) · - 𝐴 ) = ( i · ( i · - 𝐴 ) ) )
252	138	oveq1i	⊢ ( ( i · i ) · - 𝐴 ) = ( - 1 · - 𝐴 )
253		mul2neg	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - 1 · - 𝐴 ) = ( 1 · 𝐴 ) )
254	6 64 253	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - 1 · - 𝐴 ) = ( 1 · 𝐴 ) )
255		mullid	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
256	255	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 · 𝐴 ) = 𝐴 )
257	254 256	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - 1 · - 𝐴 ) = 𝐴 )
258	252 257	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · i ) · - 𝐴 ) = 𝐴 )
259	66	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( i · - 𝐴 ) ) = ( i · - ( i · 𝐴 ) ) )
260	251 258 259	3eqtr3rd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · - ( i · 𝐴 ) ) = 𝐴 )
261	250 260	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( i / 2 ) · 2 ) · - ( i · 𝐴 ) ) = 𝐴 )
262		mulneg2	⊢ ( ( 2 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 2 · - ( i · 𝐴 ) ) = - ( 2 · ( i · 𝐴 ) ) )
263	206 76 262	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · - ( i · 𝐴 ) ) = - ( 2 · ( i · 𝐴 ) ) )
264	263	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i / 2 ) · ( 2 · - ( i · 𝐴 ) ) ) = ( ( i / 2 ) · - ( 2 · ( i · 𝐴 ) ) ) )
265	248 261 264	3eqtr3rd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i / 2 ) · - ( 2 · ( i · 𝐴 ) ) ) = 𝐴 )
266	5 244 265	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arctan ‘ ( tan ‘ 𝐴 ) ) = 𝐴 )