MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tanregt0 Unicode version

Theorem tanregt0 19954
Description: The positivity of  tan ( A ) extends to complex numbers with the same real part. (Contributed by Mario Carneiro, 5-Apr-2015.)
Assertion
Ref Expression
tanregt0  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( Re `  ( tan `  A
) ) )

Proof of Theorem tanregt0
StepHypRef Expression
1 ax-1cn 8840 . . . . . . 7  |-  1  e.  CC
2 recl 11642 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
Re `  A )  e.  RR )
32adantr 451 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  A
)  e.  RR )
43recnd 8906 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  A
)  e.  CC )
53rered 11756 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
Re `  A )
)  =  ( Re
`  A ) )
6 ressxr 8921 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
7 pire 19885 . . . . . . . . . . . . . . . 16  |-  pi  e.  RR
8 rehalfcl 9985 . . . . . . . . . . . . . . . 16  |-  ( pi  e.  RR  ->  (
pi  /  2 )  e.  RR )
97, 8ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( pi 
/  2 )  e.  RR
109renegcli 9153 . . . . . . . . . . . . . 14  |-  -u (
pi  /  2 )  e.  RR
116, 10sselii 3211 . . . . . . . . . . . . 13  |-  -u (
pi  /  2 )  e.  RR*
12 0re 8883 . . . . . . . . . . . . . 14  |-  0  e.  RR
13 pipos 19886 . . . . . . . . . . . . . . . . . 18  |-  0  <  pi
147, 13elrpii 10404 . . . . . . . . . . . . . . . . 17  |-  pi  e.  RR+
15 rphalfcl 10425 . . . . . . . . . . . . . . . . 17  |-  ( pi  e.  RR+  ->  ( pi 
/  2 )  e.  RR+ )
1614, 15ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( pi 
/  2 )  e.  RR+
17 rpgt0 10412 . . . . . . . . . . . . . . . 16  |-  ( ( pi  /  2 )  e.  RR+  ->  0  < 
( pi  /  2
) )
1816, 17ax-mp 8 . . . . . . . . . . . . . . 15  |-  0  <  ( pi  /  2
)
19 lt0neg2 9326 . . . . . . . . . . . . . . . 16  |-  ( ( pi  /  2 )  e.  RR  ->  (
0  <  ( pi  /  2 )  <->  -u ( pi 
/  2 )  <  0 ) )
209, 19ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 0  <  ( pi  / 
2 )  <->  -u ( pi 
/  2 )  <  0 )
2118, 20mpbi 199 . . . . . . . . . . . . . 14  |-  -u (
pi  /  2 )  <  0
2210, 12, 21ltleii 8986 . . . . . . . . . . . . 13  |-  -u (
pi  /  2 )  <_  0
23 iooss1 10738 . . . . . . . . . . . . 13  |-  ( (
-u ( pi  / 
2 )  e.  RR*  /\  -u ( pi  /  2
)  <_  0 )  ->  ( 0 (,) ( pi  /  2
) )  C_  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
2411, 22, 23mp2an 653 . . . . . . . . . . . 12  |-  ( 0 (,) ( pi  / 
2 ) )  C_  ( -u ( pi  / 
2 ) (,) (
pi  /  2 ) )
25 simpr 447 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  A
)  e.  ( 0 (,) ( pi  / 
2 ) ) )
2624, 25sseldi 3212 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  A
)  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
275, 26eqeltrd 2390 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
Re `  A )
)  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
28 cosne0 19945 . . . . . . . . . 10  |-  ( ( ( Re `  A
)  e.  CC  /\  ( Re `  ( Re
`  A ) )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  (
Re `  A )
)  =/=  0 )
294, 27, 28syl2anc 642 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  (
Re `  A )
)  =/=  0 )
304, 29tancld 12459 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( tan `  (
Re `  A )
)  e.  CC )
31 ax-icn 8841 . . . . . . . . . 10  |-  _i  e.  CC
32 imcl 11643 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
Im `  A )  e.  RR )
3332adantr 451 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  A
)  e.  RR )
3433recnd 8906 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  A
)  e.  CC )
35 mulcl 8866 . . . . . . . . . 10  |-  ( ( _i  e.  CC  /\  ( Im `  A )  e.  CC )  -> 
( _i  x.  (
Im `  A )
)  e.  CC )
3631, 34, 35sylancr 644 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( _i  x.  (
Im `  A )
)  e.  CC )
37 rpcoshcl 12484 . . . . . . . . . . 11  |-  ( ( Im `  A )  e.  RR  ->  ( cos `  ( _i  x.  ( Im `  A ) ) )  e.  RR+ )
3833, 37syl 15 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  (
_i  x.  ( Im `  A ) ) )  e.  RR+ )
3938rpne0d 10442 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  (
_i  x.  ( Im `  A ) ) )  =/=  0 )
4036, 39tancld 12459 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( tan `  (
_i  x.  ( Im `  A ) ) )  e.  CC )
4130, 40mulcld 8900 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) )  e.  CC )
42 subcl 9096 . . . . . . 7  |-  ( ( 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 )
431, 41, 42sylancr 644 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  -  (
( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) )  e.  CC )
44 replim 11648 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  =  ( ( Re
`  A )  +  ( _i  x.  (
Im `  A )
) ) )
4544adantr 451 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  A  =  ( (
Re `  A )  +  ( _i  x.  ( Im `  A ) ) ) )
4645fveq2d 5567 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  A
)  =  ( cos `  ( ( Re `  A )  +  ( _i  x.  ( Im
`  A ) ) ) ) )
47 cosne0 19945 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  A
)  =/=  0 )
4826, 47syldan 456 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  A
)  =/=  0 )
4946, 48eqnetrrd 2499 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( cos `  (
( Re `  A
)  +  ( _i  x.  ( Im `  A ) ) ) )  =/=  0 )
50 tanaddlem 12493 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
514, 36, 29, 39, 50syl22anc 1183 . . . . . . . . 9  |-  ( ( 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 ) )
5249, 51mpbid 201 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) )  =/=  1 )
5352necomd 2562 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
1  =/=  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) )
54 subeq0 9118 . . . . . . . . 9  |-  ( ( 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 )
) ) ) ) )
5554necon3bid 2514 . . . . . . . 8  |-  ( ( 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 )
) ) ) ) )
561, 41, 55sylancr 644 . . . . . . 7  |-  ( ( 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 )
) ) ) ) )
5753, 56mpbird 223 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  -  (
( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) )  =/=  0 )
5843, 57absrpcld 11977 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  e.  RR+ )
59 2z 10101 . . . . 5  |-  2  e.  ZZ
60 rpexpcl 11169 . . . . 5  |-  ( ( ( 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+ )
6158, 59, 60sylancl 643 . . . 4  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 )  e.  RR+ )
6261rprecred 10448 . . 3  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  /  (
( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 ) )  e.  RR )
6343cjcld 11728 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( * `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  e.  CC )
6430, 40addcld 8899 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  +  ( tan `  ( _i  x.  (
Im `  A )
) ) )  e.  CC )
6563, 64mulcld 8900 . . . 4  |-  ( ( 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 )
6665recld 11726 . . 3  |-  ( ( 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 )
6761rpreccld 10447 . . . 4  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  /  (
( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 ) )  e.  RR+ )
6867rpgt0d 10440 . . 3  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( 1  /  ( ( abs `  ( 1  -  (
( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) ) ^ 2 ) ) )
693, 29retancld 12472 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( tan `  (
Re `  A )
)  e.  RR )
70 1re 8882 . . . . . 6  |-  1  e.  RR
71 retanhcl 12486 . . . . . . . 8  |-  ( ( Im `  A )  e.  RR  ->  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  RR )
7233, 71syl 15 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  RR )
7372resqcld 11318 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ^ 2 )  e.  RR )
74 resubcl 9156 . . . . . 6  |-  ( ( 1  e.  RR  /\  ( ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ^ 2 )  e.  RR )  ->  (
1  -  ( ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ^
2 ) )  e.  RR )
7570, 73, 74sylancr 644 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  -  (
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ^
2 ) )  e.  RR )
76 tanrpcl 19925 . . . . . . 7  |-  ( ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) )  ->  ( tan `  ( Re `  A ) )  e.  RR+ )
7776adantl 452 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( tan `  (
Re `  A )
)  e.  RR+ )
7877rpgt0d 10440 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( tan `  ( Re `  A
) ) )
79 absresq 11834 . . . . . . . 8  |-  ( ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  RR  ->  ( ( abs `  ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ) ^ 2 )  =  ( ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ^
2 ) )
8072, 79syl 15 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) ^ 2 )  =  ( ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ^ 2 ) )
81 tanhbnd 12488 . . . . . . . . . . . 12  |-  ( ( Im `  A )  e.  RR  ->  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  ( -u 1 (,) 1 ) )
8233, 81syl 15 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  ( -u 1 (,) 1 ) )
83 eliooord 10757 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
8482, 83syl 15 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( -u 1  <  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  /\  ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  <  1 ) )
85 abslt 11845 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
8672, 70, 85sylancl 643 . . . . . . . . . 10  |-  ( ( 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 ) ) )
8784, 86mpbird 223 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( abs `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) )  <  1 )
8872recnd 8906 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  CC )
8988abscld 11965 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( abs `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) )  e.  RR )
9070a1i 10 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
1  e.  RR )
9188absge0d 11973 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <_  ( abs `  ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) )
92 0le1 9342 . . . . . . . . . . 11  |-  0  <_  1
9392a1i 10 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <_  1 )
9489, 90, 91, 93lt2sqd 11326 . . . . . . . . 9  |-  ( ( 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 ) ) )
9587, 94mpbid 201 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) ^ 2 )  < 
( 1 ^ 2 ) )
96 sq1 11245 . . . . . . . 8  |-  ( 1 ^ 2 )  =  1
9795, 96syl6breq 4099 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) ^ 2 )  <  1 )
9880, 97eqbrtrrd 4082 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ^ 2 )  <  1 )
99 posdif 9312 . . . . . . 7  |-  ( ( ( ( ( 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 ) ) ) )
10073, 70, 99sylancl 643 . . . . . 6  |-  ( ( 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 ) ) ) )
10198, 100mpbid 201 . . . . 5  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( 1  -  ( ( ( tan `  ( _i  x.  ( Im `  A ) ) )  /  _i ) ^
2 ) ) )
10269, 75, 78, 101mulgt0d 9016 . . . 4  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( ( tan `  ( Re `  A ) )  x.  ( 1  -  (
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ^
2 ) ) ) )
10343recjd 11736 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) ) ) )
104 resub 11659 . . . . . . . . . 10  |-  ( ( 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 )
) ) ) ) ) )
1051, 41, 104sylancr 644 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) ) ) )
106 re1 11686 . . . . . . . . . . 11  |-  ( Re
`  1 )  =  1
107106oveq1i 5910 . . . . . . . . . 10  |-  ( ( Re `  1 )  -  ( Re `  ( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) )  =  ( 1  -  ( Re `  ( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) )
10869, 40remul2d 11759 . . . . . . . . . . . . 13  |-  ( ( 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 )
) ) ) ) )
10931negcli 9159 . . . . . . . . . . . . . . . . . 18  |-  -u _i  e.  CC
110109a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  -u _i  e.  CC )
111 ine0 9260 . . . . . . . . . . . . . . . . . . 19  |-  _i  =/=  0
11231, 111negne0i 9166 . . . . . . . . . . . . . . . . . 18  |-  -u _i  =/=  0
113112a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  -u _i  =/=  0 )
11440, 110, 113divcld 9581 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  -u _i )  e.  CC )
115 imre 11640 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
116114, 115syl 15 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) )
11731a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  _i  e.  CC )
118111a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  _i  =/=  0 )
11940, 117, 118divneg2d 9595 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  -u ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  =  ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  -u _i ) )
12072renegcld 9255 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  ->  -u ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i )  e.  RR )
121119, 120eqeltrrd 2391 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  -u _i )  e.  RR )
122121reim0d 11757 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  -u _i ) )  =  0 )
12340, 110, 113divcan2d 9583 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( -u _i  x.  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  -u _i ) )  =  ( tan `  (
_i  x.  ( Im `  A ) ) ) )
124123fveq2d 5567 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) ) )
125116, 122, 1243eqtr3rd 2357 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  ( tan `  ( _i  x.  ( Im `  A ) ) ) )  =  0 )
126125oveq2d 5916 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  ( Re
`  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) )  =  ( ( tan `  (
Re `  A )
)  x.  0 ) )
12730mul01d 9056 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  0 )  =  0 )
128108, 126, 1273eqtrd 2352 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) )  =  0 )
129128oveq2d 5916 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  -  (
Re `  ( ( tan `  ( Re `  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  =  ( 1  -  0 ) )
1301subid1i 9163 . . . . . . . . . . 11  |-  ( 1  -  0 )  =  1
131129, 130syl6eq 2364 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  -  (
Re `  ( ( tan `  ( Re `  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  =  1 )
132107, 131syl5eq 2360 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( Re ` 
1 )  -  (
Re `  ( ( tan `  ( Re `  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  =  1 )
133103, 105, 1323eqtrd 2352 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
* `  ( 1  -  ( ( tan `  ( Re `  A
) )  x.  ( tan `  ( _i  x.  ( Im `  A ) ) ) ) ) ) )  =  1 )
13440, 117, 118divcan2d 9583 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( _i  x.  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) )  =  ( tan `  (
_i  x.  ( Im `  A ) ) ) )
135134oveq2d 5916 . . . . . . . . . 10  |-  ( ( 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 )
) ) ) )
136135fveq2d 5567 . . . . . . . . 9  |-  ( ( 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 )
) ) ) ) )
13769, 72crred 11763 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
( tan `  (
Re `  A )
)  +  ( _i  x.  ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ) ) )  =  ( tan `  (
Re `  A )
) )
138136, 137eqtr3d 2350 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
( tan `  (
Re `  A )
)  +  ( tan `  ( _i  x.  (
Im `  A )
) ) ) )  =  ( tan `  (
Re `  A )
) )
139133, 138oveq12d 5918 . . . . . . 7  |-  ( ( 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 )
) ) )
140 mulcom 8868 . . . . . . . 8  |-  ( ( 1  e.  CC  /\  ( tan `  ( Re
`  A ) )  e.  CC )  -> 
( 1  x.  ( tan `  ( Re `  A ) ) )  =  ( ( tan `  ( Re `  A
) )  x.  1 ) )
1411, 30, 140sylancr 644 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( 1  x.  ( tan `  ( Re `  A ) ) )  =  ( ( tan `  ( Re `  A
) )  x.  1 ) )
142139, 141eqtrd 2348 . . . . . 6  |-  ( ( 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 ) )
14330, 88, 88mulassd 8903 . . . . . . 7  |-  ( ( 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 ) ) ) )
14443imcjd 11737 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) ) ) )
145 imsub 11667 . . . . . . . . . . . 12  |-  ( ( 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 )
) ) ) ) ) )
1461, 41, 145sylancr 644 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) ) ) ) )
147 im1 11687 . . . . . . . . . . . . . 14  |-  ( Im
`  1 )  =  0
148147oveq1i 5910 . . . . . . . . . . . . 13  |-  ( ( Im `  1 )  -  ( Im `  ( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) )  =  ( 0  -  ( Im `  ( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) )
149 df-neg 9085 . . . . . . . . . . . . 13  |-  -u (
Im `  ( ( tan `  ( Re `  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) )  =  ( 0  -  ( Im
`  ( ( tan `  ( Re `  A
) )  x.  ( tan `  ( _i  x.  ( Im `  A ) ) ) ) ) )
150148, 149eqtr4i 2339 . . . . . . . . . . . 12  |-  ( ( Im `  1 )  -  ( Im `  ( ( tan `  (
Re `  A )
)  x.  ( tan `  ( _i  x.  (
Im `  A )
) ) ) ) )  =  -u (
Im `  ( ( tan `  ( Re `  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) )
15169, 40immul2d 11760 . . . . . . . . . . . . . 14  |-  ( ( 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 )
) ) ) ) )
152 imval 11639 . . . . . . . . . . . . . . . . 17  |-  ( ( tan `  ( _i  x.  ( Im `  A ) ) )  e.  CC  ->  (
Im `  ( tan `  ( _i  x.  (
Im `  A )
) ) )  =  ( Re `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) )
15340, 152syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  ( tan `  ( _i  x.  ( Im `  A ) ) ) )  =  ( Re `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) ) )
15472rered 11756 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Re `  (
( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) )  =  ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) )
155153, 154eqtrd 2348 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  ( tan `  ( _i  x.  ( Im `  A ) ) ) )  =  ( ( tan `  (
_i  x.  ( Im `  A ) ) )  /  _i ) )
156155oveq2d 5916 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) )
157151, 156eqtrd 2348 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
158157negeqd 9091 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
159150, 158syl5eq 2360 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
160146, 159eqtrd 2348 . . . . . . . . . 10  |-  ( ( 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 ) ) )
161160negeqd 9091 . . . . . . . . 9  |-  ( ( 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 ) ) )
16269, 72remulcld 8908 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  ( ( tan `  ( _i  x.  ( Im `  A ) ) )  /  _i ) )  e.  RR )
163162recnd 8906 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( tan `  (
Re `  A )
)  x.  ( ( tan `  ( _i  x.  ( Im `  A ) ) )  /  _i ) )  e.  CC )
164163negnegd 9193 . . . . . . . . 9  |-  ( ( 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 ) ) )
165144, 161, 1643eqtrd 2352 . . . . . . . 8  |-  ( ( 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 ) ) )
166135fveq2d 5567 . . . . . . . . 9  |-  ( ( 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 )
) ) ) ) )
16769, 72crimd 11764 . . . . . . . . 9  |-  ( ( 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 ) )
168166, 167eqtr3d 2350 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( Im `  (
( tan `  (
Re `  A )
)  +  ( tan `  ( _i  x.  (
Im `  A )
) ) ) )  =  ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) )
169165, 168oveq12d 5918 . . . . . . 7  |-  ( ( 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 ) ) )
17088sqvald 11289 . . . . . . . 8  |-  ( ( 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 ) ) )
171170oveq2d 5916 . . . . . . 7  |-  ( ( 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 ) ) ) )
172143, 169, 1713eqtr4d 2358 . . . . . 6  |-  ( ( 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 ) ) )
173142, 172oveq12d 5918 . . . . 5  |-  ( ( 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 ) ) ) )
17463, 64remuld 11750 . . . . 5  |-  ( ( 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 )
) ) ) ) ) ) )
1751a1i 10 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
1  e.  CC )
17688sqcld 11290 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( ( tan `  ( _i  x.  (
Im `  A )
) )  /  _i ) ^ 2 )  e.  CC )
17730, 175, 176subdid 9280 . . . . 5  |-  ( ( 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 ) ) ) )
178173, 174, 1773eqtr4d 2358 . . . 4  |-  ( ( 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 ) ) ) )
179102, 178breqtrrd 4086 . . 3  |-  ( ( 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 ) ) ) ) ) ) )
18062, 66, 68, 179mulgt0d 9016 . 2  |-  ( ( 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 ) ) ) ) ) ) ) )
18145fveq2d 5567 . . . . . 6  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( tan `  A
)  =  ( tan `  ( ( Re `  A )  +  ( _i  x.  ( Im
`  A ) ) ) ) )
182 tanadd 12494 . . . . . . 7  |-  ( ( ( ( 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 )
) ) ) ) ) )
1834, 36, 29, 39, 49, 182syl23anc 1189 . . . . . 6  |-  ( ( 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 )
) ) ) ) ) )
184 recval 11853 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
18543, 57, 184syl2anc 642 . . . . . . . 8  |-  ( ( 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 ) ) )
186185oveq1d 5915 . . . . . . 7  |-  ( ( 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 ) ) ) ) ) )
18764, 43, 57divrec2d 9585 . . . . . . 7  |-  ( ( 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 ) ) ) ) ) )
18843abscld 11965 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) )  e.  RR )
189188resqcld 11318 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 )  e.  RR )
190189recnd 8906 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 )  e.  CC )
19161rpne0d 10442 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
( ( abs `  (
1  -  ( ( tan `  ( Re
`  A ) )  x.  ( tan `  (
_i  x.  ( Im `  A ) ) ) ) ) ) ^
2 )  =/=  0
)
19263, 64, 190, 191div23d 9618 . . . . . . 7  |-  ( ( 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 ) ) ) ) ) )
193186, 187, 1923eqtr4d 2358 . . . . . 6  |-  ( ( 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 ) ) )
194181, 183, 1933eqtrd 2352 . . . . 5  |-  ( ( 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 ) ) )
19565, 190, 191divrec2d 9585 . . . . 5  |-  ( ( 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 ) ) ) ) ) ) )
196194, 195eqtrd 2348 . . . 4  |-  ( ( 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 ) ) ) ) ) ) )
197196fveq2d 5567 . . 3  |-  ( ( 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 ) ) ) ) ) ) ) )
19862, 65remul2d 11759 . . 3  |-  ( ( 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 ) ) ) ) ) ) ) )
199197, 198eqtrd 2348 . 2  |-  ( ( 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 ) ) ) ) ) ) ) )
200180, 199breqtrrd 4086 1  |-  ( ( A  e.  CC  /\  ( Re `  A )  e.  ( 0 (,) ( pi  /  2
) ) )  -> 
0  <  ( Re `  ( tan `  A
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633    e. wcel 1701    =/= wne 2479    C_ wss 3186   class class class wbr 4060   ` cfv 5292  (class class class)co 5900   CCcc 8780   RRcr 8781   0cc0 8782   1c1 8783   _ici 8784    + caddc 8785    x. cmul 8787   RR*cxr 8911    < clt 8912    <_ cle 8913    - cmin 9082   -ucneg 9083    / cdiv 9468   2c2 9840   ZZcz 10071   RR+crp 10401   (,)cioo 10703   ^cexp 11151   *ccj 11628   Recre 11629   Imcim 11630   abscabs 11766   cosccos 12393   tanctan 12394   picpi 12395
This theorem is referenced by:  atantan  20272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860  ax-addf 8861  ax-mulf 8862
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-iin 3945  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-of 6120  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-er 6702  df-map 6817  df-pm 6818  df-ixp 6861  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-fi 7210  df-sup 7239  df-oi 7270  df-card 7617  df-cda 7839  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-div 9469  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856  df-10 9857  df-n0 10013  df-z 10072  df-dec 10172  df-uz 10278  df-q 10364  df-rp 10402  df-xneg 10499  df-xadd 10500  df-xmul 10501  df-ioo 10707  df-ioc 10708  df-ico 10709  df-icc 10710  df-fz 10830  df-fzo 10918  df-fl 10972  df-mod 11021  df-seq 11094  df-exp 11152  df-fac 11336  df-bc 11363  df-hash 11385  df-shft 11609  df-cj 11631  df-re 11632  df-im 11633  df-sqr 11767  df-abs 11768  df-limsup 11992  df-clim 12009  df-rlim 12010  df-sum 12206  df-ef 12396  df-sin 12398  df-cos 12399  df-tan 12400  df-pi 12401  df-struct 13197  df-ndx 13198  df-slot 13199  df-base 13200  df-sets 13201  df-ress 13202  df-plusg 13268  df-mulr 13269  df-starv 13270  df-sca 13271  df-vsca 13272  df-tset 13274  df-ple 13275  df-ds 13277  df-unif 13278  df-hom 13279  df-cco 13280  df-rest 13376  df-topn 13377  df-topgen 13393  df-pt 13394  df-prds 13397  df-xrs 13452  df-0g 13453  df-gsum 13454  df-qtop 13459  df-imas 13460  df-xps 13462  df-mre 13537  df-mrc 13538  df-acs 13540  df-mnd 14416  df-submnd 14465  df-mulg 14541  df-cntz 14842  df-cmn 15140  df-xmet 16425  df-met 16426  df-bl 16427  df-mopn 16428  df-fbas 16429  df-fg 16430  df-cnfld 16433  df-top 16692  df-bases 16694  df-topon 16695  df-topsp 16696  df-cld 16812  df-ntr 16813  df-cls 16814  df-nei 16891  df-lp 16924  df-perf 16925  df-cn 17013  df-cnp 17014  df-haus 17099  df-tx 17313  df-hmeo 17502  df-fil 17593  df-fm 17685  df-flim 17686  df-flf 17687  df-xms 17937  df-ms 17938  df-tms 17939  df-cncf 18434  df-limc 19269  df-dv 19270
  Copyright terms: Public domain W3C validator