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 _⟩