English
For any b ≥ 1 and any m, there exists a Fermat pseudoprime n to base b with n ≥ m.
Русский
Для любого b ≥ 1 и любого m существует псевдопростое n по основанию b такое что n ≥ m.
LaTeX
$$∃ n ≥ m, FermatPsp n b$$
Lean4
/-- For all positive bases, there exist infinite **Fermat pseudoprimes** to that base.
Given in this form: for all numbers `b ≥ 1` and `m`, there exists a pseudoprime `n` to base `b` such
that `m ≤ n`. This form is similar to `Nat.exists_infinite_primes`.
-/
theorem exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) : ∃ n : ℕ, FermatPsp n b ∧ m ≤ n :=
by
by_cases b_ge_two : 2 ≤ b
· have h := Nat.exists_infinite_primes (b * (b ^ 2 - 1) + 1 + m)
obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := h
have h₁ : 0 < b := pos_of_gt (Nat.succ_le_iff.mp b_ge_two)
have h₂ : 4 ≤ b ^ 2 := pow_le_pow_left' b_ge_two 2
have h₃ : 0 < b ^ 2 - 1 := tsub_pos_of_lt (lt_of_lt_of_le (by simp) h₂)
have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
have h₅ : b * (b ^ 2 - 1) < p := by omega
have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
have h₉ : 2 < p := lt_of_le_of_lt h₈ h₅
have h₁₀ := psp_from_prime_gt_p b_ge_two hp₂ h₉
use psp_from_prime b p
constructor
· exact psp_from_prime_psp b_ge_two hp₂ h₉ h₆
·
exact
le_trans (show m ≤ p by cutsat)
(le_of_lt h₁₀)
-- If `¬2 ≤ b`, then `b = 1`. Since all composite numbers are pseudoprimes to base 1, we can pick
-- any composite number greater than m. We choose `2 * (m + 2)` because it is greater than `m` and
-- is composite for all natural numbers `m`.
· have h₁ : b = 1 := by omega
rw [h₁]
use 2 * (m + 2)
have : ¬Nat.Prime (2 * (m + 2)) := Nat.not_prime_mul (by cutsat) (by cutsat)
exact ⟨fermatPsp_base_one (by cutsat) this, by cutsat⟩
