English
cos x = 1 iff there exists an integer n with x = (2n)π.
Русский
cos x = 1 тогда и только тогда, когда существует целое n такое, что x = (2n)π.
LaTeX
$$$$\cos x = 1 \iff \exists n \in \mathbb{Z}, \; x = (2n)\pi$$$$
Lean4
theorem cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π) = x :=
⟨fun h =>
let ⟨n, hn⟩ := sin_eq_zero_iff.1 (sin_eq_zero_iff_cos_eq.2 (Or.inl h))
⟨n / 2,
(Int.emod_two_eq_zero_or_one n).elim
(fun hn0 => by
rwa [← mul_assoc, ← @Int.cast_two ℝ, ← Int.cast_mul, Int.ediv_mul_cancel (Int.dvd_iff_emod_eq_zero.2 hn0)])
fun hn1 =>
by
rw [← Int.emod_add_mul_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul, add_comm, mul_comm (2 : ℤ),
Int.cast_mul, mul_assoc, Int.cast_two] at hn
rw [← hn, cos_int_mul_two_pi_add_pi] at h
exact absurd h (by norm_num)⟩,
fun ⟨_, hn⟩ => hn ▸ cos_int_mul_two_pi _⟩
