two_lt_q — Mathlib

English

For every natural p', the smallest prime factor of mersenne(p' + 2) exceeds 2.

Русский

Для любого p' наименьший простой делитель mersenne(p' + 2) больше 2.

LaTeX

$$$ 2 < q(p' + 2) $$$

Lean4

/-- If `1 < p`, then `q p`, the smallest prime factor of `mersenne p`, is more than 2. -/
theorem two_lt_q (p' : ℕ) : 2 < q (p' + 2) :=
  by
  refine (minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_
  · exact le_add_left _ _
  · rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']
    exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

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