sin_eq_zero_iff — Mathlib

English

sin x = 0 iff there exists an integer n with x = nπ.

Русский

sin x = 0 тогда и только тогда, когда существует целое n такое, что x = nπ.

LaTeX

$$$$\sin x = 0 \iff \exists n \in \mathbb{Z}, n\pi = x$$$$

Lean4

theorem sin_eq_zero_iff {x : ℝ} : sin x = 0 ↔ ∃ n : ℤ, (n : ℝ) * π = x :=
  ⟨fun h =>
    ⟨⌊x / π⌋,
      le_antisymm (sub_nonneg.1 (Int.sub_floor_div_mul_nonneg _ pi_pos))
        (sub_nonpos.1 <|
          le_of_not_gt fun h₃ =>
            (sin_pos_of_pos_of_lt_pi h₃ (Int.sub_floor_div_mul_lt _ pi_pos)).ne
              (by simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]))⟩,
    fun ⟨_, hn⟩ => hn ▸ sin_int_mul_pi _⟩

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