Metamath Proof Explorer

Theorem isosctrlem1ALT

Description: Lemma for isosctr . This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . As it is verified by the Metamath program, isosctrlem1ALT verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isosctrlem1ALT 
|- ( ( 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 1 a1i 
 |-  ( A e. CC -> 1 e. CC )
3 id 
 |-  ( A e. CC -> A e. CC )
4 2 3 subcld 
 |-  ( A e. CC -> ( 1 - A ) e. CC )
5 4 adantr 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( 1 - A ) e. CC )
6 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
7 6 biimpd 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 -> 1 = A ) )
8 7 idiALT 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 -> 1 = A ) )
9 1 3 8 sylancr 
 |-  ( A e. CC -> ( ( 1 - A ) = 0 -> 1 = A ) )
10 9 con3d 
 |-  ( A e. CC -> ( -. 1 = A -> -. ( 1 - A ) = 0 ) )
11 df-ne 
 |-  ( ( 1 - A ) =/= 0 <-> -. ( 1 - A ) = 0 )
12 11 biimpri 
 |-  ( -. ( 1 - A ) = 0 -> ( 1 - A ) =/= 0 )
13 10 12 syl6 
 |-  ( A e. CC -> ( -. 1 = A -> ( 1 - A ) =/= 0 ) )
14 13 imp 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( 1 - A ) =/= 0 )
15 5 14 logcld 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( log ` ( 1 - A ) ) e. CC )
16 15 imcld 
 |-  ( ( A e. CC /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. RR )
17 16 3adant2 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. RR )
18 pire 
 |-  _pi e. RR
19 2re 
 |-  2 e. RR
20 2ne0 
 |-  2 =/= 0
21 18 19 20 redivcli 
 |-  ( _pi / 2 ) e. RR
22 21 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( _pi / 2 ) e. RR )
23 18 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> _pi e. RR )
24 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
25 21 rexri 
 |-  ( _pi / 2 ) e. RR*
26 3 recld 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
27 26 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
28 27 subidd 
 |-  ( A e. CC -> ( ( Re ` A ) - ( Re ` A ) ) = 0 )
29 28 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) = 0 )
30 1re 
 |-  1 e. RR
31 30 a1i 
 |-  ( 1 e. CC -> 1 e. RR )
32 1 31 ax-mp 
 |-  1 e. RR
33 3 releabsd 
 |-  ( A e. CC -> ( Re ` A ) <_ ( abs ` A ) )
34 33 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( Re ` A ) <_ ( abs ` A ) )
35 id 
 |-  ( ( abs ` A ) = 1 -> ( abs ` A ) = 1 )
36 35 adantl 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( abs ` A ) = 1 )
37 34 36 breqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( Re ` A ) <_ 1 )
38 lesub1 
 |-  ( ( ( Re ` A ) e. RR /\ 1 e. RR /\ ( Re ` A ) e. RR ) -> ( ( Re ` A ) <_ 1 <-> ( ( Re ` A ) - ( Re ` A ) ) <_ ( 1 - ( Re ` A ) ) ) )
39 38 3impcombi 
 |-  ( ( 1 e. RR /\ ( Re ` A ) e. RR /\ ( Re ` A ) <_ 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) <_ ( 1 - ( Re ` A ) ) )
40 39 idiALT 
 |-  ( ( 1 e. RR /\ ( Re ` A ) e. RR /\ ( Re ` A ) <_ 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) <_ ( 1 - ( Re ` A ) ) )
41 32 26 37 40 mp3an2ani 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( ( Re ` A ) - ( Re ` A ) ) <_ ( 1 - ( Re ` A ) ) )
42 29 41 eqbrtrrd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> 0 <_ ( 1 - ( Re ` A ) ) )
43 32 a1i 
 |-  ( T. -> 1 e. RR )
44 43 rered 
 |-  ( T. -> ( Re ` 1 ) = 1 )
45 44 mptru 
 |-  ( Re ` 1 ) = 1
46 oveq1 
 |-  ( ( Re ` 1 ) = 1 -> ( ( Re ` 1 ) - ( Re ` A ) ) = ( 1 - ( Re ` A ) ) )
47 46 eqcomd 
 |-  ( ( Re ` 1 ) = 1 -> ( 1 - ( Re ` A ) ) = ( ( Re ` 1 ) - ( Re ` A ) ) )
48 45 47 ax-mp 
 |-  ( 1 - ( Re ` A ) ) = ( ( Re ` 1 ) - ( Re ` A ) )
49 resub 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( Re ` ( 1 - A ) ) = ( ( Re ` 1 ) - ( Re ` A ) ) )
50 49 eqcomd 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( Re ` 1 ) - ( Re ` A ) ) = ( Re ` ( 1 - A ) ) )
51 50 idiALT 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( Re ` 1 ) - ( Re ` A ) ) = ( Re ` ( 1 - A ) ) )
52 1 3 51 sylancr 
 |-  ( A e. CC -> ( ( Re ` 1 ) - ( Re ` A ) ) = ( Re ` ( 1 - A ) ) )
53 48 52 syl5eq 
 |-  ( A e. CC -> ( 1 - ( Re ` A ) ) = ( Re ` ( 1 - A ) ) )
54 53 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> ( 1 - ( Re ` A ) ) = ( Re ` ( 1 - A ) ) )
55 42 54 breqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 ) -> 0 <_ ( Re ` ( 1 - A ) ) )
56 argrege0 
 |-  ( ( ( 1 - A ) e. CC /\ ( 1 - A ) =/= 0 /\ 0 <_ ( Re ` ( 1 - A ) ) ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
57 56 3coml 
 |-  ( ( ( 1 - A ) =/= 0 /\ 0 <_ ( Re ` ( 1 - A ) ) /\ ( 1 - A ) e. CC ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
58 57 3com13 
 |-  ( ( ( 1 - A ) e. CC /\ 0 <_ ( Re ` ( 1 - A ) ) /\ ( 1 - A ) =/= 0 ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
59 4 55 14 58 eel12131 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
60 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 ) )
61 24 25 59 60 mp3an12i 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) <_ ( _pi / 2 ) )
62 pipos 
 |-  0 < _pi
63 18 62 elrpii 
 |-  _pi e. RR+
64 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
65 63 64 ax-mp 
 |-  ( _pi / 2 ) < _pi
66 65 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( _pi / 2 ) < _pi )
67 17 22 23 61 66 lelttrd 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) < _pi )
68 17 67 ltned 
 |-  ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) =/= _pi )