Metamath Proof Explorer

Theorem asinlem3a

Description: Lemma for asinlem3 . (Contributed by Mario Carneiro, 1-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
2 1 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Im ` A ) e. RR )
3 2 renegcld 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> -u ( Im ` A ) e. RR )
4 ax-1cn 
 |-  1 e. CC
5 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
6 5 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( A ^ 2 ) e. CC )
7 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
8 4 6 7 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( 1 - ( A ^ 2 ) ) e. CC )
9 8 sqrtcld 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
10 9 recld 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR )
11 1 le0neg1d 
 |-  ( A e. CC -> ( ( Im ` A ) <_ 0 <-> 0 <_ -u ( Im ` A ) ) )
12 11 biimpa 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ -u ( Im ` A ) )
13 8 sqrtrege0d 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
14 3 10 12 13 addge0d 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ ( -u ( Im ` A ) + ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
15 ax-icn 
 |-  _i e. CC
16 simpl 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> A e. CC )
17 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
18 15 16 17 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( _i x. A ) e. CC )
19 18 9 readdd 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( ( Re ` ( _i x. A ) ) + ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
20 negicn 
 |-  -u _i e. CC
21 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
22 20 16 21 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( -u _i x. A ) e. CC )
23 22 renegd 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` -u ( -u _i x. A ) ) = -u ( Re ` ( -u _i x. A ) ) )
24 15 negnegi 
 |-  -u -u _i = _i
25 24 oveq1i 
 |-  ( -u -u _i x. A ) = ( _i x. A )
26 mulneg1 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u -u _i x. A ) = -u ( -u _i x. A ) )
27 20 16 26 sylancr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( -u -u _i x. A ) = -u ( -u _i x. A ) )
28 25 27 eqtr3id 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( _i x. A ) = -u ( -u _i x. A ) )
29 28 fveq2d 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` ( _i x. A ) ) = ( Re ` -u ( -u _i x. A ) ) )
30 imre 
 |-  ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
31 30 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
32 31 negeqd 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> -u ( Im ` A ) = -u ( Re ` ( -u _i x. A ) ) )
33 23 29 32 3eqtr4d 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` ( _i x. A ) ) = -u ( Im ` A ) )
34 33 oveq1d 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( ( Re ` ( _i x. A ) ) + ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( -u ( Im ` A ) + ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
35 19 34 eqtrd 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( -u ( Im ` A ) + ( Re ` ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
36 14 35 breqtrrd 
 |-  ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )