# Metamath Proof Explorer

## Theorem isosctr

Description: Isosceles triangle theorem. This is Metamath 100 proof #65. (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 isosctr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left({C}-{A}\right){F}\left({B}-{A}\right)=\left({A}-{B}\right){F}\left({C}-{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 simp11 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}\in ℂ$
3 simp13 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {C}\in ℂ$
4 2 3 subcld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}-{C}\in ℂ$
5 simp12 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {B}\in ℂ$
6 5 3 subcld ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {B}-{C}\in ℂ$
7 simp21 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}\ne {C}$
8 2 3 7 subne0d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}-{C}\ne 0$
9 simp22 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {B}\ne {C}$
10 5 3 9 subne0d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {B}-{C}\ne 0$
11 simp23 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}\ne {B}$
12 subcan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{C}={B}-{C}↔{A}={B}\right)$
13 12 3ad2ant1 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left({A}-{C}={B}-{C}↔{A}={B}\right)$
14 13 necon3bid ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left({A}-{C}\ne {B}-{C}↔{A}\ne {B}\right)$
15 11 14 mpbird ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}-{C}\ne {B}-{C}$
16 simp3 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left|{A}-{C}\right|=\left|{B}-{C}\right|$
17 1 isosctrlem3 ${⊢}\left(\left({A}-{C}\in ℂ\wedge {B}-{C}\in ℂ\right)\wedge \left({A}-{C}\ne 0\wedge {B}-{C}\ne 0\wedge {A}-{C}\ne {B}-{C}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left(-\left({A}-{C}\right)\right){F}\left({B}-{C}-\left({A}-{C}\right)\right)=\left({A}-{C}-\left({B}-{C}\right)\right){F}\left(-\left({B}-{C}\right)\right)$
18 4 6 8 10 15 16 17 syl231anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left(-\left({A}-{C}\right)\right){F}\left({B}-{C}-\left({A}-{C}\right)\right)=\left({A}-{C}-\left({B}-{C}\right)\right){F}\left(-\left({B}-{C}\right)\right)$
19 2 3 negsubdi2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to -\left({A}-{C}\right)={C}-{A}$
20 5 2 3 nnncan2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {B}-{C}-\left({A}-{C}\right)={B}-{A}$
21 19 20 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left(-\left({A}-{C}\right)\right){F}\left({B}-{C}-\left({A}-{C}\right)\right)=\left({C}-{A}\right){F}\left({B}-{A}\right)$
22 2 5 3 nnncan2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to {A}-{C}-\left({B}-{C}\right)={A}-{B}$
23 5 3 negsubdi2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to -\left({B}-{C}\right)={C}-{B}$
24 22 23 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left({A}-{C}-\left({B}-{C}\right)\right){F}\left(-\left({B}-{C}\right)\right)=\left({A}-{B}\right){F}\left({C}-{B}\right)$
25 18 21 24 3eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\wedge {A}\ne {B}\right)\wedge \left|{A}-{C}\right|=\left|{B}-{C}\right|\right)\to \left({C}-{A}\right){F}\left({B}-{A}\right)=\left({A}-{B}\right){F}\left({C}-{B}\right)$