Metamath Proof Explorer

Theorem isosctrlem3

Description: Lemma for isosctr . Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 isosctrlem3.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 simp1l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> A e. CC )
3 simp21 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> A =/= 0 )
4 simp1r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> B e. CC )
5 2 4 subcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A - B ) e. CC )
6 simp23 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> A =/= B )
7 2 4 6 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A - B ) =/= 0 )
8 1 angneg 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( ( A - B ) e. CC /\ ( A - B ) =/= 0 ) ) -> ( -u A F -u ( A - B ) ) = ( A F ( A - B ) ) )
9 2 3 5 7 8 syl22anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( -u A F -u ( A - B ) ) = ( A F ( A - B ) ) )
10 2 4 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> -u ( A - B ) = ( B - A ) )
11 10 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( -u A F -u ( A - B ) ) = ( -u A F ( B - A ) ) )
12 1cnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> 1 e. CC )
13 ax-1ne0 
 |-  1 =/= 0
14 13 a1i 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> 1 =/= 0 )
15 4 2 3 divcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( B / A ) e. CC )
16 12 15 subcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( 1 - ( B / A ) ) e. CC )
17 6 necomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> B =/= A )
18 4 2 3 17 divne1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( B / A ) =/= 1 )
19 18 necomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> 1 =/= ( B / A ) )
20 12 15 19 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( 1 - ( B / A ) ) =/= 0 )
21 1 12 14 16 20 angvald 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( 1 F ( 1 - ( B / A ) ) ) = ( Im ` ( log ` ( ( 1 - ( B / A ) ) / 1 ) ) ) )
22 16 div1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( 1 - ( B / A ) ) / 1 ) = ( 1 - ( B / A ) ) )
23 22 fveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( log ` ( ( 1 - ( B / A ) ) / 1 ) ) = ( log ` ( 1 - ( B / A ) ) ) )
24 23 fveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( Im ` ( log ` ( ( 1 - ( B / A ) ) / 1 ) ) ) = ( Im ` ( log ` ( 1 - ( B / A ) ) ) ) )
25 4 2 3 absdivd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` ( B / A ) ) = ( ( abs ` B ) / ( abs ` A ) ) )
26 simp3 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` A ) = ( abs ` B ) )
27 26 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` B ) = ( abs ` A ) )
28 27 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( abs ` B ) / ( abs ` A ) ) = ( ( abs ` A ) / ( abs ` A ) ) )
29 2 abscld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` A ) e. RR )
30 29 recnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` A ) e. CC )
31 2 3 absne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` A ) =/= 0 )
32 30 31 dividd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( abs ` A ) / ( abs ` A ) ) = 1 )
33 25 28 32 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( abs ` ( B / A ) ) = 1 )
34 19 neneqd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> -. 1 = ( B / A ) )
35 isosctrlem2 
 |-  ( ( ( B / A ) e. CC /\ ( abs ` ( B / A ) ) = 1 /\ -. 1 = ( B / A ) ) -> ( Im ` ( log ` ( 1 - ( B / A ) ) ) ) = ( Im ` ( log ` ( -u ( B / A ) / ( 1 - ( B / A ) ) ) ) ) )
36 15 33 34 35 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( Im ` ( log ` ( 1 - ( B / A ) ) ) ) = ( Im ` ( log ` ( -u ( B / A ) / ( 1 - ( B / A ) ) ) ) ) )
37 15 negcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> -u ( B / A ) e. CC )
38 simp22 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> B =/= 0 )
39 4 2 38 3 divne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( B / A ) =/= 0 )
40 15 39 negne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> -u ( B / A ) =/= 0 )
41 1 16 20 37 40 angvald 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( 1 - ( B / A ) ) F -u ( B / A ) ) = ( Im ` ( log ` ( -u ( B / A ) / ( 1 - ( B / A ) ) ) ) ) )
42 36 41 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( Im ` ( log ` ( 1 - ( B / A ) ) ) ) = ( ( 1 - ( B / A ) ) F -u ( B / A ) ) )
43 21 24 42 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( 1 F ( 1 - ( B / A ) ) ) = ( ( 1 - ( B / A ) ) F -u ( B / A ) ) )
44 2 mulridd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. 1 ) = A )
45 2 12 15 subdid 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. ( 1 - ( B / A ) ) ) = ( ( A x. 1 ) - ( A x. ( B / A ) ) ) )
46 4 2 3 divcan2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. ( B / A ) ) = B )
47 44 46 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A x. 1 ) - ( A x. ( B / A ) ) ) = ( A - B ) )
48 45 47 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. ( 1 - ( B / A ) ) ) = ( A - B ) )
49 44 48 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A x. 1 ) F ( A x. ( 1 - ( B / A ) ) ) ) = ( A F ( A - B ) ) )
50 1 angcan 
 |-  ( ( ( 1 e. CC /\ 1 =/= 0 ) /\ ( ( 1 - ( B / A ) ) e. CC /\ ( 1 - ( B / A ) ) =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. 1 ) F ( A x. ( 1 - ( B / A ) ) ) ) = ( 1 F ( 1 - ( B / A ) ) ) )
51 12 14 16 20 2 3 50 syl222anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A x. 1 ) F ( A x. ( 1 - ( B / A ) ) ) ) = ( 1 F ( 1 - ( B / A ) ) ) )
52 49 51 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A F ( A - B ) ) = ( 1 F ( 1 - ( B / A ) ) ) )
53 2 15 mulneg2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. -u ( B / A ) ) = -u ( A x. ( B / A ) ) )
54 46 negeqd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> -u ( A x. ( B / A ) ) = -u B )
55 53 54 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A x. -u ( B / A ) ) = -u B )
56 48 55 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. -u ( B / A ) ) ) = ( ( A - B ) F -u B ) )
57 1 angcan 
 |-  ( ( ( ( 1 - ( B / A ) ) e. CC /\ ( 1 - ( B / A ) ) =/= 0 ) /\ ( -u ( B / A ) e. CC /\ -u ( B / A ) =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. -u ( B / A ) ) ) = ( ( 1 - ( B / A ) ) F -u ( B / A ) ) )
58 16 20 37 40 2 3 57 syl222anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. -u ( B / A ) ) ) = ( ( 1 - ( B / A ) ) F -u ( B / A ) ) )
59 56 58 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( ( A - B ) F -u B ) = ( ( 1 - ( B / A ) ) F -u ( B / A ) ) )
60 43 52 59 3eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( A F ( A - B ) ) = ( ( A - B ) F -u B ) )
61 9 11 60 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( -u A F ( B - A ) ) = ( ( A - B ) F -u B ) )