English
If 0 < x ≤ 1, then sin x > 0.
Русский
Если 0 < x ≤ 1, то sin x > 0.
LaTeX
$$$\\\\forall x \\\\in \\\\mathbb{R}, 0 < x \\\\le 1 \\\\Rightarrow \\\\sin x > 0$$$
Lean4
theorem sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < sin x :=
calc
0 < x - x ^ 3 / 6 - |x| ^ 4 * (5 / 96) :=
sub_pos.2 <|
lt_sub_iff_add_lt.2
(calc
|x| ^ 4 * (5 / 96) + x ^ 3 / 6 ≤ x * (5 / 96) + x / 6 :=
by
gcongr
·
calc
|x| ^ 4 ≤ |x| ^ 1 :=
pow_le_pow_of_le_one (abs_nonneg _) (by rwa [abs_of_nonneg (le_of_lt hx0)]) (by decide)
_ = x := by simp [abs_of_nonneg (le_of_lt hx0)]
·
calc
x ^ 3 ≤ x ^ 1 := pow_le_pow_of_le_one (le_of_lt hx0) hx (by decide)
_ = x := pow_one _
_ < x := by linarith)
_ ≤ sin x := sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound (by rwa [abs_of_nonneg (le_of_lt hx0)]))).2
