English
If ∠ABC = π, then ∠CMB = π/2 where M is midpoint of AB
Русский
Если ∠ABC = π, то ∠CMB = π/2, где M — середина AB.
LaTeX
$$$\angle A M B = \frac{\pi}{2}$, где $M$ — середина $AB$$$
Lean4
/-- The angle between three points is π if and only if the second point is strictly between the
other two. -/
theorem angle_eq_pi_iff_sbtw {p₁ p₂ p₃ : P} : ∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃ :=
by
refine ⟨?_, fun h => h.angle₁₂₃_eq_pi⟩
rw [angle, angle_eq_pi_iff]
rintro ⟨hp₁p₂, r, hr, hp₃p₂⟩
refine
⟨⟨1 / (1 - r),
⟨div_nonneg zero_le_one (sub_nonneg.2 (hr.le.trans zero_le_one)),
(div_le_one (sub_pos.2 (hr.trans zero_lt_one))).2 ((le_sub_self_iff 1).2 hr.le)⟩,
?_⟩,
(vsub_ne_zero.1 hp₁p₂).symm, ?_⟩
· rw [← eq_vadd_iff_vsub_eq] at hp₃p₂
rw [AffineMap.lineMap_apply, hp₃p₂, vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev p₂ p₁, smul_neg, ← neg_smul, smul_add,
smul_smul, ← add_smul, eq_comm, eq_vadd_iff_vsub_eq]
convert (one_smul ℝ (p₂ -ᵥ p₁)).symm
field_simp [(sub_pos.2 (hr.trans zero_lt_one)).ne.symm]
ring
· rw [ne_comm, ← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]
exact ⟨hr.ne, hp₁p₂⟩
