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 _))