English
Not-collinear triangle yields a proportional relation between sines of two angles and opposite distances.
Русский
Неколлинеарный треугольник дает пропорцию между синусами двух углов и противоположными расстояниями.
LaTeX
$$$\sin(\angle p_1 p_2 p_3) / dist(p_3 p_1) = \sin(\angle p_3 p_1 p_2) / dist(p_2 p_3)$$$
Lean4
/-- In a triangle, the smaller angle is opposite the smaller side. -/
theorem dist_lt_of_angle_lt {a b c : P} (h : ¬Collinear ℝ ({ a, b, c } : Set P)) :
∠ a c b < ∠ a b c → dist a b < dist a c :=
by
have hsin := law_sin c b a
rw [dist_comm b a, angle_comm c b a] at hsin
have hac : dist a c > 0 := dist_pos.mpr (ne₁₃_of_not_collinear h)
have hsinabc : Real.sin (∠ a b c) ≥ 0 := by
apply Real.sin_nonneg_of_mem_Icc
simp [angle_nonneg, angle_le_pi]
intro h1
by_cases h2 : ∠ a b c ≤ π / 2
· have h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c) := by
exact Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h2 h1
by_contra! w
have h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b := by exact mul_lt_mul h3 w hac hsinabc
linarith
· push_neg at h2
by_contra! w
have h3 : Real.sin (∠ a b c) ≤ Real.sin (∠ a c b) :=
by
by_contra! w1
have h4 : Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b := by exact mul_lt_mul w1 w hac hsinabc
linarith
rw [← Real.sin_pi_sub (∠ a b c)] at h3
have h5 : π - ∠ a b c < π / 2 := by linarith
have h6 : π - ∠ a b c ≤ ∠ a c b := by
by_contra! w1
have := Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h5.le w1
linarith
have h7 := angle_add_angle_add_angle_eq_pi c (ne₁₂_of_not_collinear h).symm
rw [angle_comm b c a] at h7
have h8 : ∠ c a b > 0 := by
rw [angle_comm]
rw [show ({ a, b, c } : Set P) = { b, a, c } by exact Set.insert_comm a b { c }] at h
exact angle_pos_of_not_collinear h
linarith
