# 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}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right),{y}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\mathrm{log}\left(\frac{{y}}{{x}}\right)\right)\right)$
Assertion isosctrlem3 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({A}\ne 0\wedge {B}\ne 0\wedge {A}\ne {B}\right)\wedge \left|{A}\right|=\left|{B}\right|\right)\to \left(-{A}\right){F}\left({B}-{A}\right)=\left({A}-{B}\right){F}\left(-{B}\right)$

### Proof

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