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 = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion isosctr 
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( C - A ) F ( B - A ) ) = ( ( A - B ) F ( C - B ) ) )

Proof

Step Hyp Ref Expression
1 isosctrlem3.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 simp11 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> A e. CC )
3 simp13 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> C e. CC )
4 2 3 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( A - C ) e. CC )
5 simp12 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> B e. CC )
6 5 3 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( B - C ) e. CC )
7 simp21 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> A =/= C )
8 2 3 7 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( A - C ) =/= 0 )
9 simp22 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> B =/= C )
10 5 3 9 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( B - C ) =/= 0 )
11 simp23 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> A =/= B )
12 subcan2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) = ( B - C ) <-> A = B ) )
13 12 3ad2ant1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( A - C ) = ( B - C ) <-> A = B ) )
14 13 necon3bid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( A - C ) =/= ( B - C ) <-> A =/= B ) )
15 11 14 mpbird 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( A - C ) =/= ( B - C ) )
16 simp3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) )
17 1 isosctrlem3 
 |-  ( ( ( ( A - C ) e. CC /\ ( B - C ) e. CC ) /\ ( ( A - C ) =/= 0 /\ ( B - C ) =/= 0 /\ ( A - C ) =/= ( B - C ) ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( -u ( A - C ) F ( ( B - C ) - ( A - C ) ) ) = ( ( ( A - C ) - ( B - C ) ) F -u ( B - C ) ) )
18 4 6 8 10 15 16 17 syl231anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( -u ( A - C ) F ( ( B - C ) - ( A - C ) ) ) = ( ( ( A - C ) - ( B - C ) ) F -u ( B - C ) ) )
19 2 3 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> -u ( A - C ) = ( C - A ) )
20 5 2 3 nnncan2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( B - C ) - ( A - C ) ) = ( B - A ) )
21 19 20 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( -u ( A - C ) F ( ( B - C ) - ( A - C ) ) ) = ( ( C - A ) F ( B - A ) ) )
22 2 5 3 nnncan2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( A - C ) - ( B - C ) ) = ( A - B ) )
23 5 3 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> -u ( B - C ) = ( C - B ) )
24 22 23 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( ( A - C ) - ( B - C ) ) F -u ( B - C ) ) = ( ( A - B ) F ( C - B ) ) )
25 18 21 24 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( C - A ) F ( B - A ) ) = ( ( A - B ) F ( C - B ) ) )