Metamath Proof Explorer

Theorem efopnlem2

Description: Lemma for efopn . (Contributed by Mario Carneiro, 2-May-2015)

Ref Expression
Hypothesis efopn.j 
|- J = ( TopOpen ` CCfld )
Assertion efopnlem2 
|- ( ( R e. RR+ /\ R < _pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J )

Proof

Step Hyp Ref Expression
1 efopn.j 
 |-  J = ( TopOpen ` CCfld )
2 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
3 f1orn 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> ( log Fn ( CC \ { 0 } ) /\ Fun `' log ) )
4 3 simprbi 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> Fun `' log )
5 funcnvres 
 |-  ( Fun `' log -> `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) )
6 2 4 5 mp2b 
 |-  `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
7 df-log 
 |-  log = `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
8 7 cnveqi 
 |-  `' log = `' `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
9 relres 
 |-  Rel ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
10 dfrel2 
 |-  ( Rel ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) <-> `' `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) = ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) )
11 9 10 mpbi 
 |-  `' `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) = ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
12 8 11 eqtri 
 |-  `' log = ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
13 12 reseq1i 
 |-  ( `' log |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
14 imassrn 
 |-  ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ran log
15 logrn 
 |-  ran log = ( `' Im " ( -u _pi (,] _pi ) )
16 14 15 sseqtri 
 |-  ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ( `' Im " ( -u _pi (,] _pi ) )
17 resabs1 
 |-  ( ( log " ( CC \ ( -oo (,] 0 ) ) ) C_ ( `' Im " ( -u _pi (,] _pi ) ) -> ( ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) )
18 16 17 ax-mp 
 |-  ( ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
19 6 13 18 3eqtri 
 |-  `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) )
20 19 imaeq1i 
 |-  ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) )
21 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
22 0cnd 
 |-  ( ( R e. RR+ /\ R < _pi ) -> 0 e. CC )
23 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
24 23 adantr 
 |-  ( ( R e. RR+ /\ R < _pi ) -> R e. RR* )
25 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ CC )
26 21 22 24 25 mp3an2i 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ CC )
27 26 sselda 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> x e. CC )
28 27 imcld 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) e. RR )
29 efopnlem1 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` x ) ) < _pi )
30 pire 
 |-  _pi e. RR
31 abslt 
 |-  ( ( ( Im ` x ) e. RR /\ _pi e. RR ) -> ( ( abs ` ( Im ` x ) ) < _pi <-> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) ) )
32 28 30 31 sylancl 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( ( abs ` ( Im ` x ) ) < _pi <-> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) ) )
33 29 32 mpbid 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
34 33 simpld 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> -u _pi < ( Im ` x ) )
35 33 simprd 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) < _pi )
36 30 renegcli 
 |-  -u _pi e. RR
37 36 rexri 
 |-  -u _pi e. RR*
38 30 rexri 
 |-  _pi e. RR*
39 elioo2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* ) -> ( ( Im ` x ) e. ( -u _pi (,) _pi ) <-> ( ( Im ` x ) e. RR /\ -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) ) )
40 37 38 39 mp2an 
 |-  ( ( Im ` x ) e. ( -u _pi (,) _pi ) <-> ( ( Im ` x ) e. RR /\ -u _pi < ( Im ` x ) /\ ( Im ` x ) < _pi ) )
41 28 34 35 40 syl3anbrc 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` x ) e. ( -u _pi (,) _pi ) )
42 imf 
 |-  Im : CC --> RR
43 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
44 elpreima 
 |-  ( Im Fn CC -> ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) ) )
45 42 43 44 mp2b 
 |-  ( x e. ( `' Im " ( -u _pi (,) _pi ) ) <-> ( x e. CC /\ ( Im ` x ) e. ( -u _pi (,) _pi ) ) )
