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

Metamath Proof Explorer

Theorem tanregt0

Description: The real part of the tangent of a complex number with real part in the open interval ( 0 (,) ( _pi / 2 ) ) is positive. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion tanregt0 ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( tan ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
3 2 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
4 3 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
5 3 rered ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
6 neghalfpire ⊢ - ( π / 2 ) ∈ ℝ
7 6 rexri ⊢ - ( π / 2 ) ∈ ℝ*
8 0re ⊢ 0 ∈ ℝ
9 pirp ⊢ π ∈ ℝ+
10 rphalfcl ⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
11 rpgt0 ⊢ ( ( π / 2 ) ∈ ℝ+ → 0 < ( π / 2 ) )
12 9 10 11 mp2b ⊢ 0 < ( π / 2 )
13 halfpire ⊢ ( π / 2 ) ∈ ℝ
14 lt0neg2 ⊢ ( ( π / 2 ) ∈ ℝ → ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) )
15 13 14 ax-mp ⊢ ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 )
16 12 15 mpbi ⊢ - ( π / 2 ) < 0
17 6 8 16 ltleii ⊢ - ( π / 2 ) ≤ 0
18 iooss1 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ - ( π / 2 ) ≤ 0 ) → ( 0 (,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) ) )
19 7 17 18 mp2an ⊢ ( 0 (,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) )
20 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) )
21 19 20 sselid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
22 5 21 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ℜ ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
23 cosne0 ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( ℜ ‘ ( ℜ ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ℜ ‘ 𝐴 ) ) ≠ 0 )
24 4 22 23 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ ( ℜ ‘ 𝐴 ) ) ≠ 0 )
25 4 24 tancld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℂ )
26 ax-icn ⊢ i ∈ ℂ
27 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
28 27 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
30 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
31 26 29 30 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
32 rpcoshcl ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( cos ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ+ )
33 28 32 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ+ )
34 33 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ≠ 0 )
35 31 34 tancld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
36 25 35 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ )
37 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
38 1 36 37 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
39 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
40 39 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
41 40 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( cos ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
42 cosne0 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
43 21 42 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
44 41 43 eqnetrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( cos ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 0 )
45 tanaddlem ⊢ ( ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) ∧ ( ( cos ‘ ( ℜ ‘ 𝐴 ) ) ≠ 0 ∧ ( cos ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ≠ 0 ) ) → ( ( cos ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 0 ↔ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 1 ) )
46 4 31 24 34 45 syl22anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( cos ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 0 ↔ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 1 ) )
47 44 46 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 1 )
48 47 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 1 ≠ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
49 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = 0 ↔ 1 = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
50 49 necon3bid ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ≠ 0 ↔ 1 ≠ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
51 1 36 50 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ≠ 0 ↔ 1 ≠ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
52 48 51 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ≠ 0 )
53 38 52 absrpcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ∈ ℝ+ )
54 2z ⊢ 2 ∈ ℤ
55 rpexpcl ⊢ ( ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ∈ ℝ+ )
56 53 54 55 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ∈ ℝ+ )
57 56 rprecred ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) ∈ ℝ )
58 38 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ∈ ℂ )
59 25 35 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ )
60 58 59 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
61 60 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ∈ ℝ )
62 56 rpreccld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) ∈ ℝ+ )
63 62 rpgt0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) )
64 3 24 retancld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
65 1re ⊢ 1 ∈ ℝ
66 retanhcl ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℝ )
67 28 66 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℝ )
68 67 resqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ∈ ℝ )
69 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ∈ ℝ ) → ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ∈ ℝ )
70 65 68 69 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ∈ ℝ )
71 tanrpcl ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ+ )
72 71 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ+ )
73 72 rpgt0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( tan ‘ ( ℜ ‘ 𝐴 ) ) )
74 absresq ⊢ ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℝ → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ↑ 2 ) = ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) )
75 67 74 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ↑ 2 ) = ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) )
76 tanhbnd ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ( - 1 (,) 1 ) )
77 28 76 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ( - 1 (,) 1 ) )
78 eliooord ⊢ ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ( - 1 (,) 1 ) → ( - 1 < ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∧ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) < 1 ) )
79 77 78 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( - 1 < ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∧ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) < 1 ) )
80 abslt ⊢ ( ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) < 1 ↔ ( - 1 < ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∧ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) < 1 ) ) )
81 67 65 80 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) < 1 ↔ ( - 1 < ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∧ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) < 1 ) ) )
82 79 81 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) < 1 )
83 67 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℂ )
84 83 abscld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ∈ ℝ )
85 65 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 1 ∈ ℝ )
86 83 absge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 ≤ ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
87 0le1 ⊢ 0 ≤ 1
88 87 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 ≤ 1 )
89 84 85 86 88 lt2sqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) < 1 ↔ ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
90 82 89 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ↑ 2 ) < ( 1 ↑ 2 ) )
91 sq1 ⊢ ( 1 ↑ 2 ) = 1
92 90 91 breqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ↑ 2 ) < 1 )
93 75 92 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) < 1 )
94 posdif ⊢ ( ( ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) < 1 ↔ 0 < ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
95 68 65 94 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) < 1 ↔ 0 < ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
96 93 95 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) )
97 64 70 73 96 mulgt0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
98 38 recjd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = ( ℜ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
99 resub ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( ℜ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ℜ ‘ 1 ) − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
100 1 36 99 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ℜ ‘ 1 ) − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
101 re1 ⊢ ( ℜ ‘ 1 ) = 1
102 101 oveq1i ⊢ ( ( ℜ ‘ 1 ) − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( 1 − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
103 64 35 remul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ℜ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
104 negicn ⊢ - i ∈ ℂ
105 104 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - i ∈ ℂ )
106 ine0 ⊢ i ≠ 0
107 26 106 negne0i ⊢ - i ≠ 0
108 107 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - i ≠ 0 )
109 35 105 108 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ∈ ℂ )
110 imre ⊢ ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ∈ ℂ → ( ℑ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) = ( ℜ ‘ ( - i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) ) )
111 109 110 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) = ( ℜ ‘ ( - i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) ) )
112 26 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → i ∈ ℂ )
113 106 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → i ≠ 0 )
114 35 112 113 divneg2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) = ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) )
115 67 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ∈ ℝ )
116 114 115 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ∈ ℝ )
117 116 reim0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) = 0 )
118 35 105 108 divcan2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( - i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) = ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) )
119 118 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( - i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / - i ) ) ) = ( ℜ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
120 111 117 119 3eqtr3rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = 0 )
121 120 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ℜ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 0 ) )
122 25 mul01d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 0 ) = 0 )
123 103 121 122 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = 0 )
124 123 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( 1 − 0 ) )
125 1m0e1 ⊢ ( 1 − 0 ) = 1
126 124 125 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = 1 )
127 102 126 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℜ ‘ 1 ) − ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = 1 )
128 98 100 127 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = 1 )
129 35 112 113 divcan2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) = ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) )
130 129 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
131 130 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) ) = ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
132 64 67 crred ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) ) = ( tan ‘ ( ℜ ‘ 𝐴 ) ) )
133 131 132 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( tan ‘ ( ℜ ‘ 𝐴 ) ) )
134 128 133 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( 1 · ( tan ‘ ( ℜ ‘ 𝐴 ) ) ) )
135 mulcom ⊢ ( ( 1 ∈ ℂ ∧ ( tan ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 · ( tan ‘ ( ℜ ‘ 𝐴 ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 1 ) )
136 1 25 135 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 · ( tan ‘ ( ℜ ‘ 𝐴 ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 1 ) )
137 134 136 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 1 ) )
138 25 83 83 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) )
139 38 imcjd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = - ( ℑ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
140 imsub ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( ℑ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
141 1 36 140 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
142 im1 ⊢ ( ℑ ‘ 1 ) = 0
143 142 oveq1i ⊢ ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( 0 − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
144 df-neg ⊢ - ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( 0 − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
145 143 144 eqtr4i ⊢ ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = - ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
146 64 35 immul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ℑ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
147 imval ⊢ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ → ( ℑ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
148 35 147 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
149 67 rered ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) = ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) )
150 148 149 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) )
151 150 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ℑ ‘ ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
152 146 151 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
153 152 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = - ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
154 145 153 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = - ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
155 141 154 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = - ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
156 155 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - ( ℑ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = - - ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
157 64 67 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ∈ ℝ )
158 157 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ∈ ℂ )
159 158 negnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → - - ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
160 139 156 159 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
161 130 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) ) = ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
162 64 67 crimd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( i · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) ) = ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) )
163 161 162 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) )
164 160 163 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
165 83 sqvald ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) = ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) )
166 165 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) · ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ) ) )
167 138 164 166 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) )
168 137 167 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) − ( ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 1 ) − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
169 58 59 remuld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( ℜ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℜ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) − ( ( ℑ ‘ ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) · ( ℑ ‘ ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) )
170 1 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 1 ∈ ℂ )
171 83 sqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ∈ ℂ )
172 25 170 171 subdid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) = ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · 1 ) − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
173 168 169 172 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( 1 − ( ( ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) / i ) ↑ 2 ) ) ) )
174 97 173 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
175 57 61 63 174 mulgt0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) )
176 40 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) = ( tan ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
177 tanadd ⊢ ( ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) ∧ ( ( cos ‘ ( ℜ ‘ 𝐴 ) ) ≠ 0 ∧ ( cos ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ≠ 0 ∧ ( cos ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) ≠ 0 ) ) → ( tan ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
178 4 31 24 34 44 177 syl23anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
179 recval ⊢ ( ( ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ∈ ℂ ∧ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ≠ 0 ) → ( 1 / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) )
180 38 52 179 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 1 / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) )
181 180 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( 1 / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
182 59 38 52 divrec2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( 1 / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
183 38 abscld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ∈ ℝ )
184 183 resqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ∈ ℝ )
185 184 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ∈ ℂ )
186 56 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ≠ 0 )
187 58 59 185 186 div23d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) = ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
188 181 182 187 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) / ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) = ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) )
189 176 178 188 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) = ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) )
190 60 185 186 divrec2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) = ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
191 189 190 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( tan ‘ 𝐴 ) = ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) )
192 191 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) = ( ℜ ‘ ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) )
193 57 60 remul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) = ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) )
194 192 193 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( ℜ ‘ ( tan ‘ 𝐴 ) ) = ( ( 1 / ( ( abs ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ↑ 2 ) ) · ( ℜ ‘ ( ( ∗ ‘ ( 1 − ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) · ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) · ( ( tan ‘ ( ℜ ‘ 𝐴 ) ) + ( tan ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) ) ) )
195 175 194 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( 0 (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( tan ‘ 𝐴 ) ) )