Primes congruent to one

We prove that, for any positive k : ℕ, there are infinitely many primes p such that p ≡ 1 [MOD k].

theorem Nat.exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) : ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

For any positive k : ℕ there exists an arbitrarily large prime p such that p ≡ 1 [MOD k].

theorem Nat.frequently_atTop_modEq_one {k : ℕ} (hk0 : k ≠ 0) : ∃ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p ∧ p ≡ 1 [MOD k]

theorem Nat.infinite_setOf_prime_modEq_one {k : ℕ} (hk0 : k ≠ 0) : Set.Infinite {p : ℕ | Nat.Prime p ∧ p ≡ 1 [MOD k]}

For any positive k : ℕ there are infinitely many primes p such that p ≡ 1 [MOD k].