Metamath Proof Explorer

Theorem efopnlem1

Description: Lemma for efopn . (Contributed by Mario Carneiro, 23-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion efopnlem1 
|- ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) < _pi )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> A e. ( 0 ( ball ` ( abs o. - ) ) R ) )
2 rpxr 
 |-  ( R e. RR+ -> R e. RR* )
3 2 ad2antrr 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> R e. RR* )
4 eqid 
 |-  ( abs o. - ) = ( abs o. - )
5 4 cnbl0 
 |-  ( R e. RR* -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` ( abs o. - ) ) R ) )
6 3 5 syl 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( `' abs " ( 0 [,) R ) ) = ( 0 ( ball ` ( abs o. - ) ) R ) )
7 1 6 eleqtrrd 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> A e. ( `' abs " ( 0 [,) R ) ) )
8 absf 
 |-  abs : CC --> RR
9 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
10 elpreima 
 |-  ( abs Fn CC -> ( A e. ( `' abs " ( 0 [,) R ) ) <-> ( A e. CC /\ ( abs ` A ) e. ( 0 [,) R ) ) ) )
11 8 9 10 mp2b 
 |-  ( A e. ( `' abs " ( 0 [,) R ) ) <-> ( A e. CC /\ ( abs ` A ) e. ( 0 [,) R ) ) )
12 11 simplbi 
 |-  ( A e. ( `' abs " ( 0 [,) R ) ) -> A e. CC )
13 7 12 syl 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> A e. CC )
14 13 imcld 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` A ) e. RR )
15 14 recnd 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( Im ` A ) e. CC )
16 15 abscld 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) e. RR )
17 rpre 
 |-  ( R e. RR+ -> R e. RR )
18 17 ad2antrr 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> R e. RR )
19 pire 
 |-  _pi e. RR
20 19 a1i 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> _pi e. RR )
21 13 abscld 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` A ) e. RR )
22 absimle 
 |-  ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )
23 13 22 syl 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )
24 11 simprbi 
 |-  ( A e. ( `' abs " ( 0 [,) R ) ) -> ( abs ` A ) e. ( 0 [,) R ) )
25 7 24 syl 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` A ) e. ( 0 [,) R ) )
26 0re 
 |-  0 e. RR
27 elico2 
 |-  ( ( 0 e. RR /\ R e. RR* ) -> ( ( abs ` A ) e. ( 0 [,) R ) <-> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) /\ ( abs ` A ) < R ) ) )
28 26 3 27 sylancr 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( ( abs ` A ) e. ( 0 [,) R ) <-> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) /\ ( abs ` A ) < R ) ) )
29 25 28 mpbid 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) /\ ( abs ` A ) < R ) )
30 29 simp3d 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` A ) < R )
31 16 21 18 23 30 lelttrd 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) < R )
32 simplr 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> R < _pi )
33 16 18 20 31 32 lttrd 
 |-  ( ( ( R e. RR+ /\ R < _pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) < _pi )