English
For all x with -1 ≤ x ≤ 1, cos(arcsin x) = √(1 - x^2).
Русский
Для всех x с -1 ≤ x ≤ 1 выполняется cos(arcsin x) = √(1 - x^2).
LaTeX
$$$-1 \le x \le 1 \Rightarrow \cos(\arcsin x) = \sqrt{1 - x^2}$$$
Lean4
theorem cos_arcsin (x : ℝ) : cos (arcsin x) = √(1 - x ^ 2) :=
by
by_cases hx₁ : -1 ≤ x; swap
· rw [not_le] at hx₁
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
nlinarith
by_cases hx₂ : x ≤ 1; swap
· rw [not_le] at hx₂
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
nlinarith
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
sqrt_mul_self (cos_arcsin_nonneg _)] at this
rw [this, sin_arcsin hx₁ hx₂]
-- The junk values for `arcsin` and `sqrt` make this true even outside `[-1, 1]`.
