cos_two_neg

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.cos_two_neg

← MathLib Explorer

English

Cosine of 2 is negative.

Русский

Косинус от 2 отрицателен.

LaTeX

$$$\\\\cos 2 < 0$$$

Lean4

theorem cos_two_neg : cos 2 < 0 :=
  calc
    cos 2 = cos (2 * 1) := congr_arg cos (mul_one _).symm
    _ = _ := (Real.cos_two_mul 1)
    _ ≤ 2 * (5 / 9) ^ 2 - 1 := by
      gcongr
      · exact cos_one_pos.le
      · apply cos_one_le
    _ < 0 := by norm_num

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru