three_le_nValue — Mathlib

English

If N ≥ 64, then nValue(N) ≥ 3.

Русский

Если N ≥ 64, то nValue(N) ≥ 3.

LaTeX

$$$$ N \\ge 64 \\Rightarrow 3 \\le nValue(N). $$$$

Lean4

theorem three_le_nValue (hN : 64 ≤ N) : 3 ≤ nValue N :=
  by
  rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]
  apply lt_sqrt_of_sq_lt
  have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
    rw [rpow_natCast]
    exact (cast_le.2 hN).trans' (by norm_num1)
  apply lt_of_lt_of_le _ (log_le_log (rpow_pos_of_pos zero_lt_two _) this)
  rw [log_rpow zero_lt_two, ← div_lt_iff₀']
  · exact log_two_gt_d9.trans_le' (by norm_num1)
  · norm_num1

Похожие утверждения