46 27 41 45 sylanbrc 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ x e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> x e. ( `' Im " ( -u _pi (,) _pi ) ) )
47 46 ex 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( x e. ( 0 ( ball ` ( abs o. - ) ) R ) -> x e. ( `' Im " ( -u _pi (,) _pi ) ) ) )
48 47 ssrdv 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( `' Im " ( -u _pi (,) _pi ) ) )
49 df-ima 
 |-  ( log " ( CC \ ( -oo (,] 0 ) ) ) = ran ( log |` ( CC \ ( -oo (,] 0 ) ) )
50 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
51 50 logf1o2 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) )
52 f1ofo 
 |-  ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -1-1-onto-> ( `' Im " ( -u _pi (,) _pi ) ) -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -onto-> ( `' Im " ( -u _pi (,) _pi ) ) )
53 forn 
 |-  ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) : ( CC \ ( -oo (,] 0 ) ) -onto-> ( `' Im " ( -u _pi (,) _pi ) ) -> ran ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u _pi (,) _pi ) ) )
54 51 52 53 mp2b 
 |-  ran ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u _pi (,) _pi ) )
55 49 54 eqtri 
 |-  ( log " ( CC \ ( -oo (,] 0 ) ) ) = ( `' Im " ( -u _pi (,) _pi ) )
56 48 55 sseqtrrdi 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( log " ( CC \ ( -oo (,] 0 ) ) ) )
57 resima2 
 |-  ( ( 0 ( ball ` ( abs o. - ) ) R ) C_ ( log " ( CC \ ( -oo (,] 0 ) ) ) -> ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
58 56 57 syl 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( ( exp |` ( log " ( CC \ ( -oo (,] 0 ) ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
59 20 58 syl5eq 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) = ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) )
60 50 logcn 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
61 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
62 ssid 
 |-  CC C_ CC
63 eqid 
 |-  ( J |`t ( CC \ ( -oo (,] 0 ) ) ) = ( J |`t ( CC \ ( -oo (,] 0 ) ) )
64 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
65 64 toponrestid 
 |-  J = ( J |`t CC )
66 1 63 65 cncfcn 
 |-  ( ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ CC C_ CC ) -> ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) Cn J ) )
67 61 62 66 mp2an 
 |-  ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) Cn J )
68 60 67 eleqtri 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) Cn J )
69 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
70 69 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ R e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) R ) e. J )
71 21 22 24 70 mp3an2i 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( 0 ( ball ` ( abs o. - ) ) R ) e. J )
72 cnima 
 |-  ( ( ( log |` ( CC \ ( -oo (,] 0 ) ) ) e. ( ( J |`t ( CC \ ( -oo (,] 0 ) ) ) Cn J ) /\ ( 0 ( ball ` ( abs o. - ) ) R ) e. J ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J |`t ( CC \ ( -oo (,] 0 ) ) ) )
73 68 71 72 sylancr 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( `' ( log |` ( CC \ ( -oo (,] 0 ) ) ) " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J |`t ( CC \ ( -oo (,] 0 ) ) ) )
74 59 73 eqeltrrd 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J |`t ( CC \ ( -oo (,] 0 ) ) ) )
75 1 cnfldtop 
 |-  J e. Top
76 50 logdmopn 
 |-  ( CC \ ( -oo (,] 0 ) ) e. ( TopOpen ` CCfld )
77 76 1 eleqtrri 
 |-  ( CC \ ( -oo (,] 0 ) ) e. J
78 restopn2 
 |-  ( ( J e. Top /\ ( CC \ ( -oo (,] 0 ) ) e. J ) -> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J |`t ( CC \ ( -oo (,] 0 ) ) ) <-> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) ) )
79 75 77 78 mp2an 
 |-  ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. ( J |`t ( CC \ ( -oo (,] 0 ) ) ) <-> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) )
80 74 79 sylib 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J /\ ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) C_ ( CC \ ( -oo (,] 0 ) ) ) )
81 80 simpld 
 |-  ( ( R e. RR+ /\ R < _pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J )