Metamath Proof Explorer

Theorem angpined

Description: If the angle at ABC is _pi , then A is not equal to C. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses angpieqvd.angdef ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
angpieqvd.A ⊢ φ → A ∈ ℂ
angpieqvd.B ⊢ φ → B ∈ ℂ
angpieqvd.C ⊢ φ → C ∈ ℂ
angpieqvd.AneB ⊢ φ → A ≠ B
angpieqvd.BneC ⊢ φ → B ≠ C
Assertion angpined ⊢ φ → A − B F C − B = π → A ≠ C

Proof

Step Hyp Ref Expression
1 angpieqvd.angdef ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 angpieqvd.A ⊢ φ → A ∈ ℂ
3 angpieqvd.B ⊢ φ → B ∈ ℂ
4 angpieqvd.C ⊢ φ → C ∈ ℂ
5 angpieqvd.AneB ⊢ φ → A ≠ B
6 angpieqvd.BneC ⊢ φ → B ≠ C
7 1 2 3 4 5 6 angpieqvdlem2 ⊢ φ → − C − B A − B ∈ ℝ + ↔ A − B F C − B = π
8 1rp ⊢ 1 ∈ ℝ +
9 1re ⊢ 1 ∈ ℝ
10 ax-1ne0 ⊢ 1 ≠ 0
11 rpneg ⊢ 1 ∈ ℝ ∧ 1 ≠ 0 → 1 ∈ ℝ + ↔ ¬ − 1 ∈ ℝ +
12 9 10 11 mp2an ⊢ 1 ∈ ℝ + ↔ ¬ − 1 ∈ ℝ +
13 8 12 mpbi ⊢ ¬ − 1 ∈ ℝ +
14 2 3 subcld ⊢ φ → A − B ∈ ℂ
15 14 adantr ⊢ φ ∧ C = A → A − B ∈ ℂ
16 2 3 5 subne0d ⊢ φ → A − B ≠ 0
17 16 adantr ⊢ φ ∧ C = A → A − B ≠ 0
18 simpr ⊢ φ ∧ C = A → C = A
19 18 oveq1d ⊢ φ ∧ C = A → C − B = A − B
20 15 17 19 diveq1bd ⊢ φ ∧ C = A → C − B A − B = 1
21 20 adantlr ⊢ φ ∧ − C − B A − B ∈ ℝ + ∧ C = A → C − B A − B = 1
22 21 negeqd ⊢ φ ∧ − C − B A − B ∈ ℝ + ∧ C = A → − C − B A − B = − 1
23 simplr ⊢ φ ∧ − C − B A − B ∈ ℝ + ∧ C = A → − C − B A − B ∈ ℝ +
24 22 23 eqeltrrd ⊢ φ ∧ − C − B A − B ∈ ℝ + ∧ C = A → − 1 ∈ ℝ +
25 24 ex ⊢ φ ∧ − C − B A − B ∈ ℝ + → C = A → − 1 ∈ ℝ +
26 25 necon3bd ⊢ φ ∧ − C − B A − B ∈ ℝ + → ¬ − 1 ∈ ℝ + → C ≠ A
27 13 26 mpi ⊢ φ ∧ − C − B A − B ∈ ℝ + → C ≠ A
28 27 ex ⊢ φ → − C − B A − B ∈ ℝ + → C ≠ A
29 necom ⊢ C ≠ A ↔ A ≠ C
30 28 29 syl6ib ⊢ φ → − C − B A − B ∈ ℝ + → A ≠ C
31 7 30 sylbird ⊢ φ → A − B F C − B = π → A ≠ C