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 
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( tan ` A ) ) )

Proof

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