English
For every real x, sin(arccos x) = sqrt(1 - x^2).
Русский
Пусть x ∈ ℝ. Тогда sin(arccos x) = √(1 - x^2).
LaTeX
$$\n sin(\arccos x) = \sqrt{1 - x^2}$$
Lean4
theorem sin_arccos (x : ℝ) : sin (arccos x) = √(1 - x ^ 2) :=
by
by_cases hx₁ : -1 ≤ x; swap
· rw [not_le] at hx₁
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
nlinarith
by_cases hx₂ : x ≤ 1; swap
· rw [not_le] at hx₂
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
nlinarith
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]