Metamath Proof Explorer

Theorem asinlem3

Description: The argument to the logarithm in df-asin has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion asinlem3 
|- ( A e. CC -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. CC -> 0 e. RR )
2 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
3 ax-icn 
 |-  _i e. CC
4 negcl 
 |-  ( A e. CC -> -u A e. CC )
5 4 adantr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> -u A e. CC )
6 mulcl 
 |-  ( ( _i e. CC /\ -u A e. CC ) -> ( _i x. -u A ) e. CC )
7 3 5 6 sylancr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( _i x. -u A ) e. CC )
8 ax-1cn 
 |-  1 e. CC
9 5 sqcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( -u A ^ 2 ) e. CC )
10 subcl 
 |-  ( ( 1 e. CC /\ ( -u A ^ 2 ) e. CC ) -> ( 1 - ( -u A ^ 2 ) ) e. CC )
11 8 9 10 sylancr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 - ( -u A ^ 2 ) ) e. CC )
12 11 sqrtcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) e. CC )
13 7 12 addcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) e. CC )
14 asinlem 
 |-  ( -u A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 )
15 5 14 syl 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 )
16 13 15 absrpcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) e. RR+ )
17 2z 
 |-  2 e. ZZ
18 rpexpcl 
 |-  ( ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) e. RR+ )
19 16 17 18 sylancl 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) e. RR+ )
20 19 rprecred 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) e. RR )
21 13 cjcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) e. CC )
22 21 recld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) e. RR )
23 19 rpreccld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) e. RR+ )
24 23 rpge0d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 0 <_ ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) )
25 imneg 
 |-  ( A e. CC -> ( Im ` -u A ) = -u ( Im ` A ) )
26 25 adantr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Im ` -u A ) = -u ( Im ` A ) )
27 2 le0neg2d 
 |-  ( A e. CC -> ( 0 <_ ( Im ` A ) <-> -u ( Im ` A ) <_ 0 ) )
28 27 biimpa 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> -u ( Im ` A ) <_ 0 )
29 26 28 eqbrtrd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Im ` -u A ) <_ 0 )
30 asinlem3a 
 |-  ( ( -u A e. CC /\ ( Im ` -u A ) <_ 0 ) -> 0 <_ ( Re ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
31 5 29 30 syl2anc 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 0 <_ ( Re ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
32 13 recjd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) = ( Re ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
33 31 32 breqtrrd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 0 <_ ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
34 20 22 24 33 mulge0d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 0 <_ ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) ) )
35 recval 
 |-  ( ( ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 ) -> ( 1 / ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = ( ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) )
36 13 15 35 syl2anc 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 / ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = ( ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) )
37 asinlem2 
 |-  ( A e. CC -> ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = 1 )
38 37 adantr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = 1 )
39 38 eqcomd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 1 = ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
40 1cnd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 1 e. CC )
41 simpl 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> A e. CC )
42 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
43 3 41 42 sylancr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( _i x. A ) e. CC )
44 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
45 44 adantr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( A ^ 2 ) e. CC )
46 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
47 8 45 46 sylancr 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 - ( A ^ 2 ) ) e. CC )
48 47 sqrtcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
49 43 48 addcld 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC )
50 40 49 13 15 divmul3d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( 1 / ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) <-> 1 = ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
51 39 50 mpbird 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( 1 / ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
52 19 rpcnd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) e. CC )
53 19 rpne0d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) =/= 0 )
54 21 52 53 divrec2d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) = ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
55 36 51 54 3eqtr3d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) = ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
56 55 fveq2d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( Re ` ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) ) )
57 20 21 remul2d 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Re ` ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) ) = ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) ) )
58 56 57 eqtrd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( ( 1 / ( ( abs ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ^ 2 ) ) x. ( Re ` ( * ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) ) )
59 34 58 breqtrrd 
 |-  ( ( A e. CC /\ 0 <_ ( Im ` A ) ) -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
60 asinlem3a 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
61 1 2 59 60 lecasei 
 |-  ( A e. CC -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )