English
For a complex number θ, cos θ = 0 if and only if there exists an integer k such that θ = (2k+1) π / 2.
Русский
Для комплексного числа θ, cos θ = 0 тогда и только тогда, когда существует целое число k такое, что θ = (2k+1) π / 2.
LaTeX
$$$$\\cos\\theta = 0 \\iff \\exists k \\in \\mathbb{Z}, \\theta = \\(2k+1) \\frac{\\pi}{2}$$$$
Lean4
theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2 :=
by
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 :=
by
rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg,
neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
ring_nf
rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]
refine exists_congr fun x => ?_
refine (iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)
ring
