| 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 ) ) ) ) ) ) |