English
If r > 0 and θ ∈ (-π, π), then arg(r (cos θ + i sin θ)) = θ.
Русский
Если r > 0 и θ ∈ (-π, π), то arg(r (cos θ + i sin θ)) = θ.
LaTeX
$$$\\\\arg\\\\left(r(\\\\cos\\\\theta + i\\\\sin\\\\theta)\\\\right) = \\theta , \\quad r>0, \\ theta \\in (-\\\\pi,\\\\pi)$$$
Lean4
theorem arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Set.Ioc (-π) π) :
arg (r * (cos θ + sin θ * I)) = θ :=
by
simp only [arg, norm_mul, norm_cos_add_sin_mul_I, Complex.norm_of_nonneg hr.le, mul_one]
simp only [re_ofReal_mul, im_ofReal_mul, neg_im, ← ofReal_cos, ← ofReal_sin, ← mk_eq_add_mul_I, neg_div,
mul_div_cancel_left₀ _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr]
by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
· rw [if_pos]
exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]
· rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁
rcases h₁ with h₁ | h₁
· replace hθ := hθ.1
have hcos : Real.cos θ < 0 := by
rw [← neg_pos, ← Real.cos_add_pi]
refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right] <;> [linarith; linarith;
exact hsin.not_ge; exact hcos.not_ge]
· replace hθ := hθ.2
have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith; linarith; exact hsin;
exact hcos.not_ge]
