testFalseHelper — Mathlib

English

For p' with lucasLehmerResidue(p'+2)=0, we have 2^{p'+2} < (q(p'+2))^2.

Русский

Для p' при которых lucasLehmerResidue(p'+2)=0 выполняется неравенство 2^{p'+2} < (q(p'+2))^2.

LaTeX

$$$2^{p'+2} < \bigl(q(p'+2)\bigr)^{2}$$$

Lean4

theorem testFalseHelper (p : ℕ) (hp : Nat.blt 1 p = true) (h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2))) :
    ¬LucasLehmerTest p := by
  rw [Nat.blt_eq] at hp
  rw [Nat.ble_eq, Nat.succ_le, Nat.pos_iff_ne_zero] at h
  rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp, ←
    sModNatTR_eq_sModNat]
  simpa using h

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