Prime numbers

This file develops the theory of prime numbers: natural numbers p ≥ 2 whose only divisors are p and 1.

theorem Nat.prime_mul_iff {a b : ℕ} : Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

theorem Nat.not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b)

theorem Nat.not_prime_of_mul_eq {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n

@[deprecated Nat.not_prime_of_mul_eq (since := "2025-05-24")]

theorem Nat.not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n

Alias of Nat.not_prime_of_mul_eq.

theorem Nat.Prime.dvd_iff_eq {p a : ℕ} (hp : Prime p) (a1 : a ≠ 1) : a ∣ p ↔ p = a

theorem Nat.Prime.eq_two_or_odd {p : ℕ} (hp : Prime p) : p = 2 ∨ p % 2 = 1

theorem Nat.Prime.eq_two_or_odd' {p : ℕ} (hp : Prime p) : p = 2 ∨ Odd p

theorem Nat.Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p

theorem Nat.Prime.pred_pos {p : ℕ} (pp : Prime p) : 0 < p.pred

theorem Nat.succ_pred_prime {p : ℕ} (pp : Prime p) : p.pred.succ = p

theorem Nat.exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

theorem Nat.exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n

theorem Nat.not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n

theorem Nat.not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n

theorem Nat.not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : ¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

theorem Nat.not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : ¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n

theorem Nat.dvd_of_forall_prime_mul_dvd {a b : ℕ} (hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b) : a ∣ b

theorem Nat.Prime.even_iff {p : ℕ} (hp : Prime p) : Even p ↔ p = 2

theorem Nat.Prime.odd_of_ne_two {p : ℕ} (hp : Prime p) (h_two : p ≠ 2) : Odd p

theorem Nat.Prime.even_sub_one {p : ℕ} (hp : Prime p) (h2 : p ≠ 2) : Even (p - 1)

theorem Nat.Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact (Prime p)] : p % 2 = 1 ↔ p ≠ 2

A prime p satisfies p % 2 = 1 if and only if p ≠ 2.

theorem Nat.coprime_of_dvd' {m n : ℕ} (H : ∀ (k : ℕ), Prime k → k ∣ m → k ∣ n → k ∣ 1) : m.Coprime n

theorem Nat.Prime.dvd_iff_not_coprime {p n : ℕ} (pp : Prime p) : p ∣ n ↔ ¬p.Coprime n

theorem Nat.Prime.not_coprime_iff_dvd {m n : ℕ} : ¬m.Coprime n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n

theorem Nat.coprime_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < n.minFac) : n.Coprime m

If 0 < m < minFac n, then n and m are coprime.

theorem Nat.gcd_eq_one_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < n.minFac) : n.gcd m = 1

If 0 < m < minFac n, then n and m have gcd equal to 1.

theorem Nat.Prime.not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n

@[simp]

theorem Nat.coprime_two_left {n : ℕ} : Coprime 2 n ↔ Odd n

@[simp]

theorem Nat.coprime_two_right {n : ℕ} : n.Coprime 2 ↔ Odd n

theorem Nat.Coprime.odd_of_left {n : ℕ} : Coprime 2 n → Odd n

Alias of the forward direction of Nat.coprime_two_left.

theorem Odd.coprime_two_left {n : ℕ} : Odd n → Nat.Coprime 2 n

Alias of the reverse direction of Nat.coprime_two_left.

theorem Odd.coprime_two_right {n : ℕ} : Odd n → n.Coprime 2

Alias of the reverse direction of Nat.coprime_two_right.

theorem Nat.Coprime.odd_of_right {n : ℕ} : n.Coprime 2 → Odd n

Alias of the forward direction of Nat.coprime_two_right.

theorem Nat.Prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) : p ∣ m

theorem Nat.Prime.not_prime_pow' {x n : ℕ} (hn : n ≠ 1) : ¬Prime (x ^ n)

theorem Nat.Prime.not_prime_pow {x n : ℕ} (hn : 2 ≤ n) : ¬Prime (x ^ n)

theorem Nat.Prime.eq_one_of_pow {x n : ℕ} (h : Prime (x ^ n)) : n = 1

theorem Nat.Prime.pow_eq_iff {p a k : ℕ} (hp : Prime p) : a ^ k = p ↔ a = p ∧ k = 1

theorem Nat.Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : Prime p) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p

theorem Nat.Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : a.Coprime (p ^ m)

theorem Nat.coprime_primes {p q : ℕ} (pp : Prime p) (pq : Prime q) : p.Coprime q ↔ p ≠ q

theorem Nat.coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) : (p ^ n).Coprime (q ^ m)

theorem Nat.coprime_or_dvd_of_prime {p : ℕ} (pp : Prime p) (i : ℕ) : p.Coprime i ∨ p ∣ i

theorem Nat.coprime_of_lt_prime {n p : ℕ} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : p.Coprime n

theorem Nat.eq_or_coprime_of_le_prime {n p : ℕ} (n_pos : 0 < n) (hle : n ≤ p) (pp : Prime p) : p = n ∨ p.Coprime n

theorem Nat.prime_eq_prime_of_dvd_pow {m p q : ℕ} (pp : Prime p) (pq : Prime q) (h : p ∣ q ^ m) : p = q

theorem Nat.dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k

theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Prime p1) (pp2 : Prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) : p1 * p2 ∣ n

theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a p k : ℕ} (pp : Prime p) (h₁ : ¬a ∣ p ^ k) (h₂ : a ∣ p ^ (k + 1)) : a = p ^ (k + 1)

If p is prime, and a doesn't divide p^k, but a does divide p^(k+1) then a = p^(k+1).

theorem Nat.ne_one_iff_exists_prime_dvd {n : ℕ} : n ≠ 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ n

theorem Nat.eq_one_iff_not_exists_prime_dvd {n : ℕ} : n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n

theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Prime p) {m n k l : ℕ} (hpm : p ^ k ∣ m) (hpn : p ^ l ∣ n) (hpmn : p ^ (k + l + 1) ∣ m * n) : p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n