English
The equality ((2)•θ).sign = θ.sign holds iff θ = π or |θ.toReal| < π/2.
Русский
Равенство ((2)•θ).sign = θ.sign верно тогда и только тогда, когда θ = π или |θ.toReal| < π/2.
LaTeX
$$((2:\,\mathbb{N})\cdot θ).\text{sign} = θ.\text{sign} \iff θ = π \lor |θ.toReal| < π/2$$
Lean4
theorem sign_two_nsmul_eq_sign_iff {θ : Angle} : ((2 : ℕ) • θ).sign = θ.sign ↔ θ = π ∨ |θ.toReal| < π / 2 :=
by
by_cases hpi : θ = π; · simp [hpi]
rw [or_iff_right hpi]
refine ⟨fun h => ?_, fun h => ?_⟩
· by_contra hle
rw [not_lt, le_abs, le_neg] at hle
have hpi' : θ.toReal ≠ π := by simpa using hpi
rcases hle with (hle | hle) <;> rcases hle.eq_or_lt with (heq | hlt)
· rw [← coe_toReal θ, ← heq] at h
simp at h
· rw [← sign_toReal hpi, sign_pos (pi_div_two_pos.trans hlt), ← sign_toReal,
two_nsmul_toReal_eq_two_mul_sub_two_pi.2 hlt, _root_.sign_neg] at h
· simp at h
· rw [← mul_sub]
exact mul_neg_of_pos_of_neg two_pos (sub_neg.2 ((toReal_le_pi _).lt_of_ne hpi'))
· intro he
simp [he] at h
· rw [← coe_toReal θ, heq] at h
simp at h
· rw [← sign_toReal hpi, _root_.sign_neg (hlt.trans (Left.neg_neg_iff.2 pi_div_two_pos)), ← sign_toReal] at h
swap
· intro he
simp [he] at h
rw [← neg_div] at hlt
rw [two_nsmul_toReal_eq_two_mul_add_two_pi.2 hlt.le, sign_pos] at h
· simp at h
· linarith [neg_pi_lt_toReal θ]
· have hpi' : (2 : ℕ) • θ ≠ π := by
rw [Ne, two_nsmul_eq_pi_iff, not_or]
constructor
· rintro rfl
simp [pi_pos, abs_of_pos] at h
· rintro rfl
rw [toReal_neg_pi_div_two] at h
simp [pi_pos, neg_div, abs_of_pos] at h
rw [abs_lt, ← neg_div] at h
rw [← sign_toReal hpi, ← sign_toReal hpi', two_nsmul_toReal_eq_two_mul.2 ⟨h.1, h.2.le⟩, sign_mul,
sign_pos (zero_lt_two' ℝ), one_mul]
