dist_eq_abs_sub_dist_iff_angle_eq_zero

English

If ∠ABC = 0, then dist A C = |dist A B − dist C B| is equivalent to ∠ABC = 0.

Русский

Если ∠ABC = 0, то dist(A,C) = |dist(A,B) − dist(C,B)| эквивалентно ∠ABC = 0.

LaTeX

$$$\angle A B C = 0 \Leftrightarrow dist(A,C) = |dist(A,B) - dist(C,B)|$$$

Lean4

/-- If A ≠ B and C ≠ B then ∠ABC = 0 if and only if (dist A C) = abs ((dist A B) - (dist B C)). -/
theorem dist_eq_abs_sub_dist_iff_angle_eq_zero {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) :
    dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ ∠ p₁ p₂ p₃ = 0 :=
  by
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
  exact
    norm_sub_eq_abs_sub_norm_iff_angle_eq_zero (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he)) fun he =>
      hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Похожие утверждения