Metamath Proof Explorer

Theorem efif1olem3

Description: Lemma for efif1o . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses efif1o.1 
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
efif1o.2 
|- C = ( `' abs " { 1 } )
Assertion efif1olem3 
|- ( ( ph /\ x e. C ) -> ( Im ` ( sqrt ` x ) ) e. ( -u 1 [,] 1 ) )

Proof

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