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

Metamath Proof Explorer

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 ‘ 𝐴 ) ) = 𝐴 )