Metamath Proof Explorer

Theorem ang180lem4

Description: Lemma for ang180 . Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion ang180lem4 
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) + ( 1 F A ) ) e. { -u _pi , _pi } )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 1cnd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> 1 e. CC )
3 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. CC )
4 2 3 subcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) e. CC )
5 simp3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 1 )
6 5 necomd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> 1 =/= A )
7 2 3 6 subne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) =/= 0 )
8 ax-1ne0 
 |-  1 =/= 0
9 8 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> 1 =/= 0 )
10 1 4 7 2 9 angvald 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( 1 - A ) F 1 ) = ( Im ` ( log ` ( 1 / ( 1 - A ) ) ) ) )
11 simp2 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 0 )
12 3 2 subcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) e. CC )
13 3 2 5 subne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) =/= 0 )
14 1 3 11 12 13 angvald 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A F ( A - 1 ) ) = ( Im ` ( log ` ( ( A - 1 ) / A ) ) ) )
15 10 14 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) = ( ( Im ` ( log ` ( 1 / ( 1 - A ) ) ) ) + ( Im ` ( log ` ( ( A - 1 ) / A ) ) ) ) )
16 2 4 7 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) e. CC )
17 4 7 recne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) =/= 0 )
18 16 17 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( 1 / ( 1 - A ) ) ) e. CC )
19 12 3 11 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) e. CC )
20 12 3 13 11 divne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) =/= 0 )
21 19 20 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( ( A - 1 ) / A ) ) e. CC )
22 18 21 imaddd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( Im ` ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) ) = ( ( Im ` ( log ` ( 1 / ( 1 - A ) ) ) ) + ( Im ` ( log ` ( ( A - 1 ) / A ) ) ) ) )
23 15 22 eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) = ( Im ` ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) ) )
24 1 2 9 3 11 angvald 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 F A ) = ( Im ` ( log ` ( A / 1 ) ) ) )
25 3 div1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A / 1 ) = A )
26 25 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( A / 1 ) ) = ( log ` A ) )
27 26 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( Im ` ( log ` ( A / 1 ) ) ) = ( Im ` ( log ` A ) ) )
28 24 27 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 F A ) = ( Im ` ( log ` A ) ) )
29 23 28 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) + ( 1 F A ) ) = ( ( Im ` ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) ) + ( Im ` ( log ` A ) ) ) )
30 18 21 addcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) e. CC )
31 3 11 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) e. CC )
32 30 31 imaddd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = ( ( Im ` ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) ) + ( Im ` ( log ` A ) ) ) )
33 29 32 eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) + ( 1 F A ) ) = ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) )
34 eqid 
 |-  ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) )
35 eqid 
 |-  ( ( ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) = ( ( ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) )
36 1 34 35 ang180lem3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. { -u ( _i x. _pi ) , ( _i x. _pi ) } )
37 fveq2 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = -u ( _i x. _pi ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = ( Im ` -u ( _i x. _pi ) ) )
38 ax-icn 
 |-  _i e. CC
39 picn 
 |-  _pi e. CC
40 38 39 mulcli 
 |-  ( _i x. _pi ) e. CC
41 40 imnegi 
 |-  ( Im ` -u ( _i x. _pi ) ) = -u ( Im ` ( _i x. _pi ) )
42 40 addlidi 
 |-  ( 0 + ( _i x. _pi ) ) = ( _i x. _pi )
43 42 fveq2i 
 |-  ( Im ` ( 0 + ( _i x. _pi ) ) ) = ( Im ` ( _i x. _pi ) )
44 0re 
 |-  0 e. RR
45 pire 
 |-  _pi e. RR
46 44 45 crimi 
 |-  ( Im ` ( 0 + ( _i x. _pi ) ) ) = _pi
47 43 46 eqtr3i 
 |-  ( Im ` ( _i x. _pi ) ) = _pi
48 47 negeqi 
 |-  -u ( Im ` ( _i x. _pi ) ) = -u _pi
49 41 48 eqtri 
 |-  ( Im ` -u ( _i x. _pi ) ) = -u _pi
50 37 49 eqtrdi 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = -u ( _i x. _pi ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = -u _pi )
51 fveq2 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = ( _i x. _pi ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = ( Im ` ( _i x. _pi ) ) )
52 51 47 eqtrdi 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = ( _i x. _pi ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = _pi )
53 50 52 orim12i 
 |-  ( ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = -u ( _i x. _pi ) \/ ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = ( _i x. _pi ) ) -> ( ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = -u _pi \/ ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = _pi ) )
54 ovex 
 |-  ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. _V
55 54 elpr 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. { -u ( _i x. _pi ) , ( _i x. _pi ) } <-> ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = -u ( _i x. _pi ) \/ ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) = ( _i x. _pi ) ) )
56 fvex 
 |-  ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) e. _V
57 56 elpr 
 |-  ( ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) e. { -u _pi , _pi } <-> ( ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = -u _pi \/ ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) = _pi ) )
58 53 55 57 3imtr4i 
 |-  ( ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. { -u ( _i x. _pi ) , ( _i x. _pi ) } -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) e. { -u _pi , _pi } )
59 36 58 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( Im ` ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) ) e. { -u _pi , _pi } )
60 33 59 eqeltrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( 1 - A ) F 1 ) + ( A F ( A - 1 ) ) ) + ( 1 F A ) ) e. { -u _pi , _pi } )