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 ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
Assertion isosctr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → C − A F B − A = A − B F C − B

Proof

Step Hyp Ref Expression
1 isosctrlem3.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 simp11 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A ∈ ℂ
3 simp13 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → C ∈ ℂ
4 2 3 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C ∈ ℂ
5 simp12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → B ∈ ℂ
6 5 3 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → B − C ∈ ℂ
7 simp21 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A ≠ C
8 2 3 7 subne0d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C ≠ 0
9 simp22 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → B ≠ C
10 5 3 9 subne0d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → B − C ≠ 0
11 simp23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A ≠ B
12 subcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C = B − C ↔ A = B
13 12 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C = B − C ↔ A = B
14 13 necon3bid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C ≠ B − C ↔ A ≠ B
15 11 14 mpbird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C ≠ B − C
16 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A − C = B − C
17 1 isosctrlem3 ⊢ A − C ∈ ℂ ∧ B − C ∈ ℂ ∧ A − C ≠ 0 ∧ B − C ≠ 0 ∧ A − C ≠ B − C ∧ A − C = B − C → − A − C F B - C - A − C = A - C - B − C F − B − C
18 4 6 8 10 15 16 17 syl231anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → − A − C F B - C - A − C = A - C - B − C F − B − C
19 2 3 negsubdi2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → − A − C = C − A
20 5 2 3 nnncan2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → B - C - A − C = B − A
21 19 20 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → − A − C F B - C - A − C = C − A F B − A
22 2 5 3 nnncan2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A - C - B − C = A − B
23 5 3 negsubdi2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → − B − C = C − B
24 22 23 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → A - C - B − C F − B − C = A − B F C − B
25 18 21 24 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ A ≠ C ∧ B ≠ C ∧ A ≠ B ∧ A − C = B − C → C − A F B − A = A − B F C − B