Metamath Proof Explorer

Theorem isosctrlem1

Description: Lemma for isosctr . (Contributed by Saveliy Skresanov, 30-Dec-2016)

Ref Expression
Assertion isosctrlem1 
|- ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) =/= _pi )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
3 1 2 mpan 
 |-  ( A e. CC -> ( 1 - A ) e. CC )
4 3 adantr 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( 1 - A ) e. CC )
5 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
6 5 notbid 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( -. ( 1 - A ) = 0 <-> -. 1 = A ) )
7 1 6 mpan 
 |-  ( A e. CC -> ( -. ( 1 - A ) = 0 <-> -. 1 = A ) )
8 7 biimpar 
 |-  ( ( A e. CC /\ -. 1 = A ) -> -. ( 1 - A ) = 0 )
9 8 neqned 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( 1 - A ) =/= 0 )
10 4 9 logcld 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( log ` ( 1 - A ) ) e. CC )
11 10 imcld 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. RR )
12 11 3adant2 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. RR )
13 3 3ad2ant1 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( 1 - A ) e. CC )
14 9 3adant2 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( 1 - A ) =/= 0 )
15 releabs 
 |-  ( A e. CC -> ( Re ` A ) <_ ( abs ` A ) )
16 15 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( Re ` A ) <_ ( abs ` A ) )
17 breq2 
 |-  ( ( abs ` A ) = 1 -> ( ( Re ` A ) <_ ( abs ` A ) <-> ( Re ` A ) <_ 1 ) )
18 17 adantl 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( ( Re ` A ) <_ ( abs ` A ) <-> ( Re ` A ) <_ 1 ) )
19 16 18 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( Re ` A ) <_ 1 )
20 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
21 20 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
22 21 subidd 
 |-  ( A e. CC -> ( ( Re ` A ) - ( Re ` A ) ) = 0 )
23 22 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) = 0 )
24 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> A e. CC )
25 24 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> ( Re ` A ) e. RR )
26 1red 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> 1 e. RR )
27 simpr 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> ( Re ` A ) <_ 1 )
28 25 26 25 27 lesub1dd 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) <_ ( 1 - ( Re ` A ) ) )
29 23 28 eqbrtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) <_ 1 ) -> 0 <_ ( 1 - ( Re ` A ) ) )
30 19 29 syldan 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> 0 <_ ( 1 - ( Re ` A ) ) )
31 resub 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( Re ` ( 1 - A ) ) = ( ( Re ` 1 ) - ( Re ` A ) ) )
32 re1 
 |-  ( Re ` 1 ) = 1
33 32 oveq1i 
 |-  ( ( Re ` 1 ) - ( Re ` A ) ) = ( 1 - ( Re ` A ) )
34 31 33 eqtrdi 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( Re ` ( 1 - A ) ) = ( 1 - ( Re ` A ) ) )
35 1 34 mpan 
 |-  ( A e. CC -> ( Re ` ( 1 - A ) ) = ( 1 - ( Re ` A ) ) )
36 35 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( Re ` ( 1 - A ) ) = ( 1 - ( Re ` A ) ) )
37 30 36 breqtrrd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> 0 <_ ( Re ` ( 1 - A ) ) )
38 37 3adant3 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> 0 <_ ( Re ` ( 1 - A ) ) )
39 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
40 halfpire 
 |-  ( _pi / 2 ) e. RR
41 40 rexri 
 |-  ( _pi / 2 ) e. RR*
42 argrege0 
 |-  ( ( ( 1 - A ) e. CC /\ ( 1 - A ) =/= 0 /\ 0 <_ ( Re ` ( 1 - A ) ) ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
43 iccleub 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* /\ ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) )
44 39 41 42 43 mp3an12i 
 |-  ( ( ( 1 - A ) e. CC /\ ( 1 - A ) =/= 0 /\ 0 <_ ( Re ` ( 1 - A ) ) ) -> ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) )
45 13 14 38 44 syl3anc 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) )
46 pirp 
 |-  _pi e. RR+
47 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
48 46 47 ax-mp 
 |-  ( _pi / 2 ) < _pi
49 45 48 jctir 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) )
50 pire 
 |-  _pi e. RR
51 50 a1i 
 |-  ( ( A e. CC /\ -. 1 = A ) -> _pi e. RR )
52 51 rehalfcld 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( _pi / 2 ) e. RR )
53 lelttr 
 |-  ( ( ( Im ` ( log ` ( 1 - A ) ) ) e. RR /\ ( _pi / 2 ) e. RR /\ _pi e. RR ) -> ( ( ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) -> ( Im ` ( log ` ( 1 - A ) ) ) < _pi ) )
54 11 52 51 53 syl3anc 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( ( ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) -> ( Im ` ( log ` ( 1 - A ) ) ) < _pi ) )
55 54 3adant2 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( ( ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) /\ ( _pi / 2 ) < _pi ) -> ( Im ` ( log ` ( 1 - A ) ) ) < _pi ) )
56 49 55 mpd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) < _pi )
57 12 56 ltned 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) =/= _pi )