English
For any positive k, there exists a prime p with p ≡ 1 (mod k) that is larger than any given bound.
Русский
Для любого положительного k существует простое p, удовлетворяющее p ≡ 1 (mod k), причем p может быть сколь угодно большим.
LaTeX
$$$\exists p \in \mathbb{N}, \operatorname{Prime}(p) \wedge n < p \wedge p \equiv 1 \, [MOD\ k]$$$
Lean4
/-- For any positive `k : ℕ` there exists an arbitrarily large prime `p` such that
`p ≡ 1 [MOD k]`. -/
theorem exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) : ∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k] :=
by
rcases (one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
· rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩
exact ⟨p, hp, hnp, modEq_one⟩
let b := k * (n !)
have hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs :=
by
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
calc
1 ≤ b - 1 := le_tsub_of_add_le_left hb
_ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs := sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
let p := minFac (eval (↑b) (cyclotomic k ℤ)).natAbs
haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) :=
by
have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_natCast, this, eval₂_hom,
Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]
apply Int.dvd_natAbs.1
exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
have hpb : ¬p ∣ b := hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩
· exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)
· have hdiv : orderOf (b : ZMod p) ∣ p - 1 := ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
haveI : NeZero (k : ZMod p) := NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
rw [← this] at hdiv
exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm
