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 ‘ ( 𝐵 − 𝐶 ) ) ) → ( ( 𝐶 − 𝐴 ) 𝐹 ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) )