| Step |
Hyp |
Ref |
Expression |
| 1 |
|
efif1o.1 |
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) ) |
| 2 |
|
efif1o.2 |
|- C = ( `' abs " { 1 } ) |
| 3 |
|
simpr |
|- ( ( ph /\ x e. C ) -> x e. C ) |
| 4 |
3 2
|
eleqtrdi |
|- ( ( ph /\ x e. C ) -> x e. ( `' abs " { 1 } ) ) |
| 5 |
|
absf |
|- abs : CC --> RR |
| 6 |
|
ffn |
|- ( abs : CC --> RR -> abs Fn CC ) |
| 7 |
|
fniniseg |
|- ( abs Fn CC -> ( x e. ( `' abs " { 1 } ) <-> ( x e. CC /\ ( abs ` x ) = 1 ) ) ) |
| 8 |
5 6 7
|
mp2b |
|- ( x e. ( `' abs " { 1 } ) <-> ( x e. CC /\ ( abs ` x ) = 1 ) ) |
| 9 |
4 8
|
sylib |
|- ( ( ph /\ x e. C ) -> ( x e. CC /\ ( abs ` x ) = 1 ) ) |
| 10 |
9
|
simpld |
|- ( ( ph /\ x e. C ) -> x e. CC ) |
| 11 |
10
|
sqrtcld |
|- ( ( ph /\ x e. C ) -> ( sqrt ` x ) e. CC ) |
| 12 |
11
|
imcld |
|- ( ( ph /\ x e. C ) -> ( Im ` ( sqrt ` x ) ) e. RR ) |
| 13 |
|
absimle |
|- ( ( sqrt ` x ) e. CC -> ( abs ` ( Im ` ( sqrt ` x ) ) ) <_ ( abs ` ( sqrt ` x ) ) ) |
| 14 |
11 13
|
syl |
|- ( ( ph /\ x e. C ) -> ( abs ` ( Im ` ( sqrt ` x ) ) ) <_ ( abs ` ( sqrt ` x ) ) ) |
| 15 |
10
|
sqsqrtd |
|- ( ( ph /\ x e. C ) -> ( ( sqrt ` x ) ^ 2 ) = x ) |
| 16 |
15
|
fveq2d |
|- ( ( ph /\ x e. C ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( abs ` x ) ) |
| 17 |
|
2nn0 |
|- 2 e. NN0 |
| 18 |
|
absexp |
|- ( ( ( sqrt ` x ) e. CC /\ 2 e. NN0 ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( ( abs ` ( sqrt ` x ) ) ^ 2 ) ) |
| 19 |
11 17 18
|
sylancl |
|- ( ( ph /\ x e. C ) -> ( abs ` ( ( sqrt ` x ) ^ 2 ) ) = ( ( abs ` ( sqrt ` x ) ) ^ 2 ) ) |
| 20 |
9
|
simprd |
|- ( ( ph /\ x e. C ) -> ( abs ` x ) = 1 ) |
| 21 |
16 19 20
|
3eqtr3d |
|- ( ( ph /\ x e. C ) -> ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = 1 ) |
| 22 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
| 23 |
21 22
|
eqtr4di |
|- ( ( ph /\ x e. C ) -> ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = ( 1 ^ 2 ) ) |
| 24 |
11
|
abscld |
|- ( ( ph /\ x e. C ) -> ( abs ` ( sqrt ` x ) ) e. RR ) |
| 25 |
11
|
absge0d |
|- ( ( ph /\ x e. C ) -> 0 <_ ( abs ` ( sqrt ` x ) ) ) |
| 26 |
|
1re |
|- 1 e. RR |
| 27 |
|
0le1 |
|- 0 <_ 1 |
| 28 |
|
sq11 |
|- ( ( ( ( abs ` ( sqrt ` x ) ) e. RR /\ 0 <_ ( abs ` ( sqrt ` x ) ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` ( sqrt ` x ) ) = 1 ) ) |
| 29 |
26 27 28
|
mpanr12 |
|- ( ( ( abs ` ( sqrt ` x ) ) e. RR /\ 0 <_ ( abs ` ( sqrt ` x ) ) ) -> ( ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` ( sqrt ` x ) ) = 1 ) ) |
| 30 |
24 25 29
|
syl2anc |
|- ( ( ph /\ x e. C ) -> ( ( ( abs ` ( sqrt ` x ) ) ^ 2 ) = ( 1 ^ 2 ) <-> ( abs ` ( sqrt ` x ) ) = 1 ) ) |
| 31 |
23 30
|
mpbid |
|- ( ( ph /\ x e. C ) -> ( abs ` ( sqrt ` x ) ) = 1 ) |
| 32 |
14 31
|
breqtrd |
|- ( ( ph /\ x e. C ) -> ( abs ` ( Im ` ( sqrt ` x ) ) ) <_ 1 ) |
| 33 |
|
absle |
|- ( ( ( Im ` ( sqrt ` x ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( Im ` ( sqrt ` x ) ) ) <_ 1 <-> ( -u 1 <_ ( Im ` ( sqrt ` x ) ) /\ ( Im ` ( sqrt ` x ) ) <_ 1 ) ) ) |
| 34 |
12 26 33
|
sylancl |
|- ( ( ph /\ x e. C ) -> ( ( abs ` ( Im ` ( sqrt ` x ) ) ) <_ 1 <-> ( -u 1 <_ ( Im ` ( sqrt ` x ) ) /\ ( Im ` ( sqrt ` x ) ) <_ 1 ) ) ) |
| 35 |
32 34
|
mpbid |
|- ( ( ph /\ x e. C ) -> ( -u 1 <_ ( Im ` ( sqrt ` x ) ) /\ ( Im ` ( sqrt ` x ) ) <_ 1 ) ) |
| 36 |
35
|
simpld |
|- ( ( ph /\ x e. C ) -> -u 1 <_ ( Im ` ( sqrt ` x ) ) ) |
| 37 |
35
|
simprd |
|- ( ( ph /\ x e. C ) -> ( Im ` ( sqrt ` x ) ) <_ 1 ) |
| 38 |
|
neg1rr |
|- -u 1 e. RR |
| 39 |
38 26
|
elicc2i |
|- ( ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) <-> ( ( Im ` ( sqrt ` x ) ) e. RR /\ -u 1 <_ ( Im ` ( sqrt ` x ) ) /\ ( Im ` ( sqrt ` x ) ) <_ 1 ) ) |
| 40 |
12 36 37 39
|
syl3anbrc |
|- ( ( ph /\ x e. C ) -> ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) ) |