# 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 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
Assertion isosctr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐶𝐴 ) 𝐹 ( 𝐵𝐴 ) ) = ( ( 𝐴𝐵 ) 𝐹 ( 𝐶𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 isosctrlem3.1 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 simp11 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐴 ∈ ℂ )
3 simp13 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐶 ∈ ℂ )
4 2 3 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( 𝐴𝐶 ) ∈ ℂ )
5 simp12 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐵 ∈ ℂ )
6 5 3 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( 𝐵𝐶 ) ∈ ℂ )
7 simp21 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐴𝐶 )
8 2 3 7 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( 𝐴𝐶 ) ≠ 0 )
9 simp22 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐵𝐶 )
10 5 3 9 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( 𝐵𝐶 ) ≠ 0 )
11 simp23 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → 𝐴𝐵 )
12 subcan2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ↔ 𝐴 = 𝐵 ) )
13 12 3ad2ant1 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ↔ 𝐴 = 𝐵 ) )
14 13 necon3bid ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐴𝐶 ) ≠ ( 𝐵𝐶 ) ↔ 𝐴𝐵 ) )
15 11 14 mpbird ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( 𝐴𝐶 ) ≠ ( 𝐵𝐶 ) )
16 simp3 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) )
17 1 isosctrlem3 ( ( ( ( 𝐴𝐶 ) ∈ ℂ ∧ ( 𝐵𝐶 ) ∈ ℂ ) ∧ ( ( 𝐴𝐶 ) ≠ 0 ∧ ( 𝐵𝐶 ) ≠ 0 ∧ ( 𝐴𝐶 ) ≠ ( 𝐵𝐶 ) ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( - ( 𝐴𝐶 ) 𝐹 ( ( 𝐵𝐶 ) − ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) 𝐹 - ( 𝐵𝐶 ) ) )
18 4 6 8 10 15 16 17 syl231anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( - ( 𝐴𝐶 ) 𝐹 ( ( 𝐵𝐶 ) − ( 𝐴𝐶 ) ) ) = ( ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) 𝐹 - ( 𝐵𝐶 ) ) )
19 2 3 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → - ( 𝐴𝐶 ) = ( 𝐶𝐴 ) )
20 5 2 3 nnncan2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐵𝐶 ) − ( 𝐴𝐶 ) ) = ( 𝐵𝐴 ) )
21 19 20 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( - ( 𝐴𝐶 ) 𝐹 ( ( 𝐵𝐶 ) − ( 𝐴𝐶 ) ) ) = ( ( 𝐶𝐴 ) 𝐹 ( 𝐵𝐴 ) ) )
22 2 5 3 nnncan2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) = ( 𝐴𝐵 ) )
23 5 3 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → - ( 𝐵𝐶 ) = ( 𝐶𝐵 ) )
24 22 23 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( ( 𝐴𝐶 ) − ( 𝐵𝐶 ) ) 𝐹 - ( 𝐵𝐶 ) ) = ( ( 𝐴𝐵 ) 𝐹 ( 𝐶𝐵 ) ) )
25 18 21 24 3eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐶𝐵𝐶𝐴𝐵 ) ∧ ( abs ‘ ( 𝐴𝐶 ) ) = ( abs ‘ ( 𝐵𝐶 ) ) ) → ( ( 𝐶𝐴 ) 𝐹 ( 𝐵𝐴 ) ) = ( ( 𝐴𝐵 ) 𝐹 ( 𝐶𝐵 ) ) )