doc-next-gen

Mathlib.Data.Nat.Prime.Basic

Module docstring

{"# Prime numbers

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

"}

Nat.prime_mul_iff theorem
{a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1
Full source 
theorem prime_mul_iff {a b : ℕ} : Nat.PrimeNat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1 := by
  simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]
Prime Product Characterization for Natural Numbers
Informal description
For natural numbers $a$ and $b$, the product $a \cdot b$ is prime if and only if either $a$ is prime and $b = 1$, or $b$ is prime and $a = 1$.
Nat.not_prime_mul theorem
{a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b)
Full source 
theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b) := by
  simp [prime_mul_iff, _root_.not_or, *]
Product of Non-Unit Natural Numbers is Not Prime
Informal description
For any natural numbers $a$ and $b$ such that $a \neq 1$ and $b \neq 1$, the product $a \cdot b$ is not a prime number.
Nat.not_prime_mul' theorem
{a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n
Full source 
theorem not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
  h ▸ not_prime_mul h₁ h₂
Product of Non-Unit Natural Numbers is Not Prime (General Form)
Informal description
For any natural numbers $a$, $b$, and $n$ such that $a \cdot b = n$, $a \neq 1$, and $b \neq 1$, the number $n$ is not prime.
Nat.Prime.dvd_iff_eq theorem
{p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a
Full source 
theorem Prime.dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ pa ∣ p ↔ p = a := by
  refine ⟨?_, by rintro rfl; rfl⟩
  rintro ⟨j, rfl⟩
  rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
  · exact mul_one _
  · exact (a1 rfl).elim
Divisibility Criterion for Prime Numbers: $a \mid p \leftrightarrow a = p$ when $a \neq 1$
Informal description
For a prime natural number $p$ and a natural number $a \neq 1$, $a$ divides $p$ if and only if $a = p$.
Nat.Prime.five_le_of_ne_two_of_ne_three theorem
{p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p
Full source 
theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2)
    (h_three : p ≠ 3) : 5 ≤ p := by
  by_contra! h
  revert h_two h_three hp
  decide +revert
Lower Bound for Primes Not Equal to Two or Three: $5 \leq p$
Informal description
For any prime natural number $p$ such that $p \neq 2$ and $p \neq 3$, it holds that $5 \leq p$.
Nat.Prime.pred_pos theorem
{p : ℕ} (pp : Prime p) : 0 < pred p
Full source 
theorem Prime.pred_pos {p : ℕ} (pp : Prime p) : 0 < pred p :=
  lt_pred_iff.2 pp.one_lt
Positivity of Predecessor for Prime Numbers: $\mathrm{pred}\,p > 0$
Informal description
For any prime natural number $p$, the predecessor of $p$ is positive, i.e., $\mathrm{pred}\,p > 0$.
Nat.succ_pred_prime theorem
{p : ℕ} (pp : Prime p) : succ (pred p) = p
Full source 
theorem succ_pred_prime {p : ℕ} (pp : Prime p) : succ (pred p) = p :=
  succ_pred_eq_of_pos pp.pos
Successor of Predecessor of Prime Equals Itself
Informal description
For any prime natural number $p$, the successor of its predecessor equals $p$ itself, i.e., $(\mathrm{pred}\,p) + 1 = p$.
Nat.exists_dvd_of_not_prime theorem
{n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
Full source 
theorem exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
  ⟨minFac n, minFac_dvd _, ne_of_gt (minFac_prime (ne_of_gt n2)).one_lt,
    ne_of_lt <| (not_prime_iff_minFac_lt n2).1 np⟩
Existence of Non-Trivial Proper Divisor for Composite Numbers
Informal description
For any natural number $n \geq 2$ that is not prime, there exists a natural number $m$ such that $m$ divides $n$, $m \neq 1$, and $m \neq n$.
Nat.exists_dvd_of_not_prime2 theorem
{n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
Full source 
theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) :
    ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n :=
  ⟨minFac n, minFac_dvd _, (minFac_prime (ne_of_gt n2)).two_le,
    (not_prime_iff_minFac_lt n2).1 np⟩
Existence of Non-Trivial Proper Divisor for Composite Numbers
Informal description
For any natural number $n \geq 2$ that is not prime, there exists a natural number $m$ such that $m$ divides $n$, $2 \leq m$, and $m < n$.
Nat.not_prime_of_dvd_of_ne theorem
{m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n
Full source 
theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n :=
  fun h => Or.elim (h.eq_one_or_self_of_dvd m h1) h2 h3
Non-primality from non-trivial proper divisor
Informal description
For natural numbers $m$ and $n$, if $m$ divides $n$ ($m \mid n$), $m \neq 1$, and $m \neq n$, then $n$ is not a prime number.
Nat.not_prime_of_dvd_of_lt theorem
{m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n
Full source 
theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n :=
  not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3)
Non-primality from divisor between 2 and $n-1$
Informal description
For natural numbers $m$ and $n$, if $m$ divides $n$ ($m \mid n$), $2 \leq m$, and $m < n$, then $n$ is not a prime number.
Nat.not_prime_iff_exists_dvd_ne theorem
{n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
Full source 
theorem not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
  ⟨exists_dvd_of_not_prime h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩
Characterization of Non-Prime Numbers via Non-Trivial Proper Divisors
Informal description
For any natural number $n \geq 2$, $n$ is not prime if and only if there exists a natural number $m$ such that $m$ divides $n$, $m \neq 1$, and $m \neq n$.
Nat.not_prime_iff_exists_dvd_lt theorem
{n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
Full source 
theorem not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n :=
  ⟨exists_dvd_of_not_prime2 h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩
Characterization of Non-Prime Numbers via Proper Divisors
Informal description
For any natural number $n \geq 2$, $n$ is not prime if and only if there exists a natural number $m$ such that $m$ divides $n$, $2 \leq m$, and $m < n$.
Nat.dvd_of_forall_prime_mul_dvd theorem
{a b : ℕ} (hdvd : ∀ p : ℕ, p.Prime → p ∣ a → p * a ∣ b) : a ∣ b
Full source 
theorem dvd_of_forall_prime_mul_dvd {a b : ℕ}
    (hdvd : ∀ p : ℕ, p.Prime → p ∣ a → p * a ∣ b) : a ∣ b := by
  obtain rfl | ha := eq_or_ne a 1
  · apply one_dvd
  obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
  exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)
Divisibility Condition via Prime Multiples
Informal description
For any natural numbers $a$ and $b$, if for every prime $p$ dividing $a$ we have $p \cdot a$ divides $b$, then $a$ divides $b$.
Nat.Prime.odd_of_ne_two theorem
{p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) : Odd p
Full source 
theorem Prime.odd_of_ne_two {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) : Odd p :=
  hp.eq_two_or_odd'.resolve_left h_two
Oddness of Primes Not Equal to Two
Informal description
For any prime natural number \( p \) such that \( p \neq 2 \), \( p \) is odd.
Nat.Prime.mod_two_eq_one_iff_ne_two theorem
{p : ℕ} [Fact p.Prime] : p % 2 = 1 ↔ p ≠ 2
Full source 
/-- A prime `p` satisfies `p % 2 = 1` if and only if `p ≠ 2`. -/
theorem Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact p.Prime] : p % 2 = 1 ↔ p ≠ 2 := by
  refine ⟨fun h hf => ?_, (Nat.Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left⟩
  rw [hf] at h
  simp at h
Prime Number Modulo Two Equals One if and only if Not Two
Informal description
For any prime natural number $p$, the remainder when $p$ is divided by 2 is 1 if and only if $p$ is not equal to 2. In other words, $p \equiv 1 \mod 2$ if and only if $p \neq 2$.
Nat.coprime_of_dvd' theorem
{m n : ℕ} (H : ∀ k, Prime k → k ∣ m → k ∣ n → k ∣ 1) : Coprime m n
Full source 
theorem coprime_of_dvd' {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → k ∣ n → k ∣ 1) : Coprime m n :=
  coprime_of_dvd fun k kp km kn => not_le_of_gt kp.one_lt <| le_of_dvd Nat.one_pos <| H k kp km kn
Coprimality from Prime Divisors Dividing One
Informal description
For any natural numbers $m$ and $n$, if for every prime number $k$ that divides both $m$ and $n$, $k$ also divides $1$, then $m$ and $n$ are coprime.
Nat.Prime.dvd_iff_not_coprime theorem
{p n : ℕ} (pp : Prime p) : p ∣ n ↔ ¬Coprime p n
Full source 
theorem Prime.dvd_iff_not_coprime {p n : ℕ} (pp : Prime p) : p ∣ np ∣ n ↔ ¬Coprime p n :=
  iff_not_comm.2 pp.coprime_iff_not_dvd
Prime Divisibility Condition: $p \mid n \leftrightarrow \neg \text{Coprime}(p, n)$
Informal description
For any prime natural number $p$ and any natural number $n$, $p$ divides $n$ if and only if $p$ and $n$ are not coprime, i.e., $p \mid n \leftrightarrow \neg \text{Coprime}(p, n)$.
Nat.Prime.not_coprime_iff_dvd theorem
{m n : ℕ} : ¬Coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
Full source 
theorem Prime.not_coprime_iff_dvd {m n : ℕ} : ¬Coprime m n¬Coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n := by
  apply Iff.intro
  · intro h
    exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
  · intro h
    obtain ⟨p, hp⟩ := h
    apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2
Characterization of Non-Coprime Numbers via Common Prime Divisors
Informal description
For any natural numbers $m$ and $n$, $m$ and $n$ are not coprime if and only if there exists a prime number $p$ such that $p$ divides both $m$ and $n$. In other words, $\neg \text{Coprime}(m, n) \leftrightarrow \exists p, \text{Prime}(p) \land p \mid m \land p \mid n$.
Nat.coprime_of_lt_minFac theorem
{n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : Coprime n m
Full source 
/-- If `0 < m < minFac n`, then `n` and `m` are coprime. -/
lemma coprime_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : Coprime n m  := by
  rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
  push_neg
  exact fun p hp hn hm ↦
    ((le_of_dvd (by omega) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false
Coprimality Condition for Numbers Below Minimal Prime Factor
Informal description
For any natural numbers $n$ and $m$ with $m \neq 0$, if $m$ is less than the minimal prime factor of $n$, then $n$ and $m$ are coprime, i.e., $\gcd(n, m) = 1$.
Nat.gcd_eq_one_of_lt_minFac theorem
{n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : n.gcd m = 1
Full source 
/-- If `0 < m < minFac n`, then `n` and `m` have gcd equal to `1`. -/
lemma gcd_eq_one_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < minFac n) : n.gcd m = 1 :=
  coprime_iff_gcd_eq_one.mp <| coprime_of_lt_minFac h₀ h
Greatest Common Divisor Condition for Numbers Below Minimal Prime Factor
Informal description
For any natural numbers $n$ and $m$ with $m \neq 0$, if $m$ is less than the minimal prime factor of $n$, then the greatest common divisor of $n$ and $m$ is $1$, i.e., $\gcd(n, m) = 1$.
Nat.Prime.not_dvd_mul theorem
{p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n
Full source 
theorem Prime.not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n :=
  mt pp.dvd_mul.1 <| by simp [Hm, Hn]
Prime Does Not Divide Product if It Divides Neither Factor
Informal description
For any prime natural number $p$ and natural numbers $m$ and $n$, if $p$ does not divide $m$ and $p$ does not divide $n$, then $p$ does not divide the product $m \cdot n$.
Nat.coprime_two_right theorem
: n.Coprime 2 ↔ Odd n
Full source 
@[simp] lemma coprime_two_right : n.Coprime 2 ↔ Odd n := coprime_comm.trans coprime_two_left
Coprimality with Two Equals Oddness: $\text{Coprime}(n, 2) \leftrightarrow \text{Odd}(n)$
Informal description
For any natural number $n$, the numbers $n$ and $2$ are coprime if and only if $n$ is odd, i.e., $\text{Coprime}(n, 2) \leftrightarrow \text{Odd}(n)$.
Nat.Prime.dvd_of_dvd_pow theorem
{p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) : p ∣ m
Full source 
theorem Prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) : p ∣ m :=
  pp.prime.dvd_of_dvd_pow h
Prime Divisor Property: $p \mid m^n \Rightarrow p \mid m$ for prime $p$
Informal description
For any prime natural number $p$ and natural numbers $m, n$, if $p$ divides $m^n$, then $p$ divides $m$.
Nat.Prime.not_prime_pow' theorem
{x n : ℕ} (hn : n ≠ 1) : ¬(x ^ n).Prime
Full source 
theorem Prime.not_prime_pow' {x n : ℕ} (hn : n ≠ 1) : ¬(x ^ n).Prime :=
  not_irreducible_pow hn
Power of Natural Number with Exponent Not One is Not Prime
Informal description
For any natural numbers $x$ and $n$ with $n \neq 1$, the number $x^n$ is not prime.
Nat.Prime.not_prime_pow theorem
{x n : ℕ} (hn : 2 ≤ n) : ¬(x ^ n).Prime
Full source 
theorem Prime.not_prime_pow {x n : ℕ} (hn : 2 ≤ n) : ¬(x ^ n).Prime :=
  not_prime_pow' ((two_le_iff _).mp hn).2
Non-primality of Powers with Exponent at Least Two
Informal description
For any natural numbers $x$ and $n$ with $n \geq 2$, the number $x^n$ is not prime.
Nat.Prime.pow_eq_iff theorem
{p a k : ℕ} (hp : p.Prime) : a ^ k = p ↔ a = p ∧ k = 1
Full source 
theorem Prime.pow_eq_iff {p a k : ℕ} (hp : p.Prime) : a ^ k = p ↔ a = p ∧ k = 1 := by
  refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩
  rw [← h] at hp
  rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
Prime Power Equality Characterization: $a^k = p \leftrightarrow a = p \land k = 1$
Informal description
For a prime natural number $p$, and natural numbers $a$ and $k$, the equality $a^k = p$ holds if and only if $a = p$ and $k = 1$.
Nat.Prime.mul_eq_prime_sq_iff theorem
{x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p
Full source 
theorem Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (hy : y ≠ 1) :
    x * y = p ^ 2 ↔ x = p ∧ y = p := by
  refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
  have pdvdxy : p ∣ x * y := by rw [h]; simp [sq]
  -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.
  suffices ∀ x' y' : ℕ, x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p by
    obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy] <;>
      apply this <;>
      assumption
  rintro x y hx hy h ⟨a, ha⟩
  have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h⟩
  obtain ha1 | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
  · subst ha1
    rw [mul_one] at ha
    subst ha
    simp only [sq, mul_right_inj' hp.ne_zero] at h
    subst h
    exact ⟨rfl, rfl⟩
  · refine (hy ?_).elim
    subst hap
    subst ha
    rw [sq, Nat.mul_right_eq_self_iff (Nat.mul_pos hp.pos hp.pos : 0 < a * a)] at h
    exact h
Prime Square Factorization: $x \cdot y = p^2 \leftrightarrow x = p \land y = p$ for $x, y \neq 1$
Informal description
For any prime natural number $p$ and natural numbers $x, y$ with $x \neq 1$ and $y \neq 1$, the product $x \cdot y$ equals $p^2$ if and only if $x = p$ and $y = p$.
Nat.Prime.coprime_pow_of_not_dvd theorem
{p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : Coprime a (p ^ m)
Full source 
theorem Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : Coprime a (p ^ m) :=
  (pp.coprime_iff_not_dvd.2 h).symm.pow_right _
Coprimality of Non-Divisible Number with Prime Power: $\text{Coprime}(a, p^m)$ when $p \nmid a$
Informal description
For any prime natural number $p$, natural number $a$, and positive integer $m$, if $p$ does not divide $a$, then $a$ and $p^m$ are coprime.
Nat.coprime_pow_primes theorem
{p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) : Coprime (p ^ n) (q ^ m)
Full source 
theorem coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) :
    Coprime (p ^ n) (q ^ m) :=
  ((coprime_primes pp pq).2 h).pow _ _
Coprimality of Powers of Distinct Primes: $\text{Coprime}(p^n, q^m)$ for $p \neq q$
Informal description
For any distinct prime natural numbers $p$ and $q$, and for any natural numbers $n$ and $m$, the powers $p^n$ and $q^m$ are coprime.
Nat.coprime_or_dvd_of_prime theorem
{p} (pp : Prime p) (i : ℕ) : Coprime p i ∨ p ∣ i
Full source 
theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : CoprimeCoprime p i ∨ p ∣ i := by
  rw [pp.dvd_iff_not_coprime]; apply em
Prime Divisibility or Coprimality: $\text{Coprime}(p, i) \lor p \mid i$
Informal description
For any prime natural number $p$ and any natural number $i$, either $p$ and $i$ are coprime or $p$ divides $i$.
Nat.coprime_of_lt_prime theorem
{n p} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : Coprime p n
Full source 
theorem coprime_of_lt_prime {n p} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : Coprime p n :=
  (coprime_or_dvd_of_prime pp n).resolve_right fun h => Nat.lt_le_asymm hlt (le_of_dvd n_pos h)
Coprimality of Natural Number Less Than Prime: $\text{Coprime}(p, n)$ for $0 < n < p$
Informal description
For any positive natural number $n$ and prime natural number $p$ such that $n < p$, the numbers $p$ and $n$ are coprime, i.e., $\text{Coprime}(p, n)$.
Nat.prime_eq_prime_of_dvd_pow theorem
{m p q} (pp : Prime p) (pq : Prime q) (h : p ∣ q ^ m) : p = q
Full source 
theorem prime_eq_prime_of_dvd_pow {m p q} (pp : Prime p) (pq : Prime q) (h : p ∣ q ^ m) : p = q :=
  (prime_dvd_prime_iff_eq pp pq).mp (pp.dvd_of_dvd_pow h)
Prime Divisibility of Powers: $p \mid q^m \Rightarrow p = q$
Informal description
For any prime natural numbers $p$ and $q$ and any natural number $m$, if $p$ divides $q^m$, then $p = q$.
Nat.dvd_prime_pow theorem
{p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
Full source 
theorem dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ mi ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k := by
  simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]
Divisibility Condition for Powers of a Prime Number
Informal description
Let $p$ be a prime natural number. For any natural numbers $m$ and $i$, the number $i$ divides $p^m$ if and only if there exists a natural number $k \leq m$ such that $i = p^k$.
Nat.Prime.dvd_mul_of_dvd_ne theorem
{p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Prime p1) (pp2 : Prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) : p1 * p2 ∣ n
Full source 
theorem 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 :=
  Coprime.mul_dvd_of_dvd_of_dvd ((coprime_primes pp1 pp2).mpr h_neq) h1 h2
Product of Distinct Primes Divides Common Multiple
Informal description
For any distinct prime numbers $p_1$ and $p_2$ and any natural number $n$, if $p_1$ divides $n$ and $p_2$ divides $n$, then the product $p_1 \times p_2$ divides $n$.
Nat.ne_one_iff_exists_prime_dvd theorem
: ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
Full source 
theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    let a := n + 2
    have ha : a ≠ 1 := Nat.succ_succ_ne_one n
    simp only [a, true_iff, Ne, not_false_iff, ha]
    exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩
Characterization of Non-One Natural Numbers via Prime Divisors
Informal description
For any natural number $n$, $n \neq 1$ if and only if there exists a prime number $p$ such that $p$ divides $n$.
Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul theorem
{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
Full source 
theorem 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) ∣ mp ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n := by
  have hpd : p ^ (k + l) * p ∣ m * n := by
      let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
      rwa [pow_succ'] at hpmn'
  have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
  have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
  have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
  have hpd5 : p ∣ m / p ^ kp ∣ m / p ^ k ∨ p ∣ n / p ^ l :=
    (Prime.dvd_mul p_prime).1 hpd4
  suffices p ^ k * p ∣ mp ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
  exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h
Prime Power Divisibility of Product Implies Higher Power Divisibility of a Factor
Informal description
Let $p$ be a prime natural number, and let $m, n, k, l$ be natural numbers such that $p^k$ divides $m$, $p^l$ divides $n$, and $p^{k+l+1}$ divides the product $m \cdot n$. Then either $p^{k+1}$ divides $m$ or $p^{l+1}$ divides $n$.