order_ineq — Mathlib

English

If a certain Lucas–Lehmer residue vanishes, then 2^(p'+2) is strictly less than q(p'+2)^2, where q is the associated parameter.

Русский

Если при некотором p' ноль остаток Лукса–Леммера, то 2^(p'+2) меньше чем q(p'+2)^2, где q — соответствующий параметр.

LaTeX

$$$\forall p'\; (\text{lucasLehmerResidue }(p'+2)=0) \implies 2^{p'+2} < q(p'+2)^2$$$

Lean4

theorem order_ineq (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : 2 ^ (p' + 2) < (q (p' + 2) : ℕ) ^ 2 :=
  calc
    2 ^ (p' + 2) = orderOf (ωUnit (p' + 2)) := (order_ω p' h).symm
    _ ≤ Fintype.card (X (q (p' + 2)))ˣ := orderOf_le_card_univ
    _ < q (p' + 2) ^ 2 := card_units_lt (Nat.lt_of_succ_lt (two_lt_q _))

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