Nat.infinite_setOf_prime_modEq_one
theorem Nat.infinite_setOf_prime_modEq_one : ∀ {k : ℕ}, k ≠ 0 → {p | p.Prime ∧ k.ModEq p 1}.Infinite
This theorem asserts that, for any positive natural number `k`, there are infinitely many prime numbers `p` that satisfy the congruence `p ≡ 1 [MOD k]`. In other words, when these prime numbers `p` are divided by `k`, the remainder is always 1. This remains true regardless of the value of `k`, as long as `k` is not zero.
More concisely: For every positive natural number `k`, there exist infinitely many prime numbers `p` such that `p` is congruent to 1 modulo `k`.
|
Nat.exists_prime_gt_modEq_one
theorem Nat.exists_prime_gt_modEq_one : ∀ {k : ℕ} (n : ℕ), k ≠ 0 → ∃ p, p.Prime ∧ n < p ∧ k.ModEq p 1
The theorem `Nat.exists_prime_gt_modEq_one` states that for any non-zero natural number `k`, and any given natural number `n`, there exists a prime number `p` such that `p` is greater than `n` and `p` is congruent to 1 modulo `k`. In mathematical notation, this can be written as: For every non-zero $k \in \mathbb{N}$ and any $n \in \mathbb{N}$, there exists a prime $p$ such that $p>n$ and $p \equiv 1 \mod k$.
More concisely: For every non-zero natural number `k` and natural number `n`, there exists a prime number `p` greater than `n` that is congruent to 1 modulo `k`.
|