angle_eq_zero_of_angle_eq_pi_left

English

If ∠ABC = π, then ∠BAC = 0.

Русский

Если ∠ABC = π, тогда ∠BAC = 0.

LaTeX

$$$\angle A B C = \pi \Rightarrow \angle B A C = 0$$$

Lean4

/-- If the angle ∠ABC at a point is π, the angle ∠BAC is 0. -/
theorem angle_eq_zero_of_angle_eq_pi_left {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) : ∠ p₂ p₁ p₃ = 0 :=
  by
  unfold angle at h
  rw [angle_eq_pi_iff] at h
  rcases h with ⟨hp₁p₂, ⟨r, ⟨hr, hpr⟩⟩⟩
  unfold angle
  rw [angle_eq_zero_iff]
  rw [← neg_vsub_eq_vsub_rev, neg_ne_zero] at hp₁p₂
  use hp₁p₂, -r + 1, add_pos (neg_pos_of_neg hr) zero_lt_one
  rw [add_smul, ← neg_vsub_eq_vsub_rev p₁ p₂, smul_neg]
  simp [← hpr]

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